This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ < = ( lt ‘ ℝfld )
5 2 3 4 isarchiofld ⊢ ( ℝfld ∈ oField → ( ℝfld ∈ Archi ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) ) )
6 1 5 ax-mp ⊢ ( ℝfld ∈ Archi ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℕ 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) )
7 arch ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 )
8 nnz ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
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 ⊢ ( .g ‘ ℝfld ) = ( .g ‘ ℝfld )
15 re1r ⊢ 1 = ( 1r ‘ ℝfld )
16 3 14 15 zrhmulg ⊢ ( ( ℝfld ∈ Ring ∧ 𝑛 ∈ ℤ ) → ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) = ( 𝑛 ( .g ‘ ℝfld ) 1 ) )
17 13 16 mpan ⊢ ( 𝑛 ∈ ℤ → ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) = ( 𝑛 ( .g ‘ ℝfld ) 1 ) )
18 1re ⊢ 1 ∈ ℝ
19 remulg ⊢ ( ( 𝑛 ∈ ℤ ∧ 1 ∈ ℝ ) → ( 𝑛 ( .g ‘ ℝfld ) 1 ) = ( 𝑛 · 1 ) )
20 18 19 mpan2 ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ( .g ‘ ℝfld ) 1 ) = ( 𝑛 · 1 ) )
21 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
22 21 mulridd ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · 1 ) = 𝑛 )
23 17 20 22 3eqtrd ⊢ ( 𝑛 ∈ ℤ → ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) = 𝑛 )
24 23 breq2d ⊢ ( 𝑛 ∈ ℤ → ( 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) ↔ 𝑥 < 𝑛 ) )
25 8 24 syl ⊢ ( 𝑛 ∈ ℕ → ( 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) ↔ 𝑥 < 𝑛 ) )
26 25 rexbiia ⊢ ( ∃ 𝑛 ∈ ℕ 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 )
27 7 26 sylibr ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝑥 < ( ( ℤRHom ‘ ℝfld ) ‘ 𝑛 ) )
28 6 27 mprgbir ⊢ ℝfld ∈ Archi