nn0omnd

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

		Ref	Expression
	Assertion	nn0omnd	⊢ ( ℂ_fld ↾_s ℕ₀ ) ∈ oMnd

Step	Hyp	Ref	Expression
1		df-refld	⊢ ℝ_fld = ( ℂ_fld ↾_s ℝ )
2	1	oveq1i	⊢ ( ℝ_fld ↾_s ℕ₀ ) = ( ( ℂ_fld ↾_s ℝ ) ↾_s ℕ₀ )
3		reex	⊢ ℝ ∈ V
4		nn0ssre	⊢ ℕ₀ ⊆ ℝ
5		ressabs	⊢ ( ( ℝ ∈ V ∧ ℕ₀ ⊆ ℝ ) → ( ( ℂ_fld ↾_s ℝ ) ↾_s ℕ₀ ) = ( ℂ_fld ↾_s ℕ₀ ) )
6	3 4 5	mp2an	⊢ ( ( ℂ_fld ↾_s ℝ ) ↾_s ℕ₀ ) = ( ℂ_fld ↾_s ℕ₀ )
7	2 6	eqtri	⊢ ( ℝ_fld ↾_s ℕ₀ ) = ( ℂ_fld ↾_s ℕ₀ )
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	⊢ ℕ₀ ∈ ( SubMnd ‘ ℂ_fld )
17		eqid	⊢ ( ℂ_fld ↾_s ℕ₀ ) = ( ℂ_fld ↾_s ℕ₀ )
18	17	submmnd	⊢ ( ℕ₀ ∈ ( SubMnd ‘ ℂ_fld ) → ( ℂ_fld ↾_s ℕ₀ ) ∈ Mnd )
19	16 18	ax-mp	⊢ ( ℂ_fld ↾_s ℕ₀ ) ∈ Mnd
20	7 19	eqeltri	⊢ ( ℝ_fld ↾_s ℕ₀ ) ∈ Mnd
21		submomnd	⊢ ( ( ℝ_fld ∈ oMnd ∧ ( ℝ_fld ↾_s ℕ₀ ) ∈ Mnd ) → ( ℝ_fld ↾_s ℕ₀ ) ∈ oMnd )
22	15 20 21	mp2an	⊢ ( ℝ_fld ↾_s ℕ₀ ) ∈ oMnd
23	7 22	eqeltrri	⊢ ( ℂ_fld ↾_s ℕ₀ ) ∈ oMnd

Metamath Proof Explorer