Theorem cnegex2

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

	Ref	Expression
Assertion	cnegex2	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( 𝑥 + 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2	1 1	mulcli	⊢ ( i · i ) ∈ ℂ
3		mulcl	⊢ ( ( ( i · i ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( i · i ) · 𝐴 ) ∈ ℂ )
4	2 3	mpan	⊢ ( 𝐴 ∈ ℂ → ( ( i · i ) · 𝐴 ) ∈ ℂ )
5		mulid2	⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
6	5	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · i ) · 𝐴 ) + ( 1 · 𝐴 ) ) = ( ( ( i · i ) · 𝐴 ) + 𝐴 ) )
7		ax-i2m1	⊢ ( ( i · i ) + 1 ) = 0
8	7	oveq1i	⊢ ( ( ( i · i ) + 1 ) · 𝐴 ) = ( 0 · 𝐴 )
9		ax-1cn	⊢ 1 ∈ ℂ
10		adddir	⊢ ( ( ( i · i ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( ( i · i ) + 1 ) · 𝐴 ) = ( ( ( i · i ) · 𝐴 ) + ( 1 · 𝐴 ) ) )
11	2 9 10	mp3an12	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · i ) + 1 ) · 𝐴 ) = ( ( ( i · i ) · 𝐴 ) + ( 1 · 𝐴 ) ) )
12		mul02	⊢ ( 𝐴 ∈ ℂ → ( 0 · 𝐴 ) = 0 )
13	8 11 12	3eqtr3a	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · i ) · 𝐴 ) + ( 1 · 𝐴 ) ) = 0 )
14	6 13	eqtr3d	⊢ ( 𝐴 ∈ ℂ → ( ( ( i · i ) · 𝐴 ) + 𝐴 ) = 0 )
15		oveq1	⊢ ( 𝑥 = ( ( i · i ) · 𝐴 ) → ( 𝑥 + 𝐴 ) = ( ( ( i · i ) · 𝐴 ) + 𝐴 ) )
16	15	eqeq1d	⊢ ( 𝑥 = ( ( i · i ) · 𝐴 ) → ( ( 𝑥 + 𝐴 ) = 0 ↔ ( ( ( i · i ) · 𝐴 ) + 𝐴 ) = 0 ) )
17	16	rspcev	⊢ ( ( ( ( i · i ) · 𝐴 ) ∈ ℂ ∧ ( ( ( i · i ) · 𝐴 ) + 𝐴 ) = 0 ) → ∃ 𝑥 ∈ ℂ ( 𝑥 + 𝐴 ) = 0 )
18	4 14 17	syl2anc	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( 𝑥 + 𝐴 ) = 0 )