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 ( 𝐴 ∈ ℝ → ( ∃ 𝑥 ∈ ℤ 𝑥 < 𝐴 ∧ ∃ 𝑦 ∈ ℤ 𝐴 < 𝑦 ) )

Proof

Step Hyp Ref Expression
1 renegcl ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
2 arch ( - 𝐴 ∈ ℝ → ∃ 𝑧 ∈ ℕ - 𝐴 < 𝑧 )
3 1 2 syl ( 𝐴 ∈ ℝ → ∃ 𝑧 ∈ ℕ - 𝐴 < 𝑧 )
4 nnre ( 𝑧 ∈ ℕ → 𝑧 ∈ ℝ )
5 ltnegcon1 ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( - 𝐴 < 𝑧 ↔ - 𝑧 < 𝐴 ) )
6 5 ex ( 𝐴 ∈ ℝ → ( 𝑧 ∈ ℝ → ( - 𝐴 < 𝑧 ↔ - 𝑧 < 𝐴 ) ) )
7 4 6 syl5 ( 𝐴 ∈ ℝ → ( 𝑧 ∈ ℕ → ( - 𝐴 < 𝑧 ↔ - 𝑧 < 𝐴 ) ) )
8 7 pm5.32d ( 𝐴 ∈ ℝ → ( ( 𝑧 ∈ ℕ ∧ - 𝐴 < 𝑧 ) ↔ ( 𝑧 ∈ ℕ ∧ - 𝑧 < 𝐴 ) ) )
9 nnnegz ( 𝑧 ∈ ℕ → - 𝑧 ∈ ℤ )
10 breq1 ( 𝑥 = - 𝑧 → ( 𝑥 < 𝐴 ↔ - 𝑧 < 𝐴 ) )
11 10 rspcev ( ( - 𝑧 ∈ ℤ ∧ - 𝑧 < 𝐴 ) → ∃ 𝑥 ∈ ℤ 𝑥 < 𝐴 )
12 9 11 sylan ( ( 𝑧 ∈ ℕ ∧ - 𝑧 < 𝐴 ) → ∃ 𝑥 ∈ ℤ 𝑥 < 𝐴 )
13 8 12 syl6bi ( 𝐴 ∈ ℝ → ( ( 𝑧 ∈ ℕ ∧ - 𝐴 < 𝑧 ) → ∃ 𝑥 ∈ ℤ 𝑥 < 𝐴 ) )
14 13 expd ( 𝐴 ∈ ℝ → ( 𝑧 ∈ ℕ → ( - 𝐴 < 𝑧 → ∃ 𝑥 ∈ ℤ 𝑥 < 𝐴 ) ) )
15 14 rexlimdv ( 𝐴 ∈ ℝ → ( ∃ 𝑧 ∈ ℕ - 𝐴 < 𝑧 → ∃ 𝑥 ∈ ℤ 𝑥 < 𝐴 ) )
16 3 15 mpd ( 𝐴 ∈ ℝ → ∃ 𝑥 ∈ ℤ 𝑥 < 𝐴 )
17 arch ( 𝐴 ∈ ℝ → ∃ 𝑦 ∈ ℕ 𝐴 < 𝑦 )
18 nnz ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
19 18 anim1i ( ( 𝑦 ∈ ℕ ∧ 𝐴 < 𝑦 ) → ( 𝑦 ∈ ℤ ∧ 𝐴 < 𝑦 ) )
20 19 reximi2 ( ∃ 𝑦 ∈ ℕ 𝐴 < 𝑦 → ∃ 𝑦 ∈ ℤ 𝐴 < 𝑦 )
21 17 20 syl ( 𝐴 ∈ ℝ → ∃ 𝑦 ∈ ℤ 𝐴 < 𝑦 )
22 16 21 jca ( 𝐴 ∈ ℝ → ( ∃ 𝑥 ∈ ℤ 𝑥 < 𝐴 ∧ ∃ 𝑦 ∈ ℤ 𝐴 < 𝑦 ) )