Metamath Proof Explorer


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 = fld 𝑠
Assertion nnsgrp Could not format assertion : No typesetting found for |- M e. Smgrp with typecode |-

Proof

Step Hyp Ref Expression
1 nnsgrp.m M = fld 𝑠
2 1 nnsgrpmgm M Mgm
3 nncn x x
4 nncn y y
5 nncn z z
6 addass x y z x + y + z = x + y + z
7 3 4 5 6 syl3an x y z x + y + z = x + y + z
8 7 3expia x y z x + y + z = x + y + z
9 8 ralrimiv x y z x + y + z = x + y + z
10 9 rgen2 x y z x + y + z = x + y + z
11 nnsscn
12 1 cnfldsrngbas = Base M
13 11 12 ax-mp = Base M
14 nnex V
15 1 cnfldsrngadd V + = + M
16 14 15 ax-mp + = + M
17 13 16 issgrp Could not format ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. NN A. y e. NN A. z e. NN ( ( x + y ) + z ) = ( x + ( y + z ) ) ) ) : No typesetting found for |- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. NN A. y e. NN A. z e. NN ( ( x + y ) + z ) = ( x + ( y + z ) ) ) ) with typecode |-
18 2 10 17 mpbir2an Could not format M e. Smgrp : No typesetting found for |- M e. Smgrp with typecode |-