This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zbtwnre

Description: There is a unique integer between a real number and the number plus one. Exercise 5 of Apostol p. 28. (Contributed by NM, 13-Nov-2004)

Ref Expression
Assertion zbtwnre ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < ( 𝐴 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 zmin ⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) )
2 zre ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
3 zre ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
4 peano2rem ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − 1 ) ∈ ℝ )
5 3 4 syl ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 − 1 ) ∈ ℝ )
6 ltletr ⊢ ( ( ( 𝑥 − 1 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 − 1 ) < 𝐴 ∧ 𝐴 ≤ 𝑦 ) → ( 𝑥 − 1 ) < 𝑦 ) )
7 5 6 syl3an1 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 − 1 ) < 𝐴 ∧ 𝐴 ≤ 𝑦 ) → ( 𝑥 − 1 ) < 𝑦 ) )
8 7 3expa ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 − 1 ) < 𝐴 ∧ 𝐴 ≤ 𝑦 ) → ( 𝑥 − 1 ) < 𝑦 ) )
9 2 8 sylan2 ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) ∧ 𝑦 ∈ ℤ ) → ( ( ( 𝑥 − 1 ) < 𝐴 ∧ 𝐴 ≤ 𝑦 ) → ( 𝑥 − 1 ) < 𝑦 ) )
10 zlem1lt ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 − 1 ) < 𝑦 ) )
11 10 adantlr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) ∧ 𝑦 ∈ ℤ ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 − 1 ) < 𝑦 ) )
12 9 11 sylibrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) ∧ 𝑦 ∈ ℤ ) → ( ( ( 𝑥 − 1 ) < 𝐴 ∧ 𝐴 ≤ 𝑦 ) → 𝑥 ≤ 𝑦 ) )
13 12 exp4b ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( 𝑦 ∈ ℤ → ( ( 𝑥 − 1 ) < 𝐴 → ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ) )
14 13 com23 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑥 − 1 ) < 𝐴 → ( 𝑦 ∈ ℤ → ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ) )
15 14 ralrimdv ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑥 − 1 ) < 𝐴 → ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) )
16 5 ltnrd ⊢ ( 𝑥 ∈ ℤ → ¬ ( 𝑥 − 1 ) < ( 𝑥 − 1 ) )
17 peano2zm ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 − 1 ) ∈ ℤ )
18 zlem1lt ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 − 1 ) ∈ ℤ ) → ( 𝑥 ≤ ( 𝑥 − 1 ) ↔ ( 𝑥 − 1 ) < ( 𝑥 − 1 ) ) )
19 17 18 mpdan ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ≤ ( 𝑥 − 1 ) ↔ ( 𝑥 − 1 ) < ( 𝑥 − 1 ) ) )
20 16 19 mtbird ⊢ ( 𝑥 ∈ ℤ → ¬ 𝑥 ≤ ( 𝑥 − 1 ) )
21 20 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) → ¬ 𝑥 ≤ ( 𝑥 − 1 ) )
22 lenlt ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 − 1 ) ∈ ℝ ) → ( 𝐴 ≤ ( 𝑥 − 1 ) ↔ ¬ ( 𝑥 − 1 ) < 𝐴 ) )
23 5 22 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → ( 𝐴 ≤ ( 𝑥 − 1 ) ↔ ¬ ( 𝑥 − 1 ) < 𝐴 ) )
24 23 ancoms ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 ≤ ( 𝑥 − 1 ) ↔ ¬ ( 𝑥 − 1 ) < 𝐴 ) )
25 24 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) → ( 𝐴 ≤ ( 𝑥 − 1 ) ↔ ¬ ( 𝑥 − 1 ) < 𝐴 ) )
26 breq2 ⊢ ( 𝑦 = ( 𝑥 − 1 ) → ( 𝐴 ≤ 𝑦 ↔ 𝐴 ≤ ( 𝑥 − 1 ) ) )
27 breq2 ⊢ ( 𝑦 = ( 𝑥 − 1 ) → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ≤ ( 𝑥 − 1 ) ) )
28 26 27 imbi12d ⊢ ( 𝑦 = ( 𝑥 − 1 ) → ( ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ↔ ( 𝐴 ≤ ( 𝑥 − 1 ) → 𝑥 ≤ ( 𝑥 − 1 ) ) ) )
29 28 rspcv ⊢ ( ( 𝑥 − 1 ) ∈ ℤ → ( ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) → ( 𝐴 ≤ ( 𝑥 − 1 ) → 𝑥 ≤ ( 𝑥 − 1 ) ) ) )
30 17 29 syl ⊢ ( 𝑥 ∈ ℤ → ( ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) → ( 𝐴 ≤ ( 𝑥 − 1 ) → 𝑥 ≤ ( 𝑥 − 1 ) ) ) )
31 30 imp ⊢ ( ( 𝑥 ∈ ℤ ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) → ( 𝐴 ≤ ( 𝑥 − 1 ) → 𝑥 ≤ ( 𝑥 − 1 ) ) )
32 31 adantlr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) → ( 𝐴 ≤ ( 𝑥 − 1 ) → 𝑥 ≤ ( 𝑥 − 1 ) ) )
33 25 32 sylbird ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) → ( ¬ ( 𝑥 − 1 ) < 𝐴 → 𝑥 ≤ ( 𝑥 − 1 ) ) )
34 21 33 mt3d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) → ( 𝑥 − 1 ) < 𝐴 )
35 34 ex ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) → ( 𝑥 − 1 ) < 𝐴 ) )
36 15 35 impbid ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑥 − 1 ) < 𝐴 ↔ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) )
37 1re ⊢ 1 ∈ ℝ
38 ltsubadd ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑥 − 1 ) < 𝐴 ↔ 𝑥 < ( 𝐴 + 1 ) ) )
39 37 38 mp3an2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑥 − 1 ) < 𝐴 ↔ 𝑥 < ( 𝐴 + 1 ) ) )
40 3 39 sylan ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑥 − 1 ) < 𝐴 ↔ 𝑥 < ( 𝐴 + 1 ) ) )
41 36 40 bitr3d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ↔ 𝑥 < ( 𝐴 + 1 ) ) )
42 41 ancoms ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → ( ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ↔ 𝑥 < ( 𝐴 + 1 ) ) )
43 42 anbi2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → ( ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ↔ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < ( 𝐴 + 1 ) ) ) )
44 43 reubidva ⊢ ( 𝐴 ∈ ℝ → ( ∃! 𝑥 ∈ ℤ ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ↔ ∃! 𝑥 ∈ ℤ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < ( 𝐴 + 1 ) ) ) )
45 1 44 mpbid ⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < ( 𝐴 + 1 ) ) )