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

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