Theorem sn-addid2

Description: addid2 without ax-mulcom . (Contributed by SN, 23-Jan-2024)

	Ref	Expression
Assertion	sn-addid2	$$⊢A\in ℂ\to 0+A=A$$

Proof

Step	Hyp	Ref	Expression
1		cnre	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$
2		0cnd	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to 0\in ℂ$$
3		simp2l	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to x\in ℝ$$
4	3	recnd	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to x\in ℂ$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6	5	a1i	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to \mathrm{i}\in ℂ$$
7		simp2r	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to y\in ℝ$$
8	7	recnd	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to y\in ℂ$$
9	6 8	mulcld	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to \mathrm{i}y\in ℂ$$
10	2 4 9	addassd	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to 0+x+\mathrm{i}y=0+x+\mathrm{i}y$$
11		readdid2	$$⊢x\in ℝ\to 0+x=x$$
12	11	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0+x=x$$
13	12	3ad2ant2	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to 0+x=x$$
14	13	oveq1d	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to 0+x+\mathrm{i}y=x+\mathrm{i}y$$
15	10 14	eqtr3d	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to 0+x+\mathrm{i}y=x+\mathrm{i}y$$
16		simp3	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to A=x+\mathrm{i}y$$
17	16	oveq2d	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to 0+A=0+x+\mathrm{i}y$$
18	15 17 16	3eqtr4d	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\wedge A=x+\mathrm{i}y\right)\to 0+A=A$$
19	18	3exp	$$⊢A\in ℂ\to \left(\left(x\in ℝ\wedge y\in ℝ\right)\to \left(A=x+\mathrm{i}y\to 0+A=A\right)\right)$$
20	19	rexlimdvv	$$⊢A\in ℂ\to \left(\exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y\to 0+A=A\right)$$
21	1 20	mpd	$$⊢A\in ℂ\to 0+A=A$$