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