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={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{N}$$
Assertion	nnsgrpnmnd	$$⊢M\notin \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		nnsgrp.m	$$⊢M={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{N}$$
2		nnsscn	$$⊢\mathbb{N}\subseteq ℂ$$
3	1	cnfldsrngbas	$$⊢\mathbb{N}\subseteq ℂ\to \mathbb{N}={\mathrm{Base}}_M$$
4	2 3	ax-mp	$$⊢\mathbb{N}={\mathrm{Base}}_M$$
5		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
6	1	cnfldsrngadd	$$⊢\mathbb{N}\in \mathrm{V}\to +={+}_M$$
7	5 6	ax-mp	$$⊢+={+}_M$$
8	4 7	isnmnd	$$⊢\forall z\in \mathbb{N}\exists x\in \mathbb{N}z+x\ne x\to M\notin \mathrm{Mnd}$$
9		1nn	$$⊢1\in \mathbb{N}$$
10	9	a1i	$$⊢z\in \mathbb{N}\to 1\in \mathbb{N}$$
11		oveq2	$$⊢x=1\to z+x=z+1$$
12		id	$$⊢x=1\to x=1$$
13	11 12	neeq12d	$$⊢x=1\to \left(z+x\ne x\leftrightarrow z+1\ne 1\right)$$
14	13	adantl	$$⊢\left(z\in \mathbb{N}\wedge x=1\right)\to \left(z+x\ne x\leftrightarrow z+1\ne 1\right)$$
15		nnne0	$$⊢z\in \mathbb{N}\to z\ne 0$$
16	15	necomd	$$⊢z\in \mathbb{N}\to 0\ne z$$
17		1cnd	$$⊢z\in \mathbb{N}\to 1\in ℂ$$
18		nncn	$$⊢z\in \mathbb{N}\to z\in ℂ$$
19	17 17 18	subadd2d	$$⊢z\in \mathbb{N}\to \left(1-1=z\leftrightarrow z+1=1\right)$$
20		1m1e0	$$⊢1-1=0$$
21	20	a1i	$$⊢z\in \mathbb{N}\to 1-1=0$$
22	21	eqeq1d	$$⊢z\in \mathbb{N}\to \left(1-1=z\leftrightarrow 0=z\right)$$
23	19 22	bitr3d	$$⊢z\in \mathbb{N}\to \left(z+1=1\leftrightarrow 0=z\right)$$
24	23	necon3bid	$$⊢z\in \mathbb{N}\to \left(z+1\ne 1\leftrightarrow 0\ne z\right)$$
25	16 24	mpbird	$$⊢z\in \mathbb{N}\to z+1\ne 1$$
26	10 14 25	rspcedvd	$$⊢z\in \mathbb{N}\to \exists x\in \mathbb{N}z+x\ne x$$
27	8 26	mprg	$$⊢M\notin \mathrm{Mnd}$$