Metamath Proof Explorer

Theorem rebtwnz

Description: There is a unique greatest integer less than or equal to a real number. Exercise 4 of Apostol p. 28. (Contributed by NM, 15-Nov-2004)

Ref Expression
Assertion rebtwnz ⊢ A ∈ ℝ → ∃! x ∈ ℤ x ≤ A ∧ A < x + 1

Proof

Step Hyp Ref Expression
1 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
2 zbtwnre ⊢ − A ∈ ℝ → ∃! y ∈ ℤ − A ≤ y ∧ y < - A + 1
3 1 2 syl ⊢ A ∈ ℝ → ∃! y ∈ ℤ − A ≤ y ∧ y < - A + 1
4 znegcl ⊢ x ∈ ℤ → − x ∈ ℤ
5 znegcl ⊢ y ∈ ℤ → − y ∈ ℤ
6 zcn ⊢ y ∈ ℤ → y ∈ ℂ
7 zcn ⊢ x ∈ ℤ → x ∈ ℂ
8 negcon2 ⊢ y ∈ ℂ ∧ x ∈ ℂ → y = − x ↔ x = − y
9 6 7 8 syl2an ⊢ y ∈ ℤ ∧ x ∈ ℤ → y = − x ↔ x = − y
10 5 9 reuhyp ⊢ y ∈ ℤ → ∃! x ∈ ℤ y = − x
11 breq2 ⊢ y = − x → − A ≤ y ↔ − A ≤ − x
12 breq1 ⊢ y = − x → y < - A + 1 ↔ − x < - A + 1
13 11 12 anbi12d ⊢ y = − x → − A ≤ y ∧ y < - A + 1 ↔ − A ≤ − x ∧ − x < - A + 1
14 4 10 13 reuxfr1 ⊢ ∃! y ∈ ℤ − A ≤ y ∧ y < - A + 1 ↔ ∃! x ∈ ℤ − A ≤ − x ∧ − x < - A + 1
15 zre ⊢ x ∈ ℤ → x ∈ ℝ
16 leneg ⊢ x ∈ ℝ ∧ A ∈ ℝ → x ≤ A ↔ − A ≤ − x
17 16 ancoms ⊢ A ∈ ℝ ∧ x ∈ ℝ → x ≤ A ↔ − A ≤ − x
18 peano2rem ⊢ A ∈ ℝ → A − 1 ∈ ℝ
19 ltneg ⊢ A − 1 ∈ ℝ ∧ x ∈ ℝ → A − 1 < x ↔ − x < − A − 1
20 18 19 sylan ⊢ A ∈ ℝ ∧ x ∈ ℝ → A − 1 < x ↔ − x < − A − 1
21 1re ⊢ 1 ∈ ℝ
22 ltsubadd ⊢ A ∈ ℝ ∧ 1 ∈ ℝ ∧ x ∈ ℝ → A − 1 < x ↔ A < x + 1
23 21 22 mp3an2 ⊢ A ∈ ℝ ∧ x ∈ ℝ → A − 1 < x ↔ A < x + 1
24 recn ⊢ A ∈ ℝ → A ∈ ℂ
25 ax-1cn ⊢ 1 ∈ ℂ
26 negsubdi ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → − A − 1 = - A + 1
27 24 25 26 sylancl ⊢ A ∈ ℝ → − A − 1 = - A + 1
28 27 adantr ⊢ A ∈ ℝ ∧ x ∈ ℝ → − A − 1 = - A + 1
29 28 breq2d ⊢ A ∈ ℝ ∧ x ∈ ℝ → − x < − A − 1 ↔ − x < - A + 1
30 20 23 29 3bitr3d ⊢ A ∈ ℝ ∧ x ∈ ℝ → A < x + 1 ↔ − x < - A + 1
31 17 30 anbi12d ⊢ A ∈ ℝ ∧ x ∈ ℝ → x ≤ A ∧ A < x + 1 ↔ − A ≤ − x ∧ − x < - A + 1
32 15 31 sylan2 ⊢ A ∈ ℝ ∧ x ∈ ℤ → x ≤ A ∧ A < x + 1 ↔ − A ≤ − x ∧ − x < - A + 1
33 32 bicomd ⊢ A ∈ ℝ ∧ x ∈ ℤ → − A ≤ − x ∧ − x < - A + 1 ↔ x ≤ A ∧ A < x + 1
34 33 reubidva ⊢ A ∈ ℝ → ∃! x ∈ ℤ − A ≤ − x ∧ − x < - A + 1 ↔ ∃! x ∈ ℤ x ≤ A ∧ A < x + 1
35 14 34 bitrid ⊢ A ∈ ℝ → ∃! y ∈ ℤ − A ≤ y ∧ y < - A + 1 ↔ ∃! x ∈ ℤ x ≤ A ∧ A < x + 1
36 3 35 mpbid ⊢ A ∈ ℝ → ∃! x ∈ ℤ x ≤ A ∧ A < x + 1