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⋅ℝfld1
17 13 16 mpan ⊢n∈ℤ→ℤRHom⁡ℝfld⁡n=n⋅ℝfld1
18 1re ⊢1∈ℝ
19 remulg ⊢n∈ℤ∧1∈ℝ→n⋅ℝfld1=n⋅1
20 18 19 mpan2 ⊢n∈ℤ→n⋅ℝfld1=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