Theorem addid2

Description: 0 is a left identity for addition. This used to be one of our complex number axioms, until it was discovered that it was dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cnegex	$$⊢A\in ℂ\to \exists x\in ℂA+x=0$$
2		cnegex	$$⊢x\in ℂ\to \exists y\in ℂx+y=0$$
3	2	ad2antrl	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\right)\to \exists y\in ℂx+y=0$$
4		0cn	$$⊢0\in ℂ$$
5		addass	$$⊢\left(0\in ℂ\wedge 0\in ℂ\wedge y\in ℂ\right)\to 0+0+y=0+0+y$$
6	4 4 5	mp3an12	$$⊢y\in ℂ\to 0+0+y=0+0+y$$
7	6	adantr	$$⊢\left(y\in ℂ\wedge x+y=0\right)\to 0+0+y=0+0+y$$
8	7	3ad2ant3	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to 0+0+y=0+0+y$$
9		00id	$$⊢0+0=0$$
10	9	oveq1i	$$⊢0+0+y=0+y$$
11		simp1	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to A\in ℂ$$
12		simp2l	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to x\in ℂ$$
13		simp3l	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to y\in ℂ$$
14	11 12 13	addassd	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to A+x+y=A+x+y$$
15		simp2r	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to A+x=0$$
16	15	oveq1d	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to A+x+y=0+y$$
17		simp3r	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to x+y=0$$
18	17	oveq2d	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to A+x+y=A+0$$
19	14 16 18	3eqtr3rd	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to A+0=0+y$$
20		addid1	$$⊢A\in ℂ\to A+0=A$$
21	20	3ad2ant1	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to A+0=A$$
22	19 21	eqtr3d	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to 0+y=A$$
23	10 22	eqtrid	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to 0+0+y=A$$
24	22	oveq2d	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to 0+0+y=0+A$$
25	8 23 24	3eqtr3rd	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\wedge \left(y\in ℂ\wedge x+y=0\right)\right)\to 0+A=A$$
26	25	3expia	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\right)\to \left(\left(y\in ℂ\wedge x+y=0\right)\to 0+A=A\right)$$
27	26	expd	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\right)\to \left(y\in ℂ\to \left(x+y=0\to 0+A=A\right)\right)$$
28	27	rexlimdv	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\right)\to \left(\exists y\in ℂx+y=0\to 0+A=A\right)$$
29	3 28	mpd	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge A+x=0\right)\right)\to 0+A=A$$
30	1 29	rexlimddv	$$⊢A\in ℂ\to 0+A=A$$