Theorem nnsgrpmgm

Description: The structure of positive integers together with the addition of complex numbers is a magma. (Contributed by AV, 4-Feb-2020)

	Ref	Expression
Hypothesis	nnsgrp.m	$$⊢M={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{N}$$
Assertion	nnsgrpmgm	$$⊢M\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		nnsgrp.m	$$⊢M={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{N}$$
2		1nn	$$⊢1\in \mathbb{N}$$
3		nnaddcl	$$⊢\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\to x+y\in \mathbb{N}$$
4	3	rgen2	$$⊢\forall x\in \mathbb{N}\forall y\in \mathbb{N}x+y\in \mathbb{N}$$
5		nnsscn	$$⊢\mathbb{N}\subseteq ℂ$$
6	1	cnfldsrngbas	$$⊢\mathbb{N}\subseteq ℂ\to \mathbb{N}={\mathrm{Base}}_M$$
7	5 6	ax-mp	$$⊢\mathbb{N}={\mathrm{Base}}_M$$
8		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
9	1	cnfldsrngadd	$$⊢\mathbb{N}\in \mathrm{V}\to +={+}_M$$
10	8 9	ax-mp	$$⊢+={+}_M$$
11	7 10	ismgmn0	$$⊢1\in \mathbb{N}\to \left(M\in \mathrm{Mgm}\leftrightarrow \forall x\in \mathbb{N}\forall y\in \mathbb{N}x+y\in \mathbb{N}\right)$$
12	4 11	mpbiri	$$⊢1\in \mathbb{N}\to M\in \mathrm{Mgm}$$
13	2 12	ax-mp	$$⊢M\in \mathrm{Mgm}$$