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 ↾ 𝑠 ℕ 0 ∈ Archi

Proof

Step Hyp Ref Expression
1 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
2 1 oveq1i ⊢ ℝ fld ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℝ ↾ 𝑠 ℕ 0
3 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
4 3 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
5 nn0ssre ⊢ ℕ 0 ⊆ ℝ
6 ressabs ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℕ 0 ⊆ ℝ → ℂ fld ↾ 𝑠 ℝ ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℕ 0
7 4 5 6 mp2an ⊢ ℂ fld ↾ 𝑠 ℝ ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℕ 0
8 2 7 eqtri ⊢ ℝ fld ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℕ 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 ↾ 𝑠 ℕ 0 ∈ Archi
20 11 18 19 mp2an ⊢ ℝ fld ↾ 𝑠 ℕ 0 ∈ Archi
21 8 20 eqeltrri ⊢ ℂ fld ↾ 𝑠 ℕ 0 ∈ Archi