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 = ( CCfld |`s NN )
Assertion	nnsgrpmgm	|- M e. Mgm

Proof

Step	Hyp	Ref	Expression
1		nnsgrp.m	|- M = ( CCfld |`s NN )
2		1nn	|- 1 e. NN
3		nnaddcl	|- ( ( x e. NN /\ y e. NN ) -> ( x + y ) e. NN )
4	3	rgen2	|- A. x e. NN A. y e. NN ( x + y ) e. NN
5		nnsscn	|- NN C_ CC
6	1	cnfldsrngbas	|- ( NN C_ CC -> NN = ( Base ` M ) )
7	5 6	ax-mp	|- NN = ( Base ` M )
8		nnex	|- NN e. _V
9	1	cnfldsrngadd	|- ( NN e. _V -> + = ( +g ` M ) )
10	8 9	ax-mp	|- + = ( +g ` M )
11	7 10	ismgmn0	|- ( 1 e. NN -> ( M e. Mgm <-> A. x e. NN A. y e. NN ( x + y ) e. NN ) )
12	4 11	mpbiri	|- ( 1 e. NN -> M e. Mgm )
13	2 12	ax-mp	|- M e. Mgm