Theorem nn0srg

Description: The nonnegative integers form a semiring (commutative by subcmn ). (Contributed by Thierry Arnoux, 1-May-2018)

	Ref	Expression
Assertion	nn0srg	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{SRing}$$

Proof

Step	Hyp	Ref	Expression
1		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
2		ringcmn	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
3	1 2	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
4		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
5		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
6	5	submcmn	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}\wedge {\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}$$
7	3 4 6	mp2an	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}$$
8		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
9		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
10	5 9	mgpress	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={\mathrm{mulGrp}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
11	3 8 10	mp2an	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={\mathrm{mulGrp}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
12		nn0sscn	$$⊢{\mathbb{N}}_0\subseteq ℂ$$
13		1nn0	$$⊢1\in {\mathbb{N}}_0$$
14		nn0mulcl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to xy\in {\mathbb{N}}_0$$
15	14	rgen2	$$⊢\forall x\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_{0}xy\in {\mathbb{N}}_0$$
16	9	ringmgp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
17	1 16	ax-mp	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
18		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
19	9 18	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
20		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
21	9 20	ringidval	$$⊢1=0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
22		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
23	9 22	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
24	19 21 23	issubm	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\to \left({\mathbb{N}}_0\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\leftrightarrow \left({\mathbb{N}}_0\subseteq ℂ\wedge 1\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_{0}xy\in {\mathbb{N}}_0\right)\right)$$
25	17 24	ax-mp	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\leftrightarrow \left({\mathbb{N}}_0\subseteq ℂ\wedge 1\in {\mathbb{N}}_0\wedge \forall x\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_{0}xy\in {\mathbb{N}}_0\right)$$
26	12 13 15 25	mpbir3an	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
27		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
28	27	submmnd	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
29	26 28	ax-mp	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
30	11 29	eqeltrri	$$⊢{\mathrm{mulGrp}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}\in \mathrm{Mnd}$$
31		simpl	$$⊢\left(x\in {\mathbb{N}}_0\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to x\in {\mathbb{N}}_0$$
32	31	nn0cnd	$$⊢\left(x\in {\mathbb{N}}_0\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to x\in ℂ$$
33		simprl	$$⊢\left(x\in {\mathbb{N}}_0\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to y\in {\mathbb{N}}_0$$
34	33	nn0cnd	$$⊢\left(x\in {\mathbb{N}}_0\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to y\in ℂ$$
35		simprr	$$⊢\left(x\in {\mathbb{N}}_0\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to z\in {\mathbb{N}}_0$$
36	35	nn0cnd	$$⊢\left(x\in {\mathbb{N}}_0\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to z\in ℂ$$
37	32 34 36	adddid	$$⊢\left(x\in {\mathbb{N}}_0\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to x\left(y+z\right)=xy+xz$$
38	32 34 36	adddird	$$⊢\left(x\in {\mathbb{N}}_0\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to \left(x+y\right)z=xz+yz$$
39	37 38	jca	$$⊢\left(x\in {\mathbb{N}}_0\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to \left(x\left(y+z\right)=xy+xz\wedge \left(x+y\right)z=xz+yz\right)$$
40	39	ralrimivva	$$⊢x\in {\mathbb{N}}_0\to \forall y\in {\mathbb{N}}_0\forall z\in {\mathbb{N}}_0\left(x\left(y+z\right)=xy+xz\wedge \left(x+y\right)z=xz+yz\right)$$
41		nn0cn	$$⊢x\in {\mathbb{N}}_0\to x\in ℂ$$
42	41	mul02d	$$⊢x\in {\mathbb{N}}_0\to 0\cdot x=0$$
43	41	mul01d	$$⊢x\in {\mathbb{N}}_0\to x\cdot 0=0$$
44	40 42 43	jca32	$$⊢x\in {\mathbb{N}}_0\to \left(\forall y\in {\mathbb{N}}_0\forall z\in {\mathbb{N}}_0\left(x\left(y+z\right)=xy+xz\wedge \left(x+y\right)z=xz+yz\right)\wedge \left(0\cdot x=0\wedge x\cdot 0=0\right)\right)$$
45	44	rgen	$$⊢\forall x\in {\mathbb{N}}_0\left(\forall y\in {\mathbb{N}}_0\forall z\in {\mathbb{N}}_0\left(x\left(y+z\right)=xy+xz\wedge \left(x+y\right)z=xz+yz\right)\wedge \left(0\cdot x=0\wedge x\cdot 0=0\right)\right)$$
46	5 18	ressbas2	$$⊢{\mathbb{N}}_0\subseteq ℂ\to {\mathbb{N}}_0={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
47	12 46	ax-mp	$$⊢{\mathbb{N}}_0={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
48		eqid	$$⊢{\mathrm{mulGrp}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}={\mathrm{mulGrp}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
49		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
50	5 49	ressplusg	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to +={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
51	8 50	ax-mp	$$⊢+={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
52	5 22	ressmulr	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to \times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
53	8 52	ax-mp	$$⊢\times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
54		ringmnd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
55	1 54	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
56		0nn0	$$⊢0\in {\mathbb{N}}_0$$
57		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
58	5 18 57	ress0g	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge 0\in {\mathbb{N}}_0\wedge {\mathbb{N}}_0\subseteq ℂ\right)\to 0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
59	55 56 12 58	mp3an	$$⊢0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
60	47 48 51 53 59	issrg	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{SRing}\leftrightarrow \left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}\wedge {\mathrm{mulGrp}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}\in \mathrm{Mnd}\wedge \forall x\in {\mathbb{N}}_0\left(\forall y\in {\mathbb{N}}_0\forall z\in {\mathbb{N}}_0\left(x\left(y+z\right)=xy+xz\wedge \left(x+y\right)z=xz+yz\right)\wedge \left(0\cdot x=0\wedge x\cdot 0=0\right)\right)\right)$$
61	7 30 45 60	mpbir3an	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{SRing}$$