Metamath Proof Explorer

Theorem btwnz

Description: Any real number can be sandwiched between two integers. Exercise 2 of Apostol p. 28. (Contributed by NM, 10-Nov-2004)

Ref Expression
Assertion btwnz ⊢ A ∈ ℝ → ∃ x ∈ ℤ x < A ∧ ∃ y ∈ ℤ A < y

Proof

Step Hyp Ref Expression
1 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
2 arch ⊢ − A ∈ ℝ → ∃ z ∈ ℕ − A < z
3 1 2 syl ⊢ A ∈ ℝ → ∃ z ∈ ℕ − A < z
4 nnre ⊢ z ∈ ℕ → z ∈ ℝ
5 ltnegcon1 ⊢ A ∈ ℝ ∧ z ∈ ℝ → − A < z ↔ − z < A
6 5 ex ⊢ A ∈ ℝ → z ∈ ℝ → − A < z ↔ − z < A
7 4 6 syl5 ⊢ A ∈ ℝ → z ∈ ℕ → − A < z ↔ − z < A
8 7 pm5.32d ⊢ A ∈ ℝ → z ∈ ℕ ∧ − A < z ↔ z ∈ ℕ ∧ − z < A
9 nnnegz ⊢ z ∈ ℕ → − z ∈ ℤ
10 breq1 ⊢ x = − z → x < A ↔ − z < A
11 10 rspcev ⊢ − z ∈ ℤ ∧ − z < A → ∃ x ∈ ℤ x < A
12 9 11 sylan ⊢ z ∈ ℕ ∧ − z < A → ∃ x ∈ ℤ x < A
13 8 12 biimtrdi ⊢ A ∈ ℝ → z ∈ ℕ ∧ − A < z → ∃ x ∈ ℤ x < A
14 13 expd ⊢ A ∈ ℝ → z ∈ ℕ → − A < z → ∃ x ∈ ℤ x < A
15 14 rexlimdv ⊢ A ∈ ℝ → ∃ z ∈ ℕ − A < z → ∃ x ∈ ℤ x < A
16 3 15 mpd ⊢ A ∈ ℝ → ∃ x ∈ ℤ x < A
17 arch ⊢ A ∈ ℝ → ∃ y ∈ ℕ A < y
18 nnz ⊢ y ∈ ℕ → y ∈ ℤ
19 18 anim1i ⊢ y ∈ ℕ ∧ A < y → y ∈ ℤ ∧ A < y
20 19 reximi2 ⊢ ∃ y ∈ ℕ A < y → ∃ y ∈ ℤ A < y
21 17 20 syl ⊢ A ∈ ℝ → ∃ y ∈ ℤ A < y
22 16 21 jca ⊢ A ∈ ℝ → ∃ x ∈ ℤ x < A ∧ ∃ y ∈ ℤ A < y