Metamath Proof Explorer

Theorem zmax

Description: There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( A e. RR -> -u A e. RR )
2 zmin 
 |-  ( -u A e. RR -> E! z e. ZZ ( -u A <_ z /\ A. w e. ZZ ( -u A <_ w -> z <_ w ) ) )
3 1 2 syl 
 |-  ( A e. RR -> E! z e. ZZ ( -u A <_ z /\ A. w e. ZZ ( -u A <_ w -> z <_ w ) ) )
4 znegcl 
 |-  ( x e. ZZ -> -u x e. ZZ )
5 znegcl 
 |-  ( z e. ZZ -> -u z e. ZZ )
6 zcn 
 |-  ( z e. ZZ -> z e. CC )
7 zcn 
 |-  ( x e. ZZ -> x e. CC )
8 negcon2 
 |-  ( ( z e. CC /\ x e. CC ) -> ( z = -u x <-> x = -u z ) )
9 6 7 8 syl2an 
 |-  ( ( z e. ZZ /\ x e. ZZ ) -> ( z = -u x <-> x = -u z ) )
10 5 9 reuhyp 
 |-  ( z e. ZZ -> E! x e. ZZ z = -u x )
11 breq2 
 |-  ( z = -u x -> ( -u A <_ z <-> -u A <_ -u x ) )
12 breq1 
 |-  ( z = -u x -> ( z <_ w <-> -u x <_ w ) )
13 12 imbi2d 
 |-  ( z = -u x -> ( ( -u A <_ w -> z <_ w ) <-> ( -u A <_ w -> -u x <_ w ) ) )
14 13 ralbidv 
 |-  ( z = -u x -> ( A. w e. ZZ ( -u A <_ w -> z <_ w ) <-> A. w e. ZZ ( -u A <_ w -> -u x <_ w ) ) )
15 11 14 anbi12d 
 |-  ( z = -u x -> ( ( -u A <_ z /\ A. w e. ZZ ( -u A <_ w -> z <_ w ) ) <-> ( -u A <_ -u x /\ A. w e. ZZ ( -u A <_ w -> -u x <_ w ) ) ) )
16 4 10 15 reuxfr1 
 |-  ( E! z e. ZZ ( -u A <_ z /\ A. w e. ZZ ( -u A <_ w -> z <_ w ) ) <-> E! x e. ZZ ( -u A <_ -u x /\ A. w e. ZZ ( -u A <_ w -> -u x <_ w ) ) )
17 zre 
 |-  ( x e. ZZ -> x e. RR )
18 leneg 
 |-  ( ( x e. RR /\ A e. RR ) -> ( x <_ A <-> -u A <_ -u x ) )
19 17 18 sylan 
 |-  ( ( x e. ZZ /\ A e. RR ) -> ( x <_ A <-> -u A <_ -u x ) )
20 19 ancoms 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( x <_ A <-> -u A <_ -u x ) )
21 znegcl 
 |-  ( w e. ZZ -> -u w e. ZZ )
22 breq1 
 |-  ( y = -u w -> ( y <_ A <-> -u w <_ A ) )
23 breq1 
 |-  ( y = -u w -> ( y <_ x <-> -u w <_ x ) )
24 22 23 imbi12d 
 |-  ( y = -u w -> ( ( y <_ A -> y <_ x ) <-> ( -u w <_ A -> -u w <_ x ) ) )
25 24 rspcv 
 |-  ( -u w e. ZZ -> ( A. y e. ZZ ( y <_ A -> y <_ x ) -> ( -u w <_ A -> -u w <_ x ) ) )
26 21 25 syl 
 |-  ( w e. ZZ -> ( A. y e. ZZ ( y <_ A -> y <_ x ) -> ( -u w <_ A -> -u w <_ x ) ) )
27 zre 
 |-  ( w e. ZZ -> w e. RR )
28 lenegcon1 
 |-  ( ( w e. RR /\ A e. RR ) -> ( -u w <_ A <-> -u A <_ w ) )
29 28 adantrr 
 |-  ( ( w e. RR /\ ( A e. RR /\ x e. ZZ ) ) -> ( -u w <_ A <-> -u A <_ w ) )
30 lenegcon1 
 |-  ( ( w e. RR /\ x e. RR ) -> ( -u w <_ x <-> -u x <_ w ) )
31 17 30 sylan2 
 |-  ( ( w e. RR /\ x e. ZZ ) -> ( -u w <_ x <-> -u x <_ w ) )
32 31 adantrl 
 |-  ( ( w e. RR /\ ( A e. RR /\ x e. ZZ ) ) -> ( -u w <_ x <-> -u x <_ w ) )
33 29 32 imbi12d 
 |-  ( ( w e. RR /\ ( A e. RR /\ x e. ZZ ) ) -> ( ( -u w <_ A -> -u w <_ x ) <-> ( -u A <_ w -> -u x <_ w ) ) )
34 27 33 sylan 
 |-  ( ( w e. ZZ /\ ( A e. RR /\ x e. ZZ ) ) -> ( ( -u w <_ A -> -u w <_ x ) <-> ( -u A <_ w -> -u x <_ w ) ) )
35 34 biimpd 
 |-  ( ( w e. ZZ /\ ( A e. RR /\ x e. ZZ ) ) -> ( ( -u w <_ A -> -u w <_ x ) -> ( -u A <_ w -> -u x <_ w ) ) )
36 35 ex 
 |-  ( w e. ZZ -> ( ( A e. RR /\ x e. ZZ ) -> ( ( -u w <_ A -> -u w <_ x ) -> ( -u A <_ w -> -u x <_ w ) ) ) )
37 36 com23 
 |-  ( w e. ZZ -> ( ( -u w <_ A -> -u w <_ x ) -> ( ( A e. RR /\ x e. ZZ ) -> ( -u A <_ w -> -u x <_ w ) ) ) )
38 26 37 syld 
 |-  ( w e. ZZ -> ( A. y e. ZZ ( y <_ A -> y <_ x ) -> ( ( A e. RR /\ x e. ZZ ) -> ( -u A <_ w -> -u x <_ w ) ) ) )
39 38 com13 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( A. y e. ZZ ( y <_ A -> y <_ x ) -> ( w e. ZZ -> ( -u A <_ w -> -u x <_ w ) ) ) )
40 39 ralrimdv 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( A. y e. ZZ ( y <_ A -> y <_ x ) -> A. w e. ZZ ( -u A <_ w -> -u x <_ w ) ) )
41 znegcl 
 |-  ( y e. ZZ -> -u y e. ZZ )
42 breq2 
 |-  ( w = -u y -> ( -u A <_ w <-> -u A <_ -u y ) )
43 breq2 
 |-  ( w = -u y -> ( -u x <_ w <-> -u x <_ -u y ) )
44 42 43 imbi12d 
 |-  ( w = -u y -> ( ( -u A <_ w -> -u x <_ w ) <-> ( -u A <_ -u y -> -u x <_ -u y ) ) )
45 44 rspcv 
 |-  ( -u y e. ZZ -> ( A. w e. ZZ ( -u A <_ w -> -u x <_ w ) -> ( -u A <_ -u y -> -u x <_ -u y ) ) )
46 41 45 syl 
 |-  ( y e. ZZ -> ( A. w e. ZZ ( -u A <_ w -> -u x <_ w ) -> ( -u A <_ -u y -> -u x <_ -u y ) ) )
47 zre 
 |-  ( y e. ZZ -> y e. RR )
48 leneg 
 |-  ( ( y e. RR /\ A e. RR ) -> ( y <_ A <-> -u A <_ -u y ) )
49 48 adantrr 
 |-  ( ( y e. RR /\ ( A e. RR /\ x e. ZZ ) ) -> ( y <_ A <-> -u A <_ -u y ) )
50 leneg 
 |-  ( ( y e. RR /\ x e. RR ) -> ( y <_ x <-> -u x <_ -u y ) )
51 17 50 sylan2 
 |-  ( ( y e. RR /\ x e. ZZ ) -> ( y <_ x <-> -u x <_ -u y ) )
52 51 adantrl 
 |-  ( ( y e. RR /\ ( A e. RR /\ x e. ZZ ) ) -> ( y <_ x <-> -u x <_ -u y ) )
53 49 52 imbi12d 
 |-  ( ( y e. RR /\ ( A e. RR /\ x e. ZZ ) ) -> ( ( y <_ A -> y <_ x ) <-> ( -u A <_ -u y -> -u x <_ -u y ) ) )
54 47 53 sylan 
 |-  ( ( y e. ZZ /\ ( A e. RR /\ x e. ZZ ) ) -> ( ( y <_ A -> y <_ x ) <-> ( -u A <_ -u y -> -u x <_ -u y ) ) )
55 54 exbiri 
 |-  ( y e. ZZ -> ( ( A e. RR /\ x e. ZZ ) -> ( ( -u A <_ -u y -> -u x <_ -u y ) -> ( y <_ A -> y <_ x ) ) ) )
56 55 com23 
 |-  ( y e. ZZ -> ( ( -u A <_ -u y -> -u x <_ -u y ) -> ( ( A e. RR /\ x e. ZZ ) -> ( y <_ A -> y <_ x ) ) ) )
57 46 56 syld 
 |-  ( y e. ZZ -> ( A. w e. ZZ ( -u A <_ w -> -u x <_ w ) -> ( ( A e. RR /\ x e. ZZ ) -> ( y <_ A -> y <_ x ) ) ) )
58 57 com13 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( A. w e. ZZ ( -u A <_ w -> -u x <_ w ) -> ( y e. ZZ -> ( y <_ A -> y <_ x ) ) ) )
59 58 ralrimdv 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( A. w e. ZZ ( -u A <_ w -> -u x <_ w ) -> A. y e. ZZ ( y <_ A -> y <_ x ) ) )
60 40 59 impbid 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( A. y e. ZZ ( y <_ A -> y <_ x ) <-> A. w e. ZZ ( -u A <_ w -> -u x <_ w ) ) )
61 20 60 anbi12d 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) <-> ( -u A <_ -u x /\ A. w e. ZZ ( -u A <_ w -> -u x <_ w ) ) ) )
62 61 reubidva 
 |-  ( A e. RR -> ( E! x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) <-> E! x e. ZZ ( -u A <_ -u x /\ A. w e. ZZ ( -u A <_ w -> -u x <_ w ) ) ) )
63 16 62 bitr4id 
 |-  ( A e. RR -> ( E! z e. ZZ ( -u A <_ z /\ A. w e. ZZ ( -u A <_ w -> z <_ w ) ) <-> E! x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) )
64 3 63 mpbid 
 |-  ( A e. RR -> E! x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) )