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

Proof

Step Hyp Ref Expression
1 nnsgrp.m 
 |-  M = ( CCfld |`s NN )
2 1 nnsgrpmgm 
 |-  M e. Mgm
3 nncn 
 |-  ( x e. NN -> x e. CC )
4 nncn 
 |-  ( y e. NN -> y e. CC )
5 nncn 
 |-  ( z e. NN -> z e. CC )
6 addass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
7 3 4 5 6 syl3an 
 |-  ( ( x e. NN /\ y e. NN /\ z e. NN ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
8 7 3expia 
 |-  ( ( x e. NN /\ y e. NN ) -> ( z e. NN -> ( ( x + y ) + z ) = ( x + ( y + z ) ) ) )
9 8 ralrimiv 
 |-  ( ( x e. NN /\ y e. NN ) -> A. z e. NN ( ( x + y ) + z ) = ( x + ( y + z ) ) )
10 9 rgen2 
 |-  A. x e. NN A. y e. NN A. z e. NN ( ( x + y ) + z ) = ( x + ( y + z ) )
11 nnsscn 
 |-  NN C_ CC
12 1 cnfldsrngbas 
 |-  ( NN C_ CC -> NN = ( Base ` M ) )
13 11 12 ax-mp 
 |-  NN = ( Base ` M )
14 nnex 
 |-  NN e. _V
15 1 cnfldsrngadd 
 |-  ( NN e. _V -> + = ( +g ` M ) )
16 14 15 ax-mp 
 |-  + = ( +g ` M )
17 13 16 issgrp 
 |-  ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. NN A. y e. NN A. z e. NN ( ( x + y ) + z ) = ( x + ( y + z ) ) ) )
18 2 10 17 mpbir2an 
 |-  M e. Smgrp