Metamath Proof Explorer

Theorem nn0omnd

Description: The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Assertion nn0omnd ⊢ ℂ fld ↾ 𝑠 ℕ 0 ∈ oMnd

Proof

Step Hyp Ref Expression
1 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
2 1 oveq1i ⊢ ℝ fld ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℝ ↾ 𝑠 ℕ 0
3 reex ⊢ ℝ ∈ V
4 nn0ssre ⊢ ℕ 0 ⊆ ℝ
5 ressabs ⊢ ℝ ∈ V ∧ ℕ 0 ⊆ ℝ → ℂ fld ↾ 𝑠 ℝ ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℕ 0
6 3 4 5 mp2an ⊢ ℂ fld ↾ 𝑠 ℝ ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℕ 0
7 2 6 eqtri ⊢ ℝ fld ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℕ 0
8 reofld ⊢ ℝ fld ∈ oField
9 isofld ⊢ ℝ fld ∈ oField ↔ ℝ fld ∈ Field ∧ ℝ fld ∈ oRing
10 9 simprbi ⊢ ℝ fld ∈ oField → ℝ fld ∈ oRing
11 orngogrp ⊢ ℝ fld ∈ oRing → ℝ fld ∈ oGrp
12 isogrp ⊢ ℝ fld ∈ oGrp ↔ ℝ fld ∈ Grp ∧ ℝ fld ∈ oMnd
13 12 simprbi ⊢ ℝ fld ∈ oGrp → ℝ fld ∈ oMnd
14 10 11 13 3syl ⊢ ℝ fld ∈ oField → ℝ fld ∈ oMnd
15 8 14 ax-mp ⊢ ℝ fld ∈ oMnd
16 nn0subm ⊢ ℕ 0 ∈ SubMnd ⁡ ℂ fld
17 eqid ⊢ ℂ fld ↾ 𝑠 ℕ 0 = ℂ fld ↾ 𝑠 ℕ 0
18 17 submmnd ⊢ ℕ 0 ∈ SubMnd ⁡ ℂ fld → ℂ fld ↾ 𝑠 ℕ 0 ∈ Mnd
19 16 18 ax-mp ⊢ ℂ fld ↾ 𝑠 ℕ 0 ∈ Mnd
20 7 19 eqeltri ⊢ ℝ fld ↾ 𝑠 ℕ 0 ∈ Mnd
21 submomnd ⊢ ℝ fld ∈ oMnd ∧ ℝ fld ↾ 𝑠 ℕ 0 ∈ Mnd → ℝ fld ↾ 𝑠 ℕ 0 ∈ oMnd
22 15 20 21 mp2an ⊢ ℝ fld ↾ 𝑠 ℕ 0 ∈ oMnd
23 7 22 eqeltrri ⊢ ℂ fld ↾ 𝑠 ℕ 0 ∈ oMnd