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$

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

Metamath Proof Explorer