Theorem 2zrng0

Description: The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020)

	Ref	Expression
Hypotheses	2zrng.e	$$⊢E=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}$$
	2zrngbas.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}E$$
Assertion	2zrng0	$$⊢0=0_R$$

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	$$⊢E=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}$$
2		2zrngbas.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}E$$
3		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
4		crngring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
5		ringmnd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
6	3 4 5	mp2b	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
7	1	0even	$$⊢0\in E$$
8		ssrab2	$$⊢\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\subseteq \mathbb{Z}$$
9	1 8	eqsstri	$$⊢E\subseteq \mathbb{Z}$$
10		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
11	9 10	sstri	$$⊢E\subseteq ℂ$$
12		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
13		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
14	2 12 13	ress0g	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge 0\in E\wedge E\subseteq ℂ\right)\to 0=0_R$$
15	6 7 11 14	mp3an	$$⊢0=0_R$$