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 ∃! x x A y y A y x

Proof

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