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

Metamath Proof Explorer

Theorem nn0archi

Description: The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018)

Ref Expression
Assertion nn0archi ( ℂfld ↾s ℕ0 ) ∈ Archi

Proof

Step Hyp Ref Expression
1 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
2 1 oveq1i ⊢ ( ℝfld ↾s ℕ0 ) = ( ( ℂfld ↾s ℝ ) ↾s ℕ0 )
3 resubdrg ⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
4 3 simpli ⊢ ℝ ∈ ( SubRing ‘ ℂfld )
5 nn0ssre ⊢ ℕ0 ⊆ ℝ
6 ressabs ⊢ ( ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℕ0 ⊆ ℝ ) → ( ( ℂfld ↾s ℝ ) ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 ) )
7 4 5 6 mp2an ⊢ ( ( ℂfld ↾s ℝ ) ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
8 2 7 eqtri ⊢ ( ℝfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
9 retos ⊢ ℝfld ∈ Toset
10 rearchi ⊢ ℝfld ∈ Archi
11 9 10 pm3.2i ⊢ ( ℝfld ∈ Toset ∧ ℝfld ∈ Archi )
12 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
13 subrgsubg ⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝ ∈ ( SubGrp ‘ ℂfld ) )
14 subgsubm ⊢ ( ℝ ∈ ( SubGrp ‘ ℂfld ) → ℝ ∈ ( SubMnd ‘ ℂfld ) )
15 4 13 14 mp2b ⊢ ℝ ∈ ( SubMnd ‘ ℂfld )
16 1 subsubm ⊢ ( ℝ ∈ ( SubMnd ‘ ℂfld ) → ( ℕ0 ∈ ( SubMnd ‘ ℝfld ) ↔ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) ∧ ℕ0 ⊆ ℝ ) ) )
17 15 16 ax-mp ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℝfld ) ↔ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) ∧ ℕ0 ⊆ ℝ ) )
18 12 5 17 mpbir2an ⊢ ℕ0 ∈ ( SubMnd ‘ ℝfld )
19 submarchi ⊢ ( ( ( ℝfld ∈ Toset ∧ ℝfld ∈ Archi ) ∧ ℕ0 ∈ ( SubMnd ‘ ℝfld ) ) → ( ℝfld ↾s ℕ0 ) ∈ Archi )
20 11 18 19 mp2an ⊢ ( ℝfld ↾s ℕ0 ) ∈ Archi
21 8 20 eqeltrri ⊢ ( ℂfld ↾s ℕ0 ) ∈ Archi