Theorem nnsgrpnmnd

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

	Ref	Expression
Hypothesis	nnsgrp.m	|- M = ( CCfld |`s NN )
Assertion	nnsgrpnmnd	|- M e/ Mnd

Proof

Step	Hyp	Ref	Expression
1		nnsgrp.m	|- M = ( CCfld |`s NN )
2		nnsscn	|- NN C_ CC
3	1	cnfldsrngbas	|- ( NN C_ CC -> NN = ( Base ` M ) )
4	2 3	ax-mp	|- NN = ( Base ` M )
5		nnex	|- NN e. _V
6	1	cnfldsrngadd	|- ( NN e. _V -> + = ( +g ` M ) )
7	5 6	ax-mp	|- + = ( +g ` M )
8	4 7	isnmnd	|- ( A. z e. NN E. x e. NN ( z + x ) =/= x -> M e/ Mnd )
9		1nn	|- 1 e. NN
10	9	a1i	|- ( z e. NN -> 1 e. NN )
11		oveq2	|- ( x = 1 -> ( z + x ) = ( z + 1 ) )
12		id	|- ( x = 1 -> x = 1 )
13	11 12	neeq12d	|- ( x = 1 -> ( ( z + x ) =/= x <-> ( z + 1 ) =/= 1 ) )
14	13	adantl	|- ( ( z e. NN /\ x = 1 ) -> ( ( z + x ) =/= x <-> ( z + 1 ) =/= 1 ) )
15		nnne0	|- ( z e. NN -> z =/= 0 )
16	15	necomd	|- ( z e. NN -> 0 =/= z )
17		1cnd	|- ( z e. NN -> 1 e. CC )
18		nncn	|- ( z e. NN -> z e. CC )
19	17 17 18	subadd2d	|- ( z e. NN -> ( ( 1 - 1 ) = z <-> ( z + 1 ) = 1 ) )
20		1m1e0	|- ( 1 - 1 ) = 0
21	20	a1i	|- ( z e. NN -> ( 1 - 1 ) = 0 )
22	21	eqeq1d	|- ( z e. NN -> ( ( 1 - 1 ) = z <-> 0 = z ) )
23	19 22	bitr3d	|- ( z e. NN -> ( ( z + 1 ) = 1 <-> 0 = z ) )
24	23	necon3bid	|- ( z e. NN -> ( ( z + 1 ) =/= 1 <-> 0 =/= z ) )
25	16 24	mpbird	|- ( z e. NN -> ( z + 1 ) =/= 1 )
26	10 14 25	rspcedvd	|- ( z e. NN -> E. x e. NN ( z + x ) =/= x )
27	8 26	mprg	|- M e/ Mnd