Theorem cnegex2

Description: Existence of a left inverse for addition. (Contributed by Scott Fenton, 3-Jan-2013)

	Ref	Expression
Assertion	cnegex2	$$⊢A\in ℂ\to \exists x\in ℂx+A=0$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2	1 1	mulcli	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
3		mulcl	$$⊢\left(\mathrm{i}\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}\mathrm{i}A\in ℂ$$
4	2 3	mpan	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}A\in ℂ$$
5		mullid	$$⊢A\in ℂ\to 1A=A$$
6	5	oveq2d	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}A+1A=\mathrm{i}\mathrm{i}A+A$$
7		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
8	7	oveq1i	$$⊢\left(\mathrm{i}\mathrm{i}+1\right)A=0\cdot A$$
9		ax-1cn	$$⊢1\in ℂ$$
10		adddir	$$⊢\left(\mathrm{i}\mathrm{i}\in ℂ\wedge 1\in ℂ\wedge A\in ℂ\right)\to \left(\mathrm{i}\mathrm{i}+1\right)A=\mathrm{i}\mathrm{i}A+1A$$
11	2 9 10	mp3an12	$$⊢A\in ℂ\to \left(\mathrm{i}\mathrm{i}+1\right)A=\mathrm{i}\mathrm{i}A+1A$$
12		mul02	$$⊢A\in ℂ\to 0\cdot A=0$$
13	8 11 12	3eqtr3a	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}A+1A=0$$
14	6 13	eqtr3d	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}A+A=0$$
15		oveq1	$$⊢x=\mathrm{i}\mathrm{i}A\to x+A=\mathrm{i}\mathrm{i}A+A$$
16	15	eqeq1d	$$⊢x=\mathrm{i}\mathrm{i}A\to \left(x+A=0\leftrightarrow \mathrm{i}\mathrm{i}A+A=0\right)$$
17	16	rspcev	$$⊢\left(\mathrm{i}\mathrm{i}A\in ℂ\wedge \mathrm{i}\mathrm{i}A+A=0\right)\to \exists x\in ℂx+A=0$$
18	4 14 17	syl2anc	$$⊢A\in ℂ\to \exists x\in ℂx+A=0$$