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 ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ ∀ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥 ) ) )

Proof

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