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 ⊢ A ∈ ℝ → ∃ n ∈ ℕ A < n

Proof

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