Metamath Proof Explorer


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 = fld 𝑠
Assertion nnsgrpmgm M Mgm

Proof

Step Hyp Ref Expression
1 nnsgrp.m M = fld 𝑠
2 1nn 1
3 nnaddcl x y x + y
4 3 rgen2 x y x + y
5 nnsscn
6 1 cnfldsrngbas = Base M
7 5 6 ax-mp = Base M
8 nnex V
9 1 cnfldsrngadd V + = + M
10 8 9 ax-mp + = + M
11 7 10 ismgmn0 1 M Mgm x y x + y
12 4 11 mpbiri 1 M Mgm
13 2 12 ax-mp M Mgm