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 syl6bi ⊢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