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

Metamath Proof Explorer

Theorem arch

Description: Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of Apostol p. 26. (Contributed by NM, 21-Jan-1997)

Ref Expression
Assertion arch ( 𝐴 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝐴 < 𝑛 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 < 𝑛 ↔ 𝐴 < 𝑛 ) )
2 1 rexbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 ↔ ∃ 𝑛 ∈ ℕ 𝐴 < 𝑛 ) )
3 nnunb ⊢ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 )
4 ralnex ⊢ ( ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) ↔ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
5 3 4 mpbir ⊢ ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 )
6 rexnal ⊢ ( ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) ↔ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
7 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
8 axlttri ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 𝑦 < 𝑛 ↔ ¬ ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ) )
9 7 8 sylan2 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < 𝑛 ↔ ¬ ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ) )
10 equcom ⊢ ( 𝑦 = 𝑛 ↔ 𝑛 = 𝑦 )
11 10 orbi1i ⊢ ( ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ↔ ( 𝑛 = 𝑦 ∨ 𝑛 < 𝑦 ) )
12 orcom ⊢ ( ( 𝑛 = 𝑦 ∨ 𝑛 < 𝑦 ) ↔ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
13 11 12 bitri ⊢ ( ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ↔ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
14 13 notbii ⊢ ( ¬ ( 𝑦 = 𝑛 ∨ 𝑛 < 𝑦 ) ↔ ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) )
15 9 14 bitrdi ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < 𝑛 ↔ ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) ) )
16 15 biimprd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) → 𝑦 < 𝑛 ) )
17 16 reximdva ⊢ ( 𝑦 ∈ ℝ → ( ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 ) )
18 6 17 biimtrrid ⊢ ( 𝑦 ∈ ℝ → ( ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 ) )
19 18 ralimia ⊢ ( ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦 ∨ 𝑛 = 𝑦 ) → ∀ 𝑦 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 )
20 5 19 ax-mp ⊢ ∀ 𝑦 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛
21 2 20 vtoclri ⊢ ( 𝐴 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝐴 < 𝑛 )