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