Theorem nn0mnd

Description: The set of nonnegative integers under (complex) addition is a monoid. Example in Lang p. 6. Remark: M could have also been written as ` ( CCfld |``s NN0 ) ` . (Contributed by AV, 27-Dec-2023)

	Ref	Expression
Hypothesis	nn0mnd.g	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathbb{N}}_0⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}$$
Assertion	nn0mnd	$$⊢M\in \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		nn0mnd.g	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathbb{N}}_0⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}$$
2		nn0addcl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to x+y\in {\mathbb{N}}_0$$
3		nn0cn	$$⊢x\in {\mathbb{N}}_0\to x\in ℂ$$
4		nn0cn	$$⊢y\in {\mathbb{N}}_0\to y\in ℂ$$
5		nn0cn	$$⊢z\in {\mathbb{N}}_0\to z\in ℂ$$
6	3 4 5	3anim123i	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\to \left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)$$
7	6	3expa	$$⊢\left(\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\wedge z\in {\mathbb{N}}_0\right)\to \left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)$$
8		addass	$$⊢\left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\to x+y+z=x+y+z$$
9	7 8	syl	$$⊢\left(\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\wedge z\in {\mathbb{N}}_0\right)\to x+y+z=x+y+z$$
10	9	ralrimiva	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to \forall z\in {\mathbb{N}}_{0}x+y+z=x+y+z$$
11	2 10	jca	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to \left(x+y\in {\mathbb{N}}_0\wedge \forall z\in {\mathbb{N}}_{0}x+y+z=x+y+z\right)$$
12	11	rgen2	$$⊢\forall x\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_0\left(x+y\in {\mathbb{N}}_0\wedge \forall z\in {\mathbb{N}}_{0}x+y+z=x+y+z\right)$$
13		c0ex	$$⊢0\in \mathrm{V}$$
14		eleq1	$$⊢e=0\to \left(e\in {\mathbb{N}}_0\leftrightarrow 0\in {\mathbb{N}}_0\right)$$
15		oveq1	$$⊢e=0\to e+x=0+x$$
16	15	eqeq1d	$$⊢e=0\to \left(e+x=x\leftrightarrow 0+x=x\right)$$
17		oveq2	$$⊢e=0\to x+e=x+0$$
18	17	eqeq1d	$$⊢e=0\to \left(x+e=x\leftrightarrow x+0=x\right)$$
19	16 18	anbi12d	$$⊢e=0\to \left(\left(e+x=x\wedge x+e=x\right)\leftrightarrow \left(0+x=x\wedge x+0=x\right)\right)$$
20	19	ralbidv	$$⊢e=0\to \left(\forall x\in {\mathbb{N}}_0\left(e+x=x\wedge x+e=x\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(0+x=x\wedge x+0=x\right)\right)$$
21	14 20	anbi12d	$$⊢e=0\to \left(\left(e\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_0\left(e+x=x\wedge x+e=x\right)\right)\leftrightarrow \left(0\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_0\left(0+x=x\wedge x+0=x\right)\right)\right)$$
22		0nn0	$$⊢0\in {\mathbb{N}}_0$$
23	3	addlidd	$$⊢x\in {\mathbb{N}}_0\to 0+x=x$$
24	3	addridd	$$⊢x\in {\mathbb{N}}_0\to x+0=x$$
25	23 24	jca	$$⊢x\in {\mathbb{N}}_0\to \left(0+x=x\wedge x+0=x\right)$$
26	25	rgen	$$⊢\forall x\in {\mathbb{N}}_0\left(0+x=x\wedge x+0=x\right)$$
27	22 26	pm3.2i	$$⊢\left(0\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_0\left(0+x=x\wedge x+0=x\right)\right)$$
28	13 21 27	ceqsexv2d	$$⊢\exists e\left(e\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_0\left(e+x=x\wedge x+e=x\right)\right)$$
29		df-rex	$$⊢\exists e\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(e+x=x\wedge x+e=x\right)\leftrightarrow \exists e\left(e\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_0\left(e+x=x\wedge x+e=x\right)\right)$$
30	28 29	mpbir	$$⊢\exists e\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(e+x=x\wedge x+e=x\right)$$
31	12 30	pm3.2i	$$⊢\left(\forall x\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_0\left(x+y\in {\mathbb{N}}_0\wedge \forall z\in {\mathbb{N}}_{0}x+y+z=x+y+z\right)\wedge \exists e\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(e+x=x\wedge x+e=x\right)\right)$$
32		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
33	1	grpbase	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to {\mathbb{N}}_0={\mathrm{Base}}_M$$
34	32 33	ax-mp	$$⊢{\mathbb{N}}_0={\mathrm{Base}}_M$$
35		addex	$$⊢+\in \mathrm{V}$$
36	1	grpplusg	$$⊢+\in \mathrm{V}\to +={+}_M$$
37	35 36	ax-mp	$$⊢+={+}_M$$
38	34 37	ismnd	$$⊢M\in \mathrm{Mnd}\leftrightarrow \left(\forall x\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_0\left(x+y\in {\mathbb{N}}_0\wedge \forall z\in {\mathbb{N}}_{0}x+y+z=x+y+z\right)\wedge \exists e\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(e+x=x\wedge x+e=x\right)\right)$$
39	31 38	mpbir	$$⊢M\in \mathrm{Mnd}$$