Theorem nnsgrp

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

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

Proof

Step	Hyp	Ref	Expression
1		nnsgrp.m	$$⊢M={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{N}$$
2	1	nnsgrpmgm	$$⊢M\in \mathrm{Mgm}$$
3		nncn	$$⊢x\in \mathbb{N}\to x\in ℂ$$
4		nncn	$$⊢y\in \mathbb{N}\to y\in ℂ$$
5		nncn	$$⊢z\in \mathbb{N}\to z\in ℂ$$
6		addass	$$⊢\left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\to x+y+z=x+y+z$$
7	3 4 5 6	syl3an	$$⊢\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\wedge z\in \mathbb{N}\right)\to x+y+z=x+y+z$$
8	7	3expia	$$⊢\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\to \left(z\in \mathbb{N}\to x+y+z=x+y+z\right)$$
9	8	ralrimiv	$$⊢\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\to \forall z\in \mathbb{N}x+y+z=x+y+z$$
10	9	rgen2	$$⊢\forall x\in \mathbb{N}\forall y\in \mathbb{N}\forall z\in \mathbb{N}x+y+z=x+y+z$$
11		nnsscn	$$⊢\mathbb{N}\subseteq ℂ$$
12	1	cnfldsrngbas	$$⊢\mathbb{N}\subseteq ℂ\to \mathbb{N}={\mathrm{Base}}_M$$
13	11 12	ax-mp	$$⊢\mathbb{N}={\mathrm{Base}}_M$$
14		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
15	1	cnfldsrngadd	$$⊢\mathbb{N}\in \mathrm{V}\to +={+}_M$$
16	14 15	ax-mp	$$⊢+={+}_M$$
17	13 16	issgrp	$$⊢M\in \mathrm{Smgrp}\leftrightarrow \left(M\in \mathrm{Mgm}\wedge \forall x\in \mathbb{N}\forall y\in \mathbb{N}\forall z\in \mathbb{N}x+y+z=x+y+z\right)$$
18	2 10 17	mpbir2an	$$⊢M\in \mathrm{Smgrp}$$