Metamath Proof Explorer

Theorem rearchi

Description: The field of the real numbers is Archimedean. See also arch . (Contributed by Thierry Arnoux, 9-Apr-2018)

Ref Expression
Assertion rearchi ⊢ ℝ fld ∈ Archi

Proof

Step Hyp Ref Expression
1 reofld ⊢ ℝ fld ∈ oField
2 rebase ⊢ ℝ = Base ℝ fld
3 eqid ⊢ ℤRHom ⁡ ℝ fld = ℤRHom ⁡ ℝ fld
4 relt ⊢ < = < ℝ fld
5 2 3 4 isarchiofld ⊢ ℝ fld ∈ oField → ℝ fld ∈ Archi ↔ ∀ x ∈ ℝ ∃ n ∈ ℕ x < ℤRHom ⁡ ℝ fld ⁡ n
6 1 5 ax-mp ⊢ ℝ fld ∈ Archi ↔ ∀ x ∈ ℝ ∃ n ∈ ℕ x < ℤRHom ⁡ ℝ fld ⁡ n
7 arch ⊢ x ∈ ℝ → ∃ n ∈ ℕ x < n
8 nnz ⊢ n ∈ ℕ → n ∈ ℤ
9 refld ⊢ ℝ fld ∈ Field
10 isfld ⊢ ℝ fld ∈ Field ↔ ℝ fld ∈ DivRing ∧ ℝ fld ∈ CRing
11 10 simplbi ⊢ ℝ fld ∈ Field → ℝ fld ∈ DivRing
12 drngring ⊢ ℝ fld ∈ DivRing → ℝ fld ∈ Ring
13 9 11 12 mp2b ⊢ ℝ fld ∈ Ring
14 eqid ⊢ ⋅ ℝ fld = ⋅ ℝ fld
15 re1r ⊢ 1 = 1 ℝ fld
16 3 14 15 zrhmulg ⊢ ℝ fld ∈ Ring ∧ n ∈ ℤ → ℤRHom ⁡ ℝ fld ⁡ n = n ⋅ ℝ fld 1
17 13 16 mpan ⊢ n ∈ ℤ → ℤRHom ⁡ ℝ fld ⁡ n = n ⋅ ℝ fld 1
18 1re ⊢ 1 ∈ ℝ
19 remulg ⊢ n ∈ ℤ ∧ 1 ∈ ℝ → n ⋅ ℝ fld 1 = n ⋅ 1
20 18 19 mpan2 ⊢ n ∈ ℤ → n ⋅ ℝ fld 1 = n ⋅ 1
21 zcn ⊢ n ∈ ℤ → n ∈ ℂ
22 21 mulridd ⊢ n ∈ ℤ → n ⋅ 1 = n
23 17 20 22 3eqtrd ⊢ n ∈ ℤ → ℤRHom ⁡ ℝ fld ⁡ n = n
24 23 breq2d ⊢ n ∈ ℤ → x < ℤRHom ⁡ ℝ fld ⁡ n ↔ x < n
25 8 24 syl ⊢ n ∈ ℕ → x < ℤRHom ⁡ ℝ fld ⁡ n ↔ x < n
26 25 rexbiia ⊢ ∃ n ∈ ℕ x < ℤRHom ⁡ ℝ fld ⁡ n ↔ ∃ n ∈ ℕ x < n
27 7 26 sylibr ⊢ x ∈ ℝ → ∃ n ∈ ℕ x < ℤRHom ⁡ ℝ fld ⁡ n
28 6 27 mprgbir ⊢ ℝ fld ∈ Archi