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 zre ⊢ x ∈ ℤ → x ∈ ℝ
5 leneg ⊢ x ∈ ℝ ∧ A ∈ ℝ → x ≤ A ↔ − A ≤ − x
6 4 5 sylan ⊢ x ∈ ℤ ∧ A ∈ ℝ → x ≤ A ↔ − A ≤ − x
7 6 ancoms ⊢ A ∈ ℝ ∧ x ∈ ℤ → x ≤ A ↔ − A ≤ − x
8 znegcl ⊢ w ∈ ℤ → − w ∈ ℤ
9 breq1 ⊢ y = − w → y ≤ A ↔ − w ≤ A
10 breq1 ⊢ y = − w → y ≤ x ↔ − w ≤ x
11 9 10 imbi12d ⊢ y = − w → y ≤ A → y ≤ x ↔ − w ≤ A → − w ≤ x
12 11 rspcv ⊢ − w ∈ ℤ → ∀ y ∈ ℤ y ≤ A → y ≤ x → − w ≤ A → − w ≤ x
13 8 12 syl ⊢ w ∈ ℤ → ∀ y ∈ ℤ y ≤ A → y ≤ x → − w ≤ A → − w ≤ x
14 zre ⊢ w ∈ ℤ → w ∈ ℝ
15 lenegcon1 ⊢ w ∈ ℝ ∧ A ∈ ℝ → − w ≤ A ↔ − A ≤ w
16 15 adantrr ⊢ w ∈ ℝ ∧ A ∈ ℝ ∧ x ∈ ℤ → − w ≤ A ↔ − A ≤ w
17 lenegcon1 ⊢ w ∈ ℝ ∧ x ∈ ℝ → − w ≤ x ↔ − x ≤ w
18 4 17 sylan2 ⊢ w ∈ ℝ ∧ x ∈ ℤ → − w ≤ x ↔ − x ≤ w
19 18 adantrl ⊢ w ∈ ℝ ∧ A ∈ ℝ ∧ x ∈ ℤ → − w ≤ x ↔ − x ≤ w
20 16 19 imbi12d ⊢ w ∈ ℝ ∧ A ∈ ℝ ∧ x ∈ ℤ → − w ≤ A → − w ≤ x ↔ − A ≤ w → − x ≤ w
21 14 20 sylan ⊢ w ∈ ℤ ∧ A ∈ ℝ ∧ x ∈ ℤ → − w ≤ A → − w ≤ x ↔ − A ≤ w → − x ≤ w
22 21 biimpd ⊢ w ∈ ℤ ∧ A ∈ ℝ ∧ x ∈ ℤ → − w ≤ A → − w ≤ x → − A ≤ w → − x ≤ w
23 22 ex ⊢ w ∈ ℤ → A ∈ ℝ ∧ x ∈ ℤ → − w ≤ A → − w ≤ x → − A ≤ w → − x ≤ w
24 23 com23 ⊢ w ∈ ℤ → − w ≤ A → − w ≤ x → A ∈ ℝ ∧ x ∈ ℤ → − A ≤ w → − x ≤ w
25 13 24 syld ⊢ w ∈ ℤ → ∀ y ∈ ℤ y ≤ A → y ≤ x → A ∈ ℝ ∧ x ∈ ℤ → − A ≤ w → − x ≤ w
26 25 com13 ⊢ A ∈ ℝ ∧ x ∈ ℤ → ∀ y ∈ ℤ y ≤ A → y ≤ x → w ∈ ℤ → − A ≤ w → − x ≤ w
27 26 ralrimdv ⊢ A ∈ ℝ ∧ x ∈ ℤ → ∀ y ∈ ℤ y ≤ A → y ≤ x → ∀ w ∈ ℤ − A ≤ w → − x ≤ w
28 znegcl ⊢ y ∈ ℤ → − y ∈ ℤ
29 breq2 ⊢ w = − y → − A ≤ w ↔ − A ≤ − y
30 breq2 ⊢ w = − y → − x ≤ w ↔ − x ≤ − y
31 29 30 imbi12d ⊢ w = − y → − A ≤ w → − x ≤ w ↔ − A ≤ − y → − x ≤ − y
32 31 rspcv ⊢ − y ∈ ℤ → ∀ w ∈ ℤ − A ≤ w → − x ≤ w → − A ≤ − y → − x ≤ − y
33 28 32 syl ⊢ y ∈ ℤ → ∀ w ∈ ℤ − A ≤ w → − x ≤ w → − A ≤ − y → − x ≤ − y
34 zre ⊢ y ∈ ℤ → y ∈ ℝ
35 leneg ⊢ y ∈ ℝ ∧ A ∈ ℝ → y ≤ A ↔ − A ≤ − y
36 35 adantrr ⊢ y ∈ ℝ ∧ A ∈ ℝ ∧ x ∈ ℤ → y ≤ A ↔ − A ≤ − y
37 leneg ⊢ y ∈ ℝ ∧ x ∈ ℝ → y ≤ x ↔ − x ≤ − y
38 4 37 sylan2 ⊢ y ∈ ℝ ∧ x ∈ ℤ → y ≤ x ↔ − x ≤ − y
39 38 adantrl ⊢ y ∈ ℝ ∧ A ∈ ℝ ∧ x ∈ ℤ → y ≤ x ↔ − x ≤ − y
40 36 39 imbi12d ⊢ y ∈ ℝ ∧ A ∈ ℝ ∧ x ∈ ℤ → y ≤ A → y ≤ x ↔ − A ≤ − y → − x ≤ − y
41 34 40 sylan ⊢ y ∈ ℤ ∧ A ∈ ℝ ∧ x ∈ ℤ → y ≤ A → y ≤ x ↔ − A ≤ − y → − x ≤ − y
42 41 exbiri ⊢ y ∈ ℤ → A ∈ ℝ ∧ x ∈ ℤ → − A ≤ − y → − x ≤ − y → y ≤ A → y ≤ x
43 42 com23 ⊢ y ∈ ℤ → − A ≤ − y → − x ≤ − y → A ∈ ℝ ∧ x ∈ ℤ → y ≤ A → y ≤ x
44 33 43 syld ⊢ y ∈ ℤ → ∀ w ∈ ℤ − A ≤ w → − x ≤ w → A ∈ ℝ ∧ x ∈ ℤ → y ≤ A → y ≤ x
45 44 com13 ⊢ A ∈ ℝ ∧ x ∈ ℤ → ∀ w ∈ ℤ − A ≤ w → − x ≤ w → y ∈ ℤ → y ≤ A → y ≤ x
46 45 ralrimdv ⊢ A ∈ ℝ ∧ x ∈ ℤ → ∀ w ∈ ℤ − A ≤ w → − x ≤ w → ∀ y ∈ ℤ y ≤ A → y ≤ x
47 27 46 impbid ⊢ A ∈ ℝ ∧ x ∈ ℤ → ∀ y ∈ ℤ y ≤ A → y ≤ x ↔ ∀ w ∈ ℤ − A ≤ w → − x ≤ w
48 7 47 anbi12d ⊢ A ∈ ℝ ∧ x ∈ ℤ → x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x ↔ − A ≤ − x ∧ ∀ w ∈ ℤ − A ≤ w → − x ≤ w
49 48 reubidva ⊢ A ∈ ℝ → ∃! x ∈ ℤ x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x ↔ ∃! x ∈ ℤ − A ≤ − x ∧ ∀ w ∈ ℤ − A ≤ w → − x ≤ w
50 znegcl ⊢ x ∈ ℤ → − x ∈ ℤ
51 znegcl ⊢ z ∈ ℤ → − z ∈ ℤ
52 zcn ⊢ z ∈ ℤ → z ∈ ℂ
53 zcn ⊢ x ∈ ℤ → x ∈ ℂ
54 negcon2 ⊢ z ∈ ℂ ∧ x ∈ ℂ → z = − x ↔ x = − z
55 52 53 54 syl2an ⊢ z ∈ ℤ ∧ x ∈ ℤ → z = − x ↔ x = − z
56 51 55 reuhyp ⊢ z ∈ ℤ → ∃! x ∈ ℤ z = − x
57 breq2 ⊢ z = − x → − A ≤ z ↔ − A ≤ − x
58 breq1 ⊢ z = − x → z ≤ w ↔ − x ≤ w
59 58 imbi2d ⊢ z = − x → − A ≤ w → z ≤ w ↔ − A ≤ w → − x ≤ w
60 59 ralbidv ⊢ z = − x → ∀ w ∈ ℤ − A ≤ w → z ≤ w ↔ ∀ w ∈ ℤ − A ≤ w → − x ≤ w
61 57 60 anbi12d ⊢ z = − x → − A ≤ z ∧ ∀ w ∈ ℤ − A ≤ w → z ≤ w ↔ − A ≤ − x ∧ ∀ w ∈ ℤ − A ≤ w → − x ≤ w
62 50 56 61 reuxfr1 ⊢ ∃! z ∈ ℤ − A ≤ z ∧ ∀ w ∈ ℤ − A ≤ w → z ≤ w ↔ ∃! x ∈ ℤ − A ≤ − x ∧ ∀ w ∈ ℤ − A ≤ w → − x ≤ w
63 49 62 syl6rbbr ⊢ 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