Theorem zmax 6168

Description: There is a unique largest integer less than or equal to a given real number.

Assertion

Ref	Expression
zmax	|- (A e. RR -> E!x e. ZZ (x <_ A /\ A.y e. ZZ (y <_ A -> y <_ x)))

Distinct variable group:   x,y,A

Proof of Theorem zmax

Step	Hyp	Ref	Expression
1		renegclt 5409	. . 3 |- (A e. RR -> -uA e. RR)
2		zmin 6167	. . 3 |- (-uA e. RR -> E!z e. ZZ (-uA <_ z /\ A.w e. ZZ (-uA <_ w -> z <_ w)))
3	1, 2	syl 10	. 2 |- (A e. RR -> E!z e. ZZ (-uA <_ z /\ A.w e. ZZ (-uA <_ w -> z <_ w)))
4		lenegt 5630	. . . . . . 7 |- ((x e. RR /\ A e. RR) -> (x <_ A <-> -uA <_ -ux))
5		zret 6086	. . . . . . 7 |- (x e. ZZ -> x e. RR)
6	4, 5	sylan 448	. . . . . 6 |- ((x e. ZZ /\ A e. RR) -> (x <_ A <-> -uA <_ -ux))
7	6	ancoms 436	. . . . 5 |- ((A e. RR /\ x e. ZZ) -> (x <_ A <-> -uA <_ -ux))
8		znegclt 6110	. . . . . . . . . 10 |- (w e. ZZ -> -uw e. ZZ)
9		breq1 2612	. . . . . . . . . . . 12 |- (y = -uw -> (y <_ A <-> -uw <_ A))
10		breq1 2612	. . . . . . . . . . . 12 |- (y = -uw -> (y <_ x <-> -uw <_ x))
11	9, 10	imbi12d 624	. . . . . . . . . . 11 |- (y = -uw -> ((y <_ A -> y <_ x) <-> (-uw <_ A -> -uw <_ x)))
12	11	rcla4v 1864	. . . . . . . . . 10 |- (-uw e. ZZ -> (A.y e. ZZ (y <_ A -> y <_ x) -> (-uw <_ A -> -uw <_ x)))
13	8, 12	syl 10	. . . . . . . . 9 |- (w e. ZZ -> (A.y e. ZZ (y <_ A -> y <_ x) -> (-uw <_ A -> -uw <_ x)))
14		lenegcon1t 5631	. . . . . . . . . . . . . . 15 |- ((w e. RR /\ A e. RR) -> (-uw <_ A <-> -uA <_ w))
15	14	adantrr 395	. . . . . . . . . . . . . 14 |- ((w e. RR /\ (A e. RR /\ x e. ZZ)) -> (-uw <_ A <-> -uA <_ w))
16		lenegcon1t 5631	. . . . . . . . . . . . . . . 16 |- ((w e. RR /\ x e. RR) -> (-uw <_ x <-> -ux <_ w))
17	16, 5	sylan2 451	. . . . . . . . . . . . . . 15 |- ((w e. RR /\ x e. ZZ) -> (-uw <_ x <-> -ux <_ w))
18	17	adantrl 394	. . . . . . . . . . . . . 14 |- ((w e. RR /\ (A e. RR /\ x e. ZZ)) -> (-uw <_ x <-> -ux <_ w))
19	15, 18	imbi12d 624	. . . . . . . . . . . . 13 |- ((w e. RR /\ (A e. RR /\ x e. ZZ)) -> ((-uw <_ A -> -uw <_ x) <-> (-uA <_ w -> -ux <_ w)))
20		zret 6086	. . . . . . . . . . . . 13 |- (w e. ZZ -> w e. RR)
21	19, 20	sylan 448	. . . . . . . . . . . 12 |- ((w e. ZZ /\ (A e. RR /\ x e. ZZ)) -> ((-uw <_ A -> -uw <_ x) <-> (-uA <_ w -> -ux <_ w)))
22	21	biimpd 153	. . . . . . . . . . 11 |- ((w e. ZZ /\ (A e. RR /\ x e. ZZ)) -> ((-uw <_ A -> -uw <_ x) -> (-uA <_ w -> -ux <_ w)))
23	22	ex 373	. . . . . . . . . 10 |- (w e. ZZ -> ((A e. RR /\ x e. ZZ) -> ((-uw <_ A -> -uw <_ x) -> (-uA <_ w -> -ux <_ w))))
24	23	com23 32	. . . . . . . . 9 |- (w e. ZZ -> ((-uw <_ A -> -uw <_ x) -> ((A e. RR /\ x e. ZZ) -> (-uA <_ w -> -ux <_ w))))
25	13, 24	syld 27	. . . . . . . 8 |- (w e. ZZ -> (A.y e. ZZ (y <_ A -> y <_ x) -> ((A e. RR /\ x e. ZZ) -> (-uA <_ w -> -ux <_ w))))
26	25	com13 33	. . . . . . 7 |- ((A e. RR /\ x e. ZZ) -> (A.y e. ZZ (y <_ A -> y <_ x) -> (w e. ZZ -> (-uA <_ w -> -ux <_ w))))
27	26	r19.21adv 1710	. . . . . 6 |- ((A e. RR /\ x e. ZZ) -> (A.y e. ZZ (y <_ A -> y <_ x) -> A.w e. ZZ (-uA <_ w -> -ux <_ w)))
28		znegclt 6110	. . . . . . . . . 10 |- (y e. ZZ -> -uy e. ZZ)
29		breq2 2613	. . . . . . . . . . . 12 |- (w = -uy -> (-uA <_ w <-> -uA <_ -uy))
30		breq2 2613	. . . . . . . . . . . 12 |- (w = -uy -> (-ux <_ w <-> -ux <_ -uy))
31	29, 30	imbi12d 624	. . . . . . . . . . 11 |- (w = -uy -> ((-uA <_ w -> -ux <_ w) <-> (-uA <_ -uy -> -ux <_ -uy)))
32	31	rcla4v 1864	. . . . . . . . . 10 |- (-uy e. ZZ -> (A.w e. ZZ (-uA <_ w -> -ux <_ w) -> (-uA <_ -uy -> -ux <_ -uy)))
33	28, 32	syl 10	. . . . . . . . 9 |- (y e. ZZ -> (A.w e. ZZ (-uA <_ w -> -ux <_ w) -> (-uA <_ -uy -> -ux <_ -uy)))
34		lenegt 5630	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ A e. RR) -> (y <_ A <-> -uA <_ -uy))
35	34	adantrr 395	. . . . . . . . . . . . . 14 |- ((y e. RR /\ (A e. RR /\ x e. ZZ)) -> (y <_ A <-> -uA <_ -uy))
36		lenegt 5630	. . . . . . . . . . . . . . . 16 |- ((y e. RR /\ x e. RR) -> (y <_ x <-> -ux <_ -uy))
37	36, 5	sylan2 451	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ x e. ZZ) -> (y <_ x <-> -ux <_ -uy))
38	37	adantrl 394	. . . . . . . . . . . . . 14 |- ((y e. RR /\ (A e. RR /\ x e. ZZ)) -> (y <_ x <-> -ux <_ -uy))
39	35, 38	imbi12d 624	. . . . . . . . . . . . 13 |- ((y e. RR /\ (A e. RR /\ x e. ZZ)) -> ((y <_ A -> y <_ x) <-> (-uA <_ -uy -> -ux <_ -uy)))
40		zret 6086	. . . . . . . . . . . . 13 |- (y e. ZZ -> y e. RR)
41	39, 40	sylan 448	. . . . . . . . . . . 12 |- ((y e. ZZ /\ (A e. RR /\ x e. ZZ)) -> ((y <_ A -> y <_ x) <-> (-uA <_ -uy -> -ux <_ -uy)))
42	41	biimprd 154	. . . . . . . . . . 11 |- ((y e. ZZ /\ (A e. RR /\ x e. ZZ)) -> ((-uA <_ -uy -> -ux <_ -uy) -> (y <_ A -> y <_ x)))
43	42	ex 373	. . . . . . . . . 10 |- (y e. ZZ -> ((A e. RR /\ x e. ZZ) -> ((-uA <_ -uy -> -ux <_ -uy) -> (y <_ A -> y <_ x))))
44	43	com23 32	. . . . . . . . 9 |- (y e. ZZ -> ((-uA <_ -uy -> -ux <_ -uy) -> ((A e. RR /\ x e. ZZ) -> (y <_ A -> y <_ x))))
45	33, 44	syld 27	. . . . . . . 8 |- (y e. ZZ -> (A.w e. ZZ (-uA <_ w -> -ux <_ w) -> ((A e. RR /\ x e. ZZ) -> (y <_ A -> y <_ x))))
46	45	com13 33	. . . . . . 7 |- ((A e. RR /\ x e. ZZ) -> (A.w e. ZZ (-uA <_ w -> -ux <_ w) -> (y e. ZZ -> (y <_ A -> y <_ x))))
47	46	r19.21adv 1710	. . . . . 6 |- ((A e. RR /\ x e. ZZ) -> (A.w e. ZZ (-uA <_ w -> -ux <_ w) -> A.y e. ZZ (y <_ A -> y <_ x)))
48	27, 47	impbid 514	. . . . 5 |- ((A e. RR /\ x e. ZZ) -> (A.y e. ZZ (y <_ A -> y <_ x) <-> A.w e. ZZ (-uA <_ w -> -ux <_ w)))
49	7, 48	anbi12d 626	. . . 4 |- ((A e. RR /\ x e. ZZ) -> ((x <_ A /\ A.y e. ZZ (y <_ A -> y <_ x)) <-> (-uA <_ -ux /\ A.w e. ZZ (-uA <_ w -> -ux <_ w))))
50	49	reubidva 1771	. . 3 |- (A e. RR -> (E!x e. ZZ (x <_ A /\ A.y e. ZZ (y <_ A -> y <_ x)) <-> E!x e. ZZ (-uA <_ -ux /\ A.w e. ZZ (-uA <_ w -> -ux <_ w))))
51		znegclt 6110	. . . 4 |- (x e. ZZ -> -ux e. ZZ)
52		znegclt 6110	. . . . 5 |- (z e. ZZ -> -uz e. ZZ)
53		negcon2t 5383	. . . . . 6 |- ((z e. CC /\ x e. CC) -> (z = -ux <-> x = -uz))
54		zcnt 6087	. . . . . 6 |- (z e. ZZ -> z e. CC)
55		zcnt 6087	. . . . . 6 |- (x e. ZZ -> x e. CC)
56	53, 54, 55	syl2an 454	. . . . 5 |- ((z e. ZZ /\ x e. ZZ) -> (z = -ux <-> x = -uz))
57	52, 56	reuhyp 2895	. . . 4 |- (z e. ZZ -> E!x e. ZZ z = -ux)
58		breq2 2613	. . . . 5 |- (z = -ux -> (-uA <_ z <-> -uA <_ -ux))
59		breq1 2612	. . . . . . 7 |- (z = -ux -> (z <_ w <-> -ux <_ w))
60	59	imbi2d 610	. . . . . 6 |- (z = -ux -> ((-uA <_ w -> z <_ w) <-> (-uA <_ w -> -ux <_ w)))
61	60	ralbidv 1655	. . . . 5 |- (z = -ux -> (A.w e. ZZ (-uA <_ w -> z <_ w) <-> A.w e. ZZ (-uA <_ w -> -ux <_ w)))
62	58, 61	anbi12d 626	. . . 4 |- (z = -ux -> ((-uA <_ z /\ A.w e. ZZ (-uA <_ w -> z <_ w)) <-> (-uA <_ -ux /\ A.w e. ZZ (-uA <_ w -> -ux <_ w))))
63	51, 57, 62	reuxfr 2894	. . 3 |- (E!z e. ZZ (-uA <_ z /\ A.w e. ZZ (-uA <_ w -> z <_ w)) <-> E!x e.