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 ⊢ A ∈ ℝ → ∃! x ∈ ℤ A ≤ x ∧ x < A + 1

Proof

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