Theorem zmax 4618

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(s):   x,y,A

Proof of Theorem zmax

Step	Hyp	Ref	Expression
1		renegclt 4172	. . 3 |- (A e. RR -> -uA e. RR)
2		zmin 4617	. . 3 |- (-uA e. RR -> E!z e. ZZ (-uA <_ z /\ A.w e. ZZ (-uA <_ w -> z <_ w)))
3	1, 2	syl 12	. 2 |- (A e. RR -> E!z e. ZZ (-uA <_ z /\ A.w e. ZZ (-uA <_ w -> z <_ w)))
4		lenegt 4368	. . . . . . 7 |- ((x e. RR /\ A e. RR) -> (x <_ A <-> -uA <_ -ux))
5		zret 4567	. . . . . . 7 |- (x e. ZZ -> x e. RR)
6	4, 5	sylan 343	. . . . . 6 |- ((x e. ZZ /\ A e. RR) -> (x <_ A <-> -uA <_ -ux))
7	6	ancoms 334	. . . . 5 |- ((A e. RR /\ x e. ZZ) -> (x <_ A <-> -uA <_ -ux))
8		breq1 2065	. . . . . . . . . . . . . . 15 |- (y = -uw -> (y <_ A <-> -uw <_ A))
9		breq1 2065	. . . . . . . . . . . . . . 15 |- (y = -uw -> (y <_ x <-> -uw <_ x))
10	8, 9	imbi12d 474	. . . . . . . . . . . . . 14 |- (y = -uw -> ((y <_ A -> y <_ x) <-> (-uw <_ A -> -uw <_ x)))
11	10	rcla4v 1402	. . . . . . . . . . . . 13 |- (A.y e. ZZ (y <_ A -> y <_ x) -> (-uw e. ZZ -> (-uw <_ A -> -uw <_ x)))
12	11	imp 277	. . . . . . . . . . . 12 |- ((A.y e. ZZ (y <_ A -> y <_ x) /\ -uw e. ZZ) -> (-uw <_ A -> -uw <_ x))
13		znegclt 4588	. . . . . . . . . . . 12 |- (w e. ZZ -> -uw e. ZZ)
14	12, 13	sylan2 346	. . . . . . . . . . 11 |- ((A.y e. ZZ (y <_ A -> y <_ x) /\ w e. ZZ) -> (-uw <_ A -> -uw <_ x))
15	14	adantr 306	. . . . . . . . . 10 |- (((A.y e. ZZ (y <_ A -> y <_ x) /\ w e. ZZ) /\ (A e. RR /\ x e. ZZ)) -> (-uw <_ A -> -uw <_ x))
16		lenegcon1t 4369	. . . . . . . . . . . . . 14 |- ((w e. RR /\ A e. RR) -> (-uw <_ A <-> -uA <_ w))
17	16	adantrr 312	. . . . . . . . . . . . 13 |- ((w e. RR /\ (A e. RR /\ x e. ZZ)) -> (-uw <_ A <-> -uA <_ w))
18		lenegcon1t 4369	. . . . . . . . . . . . . . 15 |- ((w e. RR /\ x e. RR) -> (-uw <_ x <-> -ux <_ w))
19	18, 5	sylan2 346	. . . . . . . . . . . . . 14 |- ((w e. RR /\ x e. ZZ) -> (-uw <_ x <-> -ux <_ w))
20	19	adantrl 311	. . . . . . . . . . . . 13 |- ((w e. RR /\ (A e. RR /\ x e. ZZ)) -> (-uw <_ x <-> -ux <_ w))
21	17, 20	imbi12d 474	. . . . . . . . . . . 12 |- ((w e. RR /\ (A e. RR /\ x e. ZZ)) -> ((-uw <_ A -> -uw <_ x) <-> (-uA <_ w -> -ux <_ w)))
22		zret 4567	. . . . . . . . . . . 12 |- (w e. ZZ -> w e. RR)
23	21, 22	sylan 343	. . . . . . . . . . 11 |- ((w e. ZZ /\ (A e. RR /\ x e. ZZ)) -> ((-uw <_ A -> -uw <_ x) <-> (-uA <_ w -> -ux <_ w)))
24	23	adantll 309	. . . . . . . . . 10 |- (((A.y e. ZZ (y <_ A -> y <_ x) /\ w e. ZZ) /\ (A e. RR /\ x e. ZZ)) -> ((-uw <_ A -> -uw <_ x) <-> (-uA <_ w -> -ux <_ w)))
25	15, 24	mpbid 170	. . . . . . . . 9 |- (((A.y e. ZZ (y <_ A -> y <_ x) /\ w e. ZZ) /\ (A e. RR /\ x e. ZZ)) -> (-uA <_ w -> -ux <_ w))
26	25	exp31 293	. . . . . . . 8 |- (A.y e. ZZ (y <_ A -> y <_ x) -> (w e. ZZ -> ((A e. RR /\ x e. ZZ) -> (-uA <_ w -> -ux <_ w))))
27	26	com3r 35	. . . . . . 7 |- ((A e. RR /\ x e. ZZ) -> (A.y e. ZZ (y <_ A -> y <_ x) -> (w e. ZZ -> (-uA <_ w -> -ux <_ w))))
28	27	r19.21adv 1262	. . . . . 6 |- ((A e. RR /\ x e. ZZ) -> (A.y e. ZZ (y <_ A -> y <_ x) -> A.w e. ZZ (-uA <_ w -> -ux <_ w)))
29		breq2 2066	. . . . . . . . . . . . . . 15 |- (w = -uy -> (-uA <_ w <-> -uA <_ -uy))
30		breq2 2066	. . . . . . . . . . . . . . 15 |- (w = -uy -> (-ux <_ w <-> -ux <_ -uy))
31	29, 30	imbi12d 474	. . . . . . . . . . . . . 14 |- (w = -uy -> ((-uA <_ w -> -ux <_ w) <-> (-uA <_ -uy -> -ux <_ -uy)))
32	31	rcla4v 1402	. . . . . . . . . . . . 13 |- (A.w e. ZZ (-uA <_ w -> -ux <_ w) -> (-uy e. ZZ -> (-uA <_ -uy -> -ux <_ -uy)))
33	32	imp 277	. . . . . . . . . . . 12 |- ((A.w e. ZZ (-uA <_ w -> -ux <_ w) /\ -uy e. ZZ) -> (-uA <_ -uy -> -ux <_ -uy))
34		znegclt 4588	. . . . . . . . . . . 12 |- (y e. ZZ -> -uy e. ZZ)
35	33, 34	sylan2 346	. . . . . . . . . . 11 |- ((A.w e. ZZ (-uA <_ w -> -ux <_ w) /\ y e. ZZ) -> (-uA <_ -uy -> -ux <_ -uy))
36	35	adantr 306	. . . . . . . . . 10 |- (((A.w e. ZZ (-uA <_ w -> -ux <_ w) /\ y e. ZZ) /\ (A e. RR /\ x e. ZZ)) -> (-uA <_ -uy -> -ux <_ -uy))
37		lenegt 4368	. . . . . . . . . . . . . 14 |- ((y e. RR /\ A e. RR) -> (y <_ A <-> -uA <_ -uy))
38	37	adantrr 312	. . . . . . . . . . . . 13 |- ((y e. RR /\ (A e. RR /\ x e. ZZ)) -> (y <_ A <-> -uA <_ -uy))
39		lenegt 4368	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ x e. RR) -> (y <_ x <-> -ux <_ -uy))
40	39, 5	sylan2 346	. . . . . . . . . . . . . 14 |- ((y e. RR /\ x e. ZZ) -> (y <_ x <-> -ux <_ -uy))
41	40	adantrl 311	. . . . . . . . . . . . 13 |- ((y e. RR /\ (A e. RR /\ x e. ZZ)) -> (y <_ x <-> -ux <_ -uy))
42	38, 41	imbi12d 474	. . . . . . . . . . . 12 |- ((y e. RR /\ (A e. RR /\ x e. ZZ)) -> ((y <_ A -> y <_ x) <-> (-uA <_ -uy -> -ux <_ -uy)))
43		zret 4567	. . . . . . . . . . . 12 |- (y e. ZZ -> y e. RR)
44	42, 43	sylan 343	. . . . . . . . . . 11 |- ((y e. ZZ /\ (A e. RR /\ x e. ZZ)) -> ((y <_ A -> y <_ x) <-> (-uA <_ -uy -> -ux <_ -uy)))
45	44	adantll 309	. . . . . . . . . 10 |- (((A.w e. ZZ (-uA <_ w -> -ux <_ w) /\ y e. ZZ) /\ (A e. RR /\ x e. ZZ)) -> ((y <_ A -> y <_ x) <-> (-uA <_ -uy -> -ux <_ -uy)))
46	36, 45	mpbird 171	. . . . . . . . 9 |- (((A.w e. ZZ (-uA <_ w -> -ux <_ w) /\ y e. ZZ) /\ (A e. RR /\ x e. ZZ)) -> (y <_ A -> y <_ x))
47	46	exp31 293	. . . . . . . 8 |- (A.w e. ZZ (-uA <_ w -> -ux <_ w) -> (y e. ZZ -> ((A e. RR /\ x e. ZZ) -> (y <_ A -> y <_ x))))
48	47	com3r 35	. . . . . . 7 |- ((A e. RR /\ x e. ZZ) -> (A.w e. ZZ (-uA <_ w -> -ux <_ w) -> (y e. ZZ -> (y <_ A -> y <_ x))))
49	48	r19.21adv 1262	. . . . . 6 |- ((A e. RR /\ x e. ZZ) -> (A.w e. ZZ (-uA <_ w -> -ux <_ w) -> A.y e. ZZ (y <_ A -> y <_ x)))
50	28, 49	impbid 397	. . . . 5 |- ((A e. RR /\ x e. ZZ) -> (A.y e. ZZ (y <_ A -> y <_ x) <-> A.w e. ZZ (-uA <_ w -> -ux <_ w)))
51	7, 50	anbi12d 476	. . . 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))))
52	51	bireudva 1317	. . 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))))
53		znegclt 4588	. . . 4 |- (x e. ZZ -> -ux e. ZZ)
54		znegclt 4588	. . . . 5 |- (z e. ZZ -> -uz e. ZZ)
55		negcon2t 4168	. . . . . 6 |- ((z e. CC /\ x e. CC) -> (z = -ux <-> x = -uz))
56		zcnt 4568	. . . . . 6 |- (z e. ZZ -> z e. CC)
57		zcnt 4568	. . . . . 6 |- (x e. ZZ -> x e. CC)
58	55, 56, 57	syl2an 349	. . . . 5 |- ((z e. ZZ /\ x e. ZZ) -> (z = -ux <-> x = -uz))
59	54, 58	reuhyp 1581	. . . 4 |- (z e. ZZ -> E!x e. ZZ z = -ux)
60		breq2 2066	. . . . 5 |- (z = -ux -> (-uA <_ z <-> -uA <_ -ux))
61		breq1 2065	. . . . . . 7 |- (z = -ux -> (z <_ w <-> -ux <_ w))
62	61	imbi2d 464	. . . . . 6 |- (z = -ux -> ((-uA <_ w -> z <_ w) <-> (-uA <_ w -> -ux <_ w)))
63	62	biraldv 1219	. . . . 5 |- (z = -ux -> (A.w e. ZZ (-uA <_ w -> z <_ w) <-> A.w e. ZZ (-uA <_ w -> -ux <_ w)))
64	60, 63	anbi12d 476	. . . 4 |- (z = -ux -> ((-uA <_ z /\ A.w e. ZZ (-uA <_ w -> z <_ w))