This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mullid ⊢ ( 𝐴 ∈ ℂ → ( 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 )