Theorem oddiadd

Description: Lemma 2 for oddinmgm : The group addition operation of M is the addition of complex numbers. (Contributed by AV, 3-Feb-2020)

	Ref	Expression
Hypotheses	oddinmgm.e	$$⊢O=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x+1\right\}$$
	oddinmgm.r	$$⊢M={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}O$$
Assertion	oddiadd	$$⊢+={+}_M$$

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	$$⊢O=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x+1\right\}$$
2		oddinmgm.r	$$⊢M={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}O$$
3		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
4	1 3	rabex2	$$⊢O\in \mathrm{V}$$
5	2	cnfldsrngadd	$$⊢O\in \mathrm{V}\to +={+}_M$$
6	4 5	ax-mp	$$⊢+={+}_M$$