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

Proof

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