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