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 syl5bir ( 𝑦 ∈ ℝ → ( ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦𝑛 = 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 ) )
19 18 ralimia ( ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑦𝑛 = 𝑦 ) → ∀ 𝑦 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛 )
20 5 19 ax-mp 𝑦 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑦 < 𝑛
21 2 20 vtoclri ( 𝐴 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝐴 < 𝑛 )