Metamath Proof Explorer


Theorem cnegex

Description: Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007) (Revised by Scott Fenton, 3-Jan-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 cnre ( 𝐴 ∈ ℂ → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝐴 = ( 𝑎 + ( i · 𝑏 ) ) )
2 ax-rnegex ( 𝑎 ∈ ℝ → ∃ 𝑐 ∈ ℝ ( 𝑎 + 𝑐 ) = 0 )
3 ax-rnegex ( 𝑏 ∈ ℝ → ∃ 𝑑 ∈ ℝ ( 𝑏 + 𝑑 ) = 0 )
4 2 3 anim12i ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ( 𝑎 + 𝑐 ) = 0 ∧ ∃ 𝑑 ∈ ℝ ( 𝑏 + 𝑑 ) = 0 ) )
5 reeanv ( ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ↔ ( ∃ 𝑐 ∈ ℝ ( 𝑎 + 𝑐 ) = 0 ∧ ∃ 𝑑 ∈ ℝ ( 𝑏 + 𝑑 ) = 0 ) )
6 4 5 sylibr ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) )
7 ax-icn i ∈ ℂ
8 7 a1i ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → i ∈ ℂ )
9 simplrr ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → 𝑑 ∈ ℝ )
10 9 recnd ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → 𝑑 ∈ ℂ )
11 8 10 mulcld ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( i · 𝑑 ) ∈ ℂ )
12 simplrl ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → 𝑐 ∈ ℝ )
13 12 recnd ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → 𝑐 ∈ ℂ )
14 11 13 addcld ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( ( i · 𝑑 ) + 𝑐 ) ∈ ℂ )
15 simplll ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → 𝑎 ∈ ℝ )
16 15 recnd ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → 𝑎 ∈ ℂ )
17 simpllr ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → 𝑏 ∈ ℝ )
18 17 recnd ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → 𝑏 ∈ ℂ )
19 8 18 mulcld ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( i · 𝑏 ) ∈ ℂ )
20 16 19 11 addassd ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( ( 𝑎 + ( i · 𝑏 ) ) + ( i · 𝑑 ) ) = ( 𝑎 + ( ( i · 𝑏 ) + ( i · 𝑑 ) ) ) )
21 8 18 10 adddid ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( i · ( 𝑏 + 𝑑 ) ) = ( ( i · 𝑏 ) + ( i · 𝑑 ) ) )
22 simprr ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( 𝑏 + 𝑑 ) = 0 )
23 22 oveq2d ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( i · ( 𝑏 + 𝑑 ) ) = ( i · 0 ) )
24 mul01 ( i ∈ ℂ → ( i · 0 ) = 0 )
25 7 24 ax-mp ( i · 0 ) = 0
26 23 25 eqtrdi ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( i · ( 𝑏 + 𝑑 ) ) = 0 )
27 21 26 eqtr3d ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( ( i · 𝑏 ) + ( i · 𝑑 ) ) = 0 )
28 27 oveq2d ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( 𝑎 + ( ( i · 𝑏 ) + ( i · 𝑑 ) ) ) = ( 𝑎 + 0 ) )
29 addid1 ( 𝑎 ∈ ℂ → ( 𝑎 + 0 ) = 𝑎 )
30 16 29 syl ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( 𝑎 + 0 ) = 𝑎 )
31 20 28 30 3eqtrd ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( ( 𝑎 + ( i · 𝑏 ) ) + ( i · 𝑑 ) ) = 𝑎 )
32 31 oveq1d ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( ( ( 𝑎 + ( i · 𝑏 ) ) + ( i · 𝑑 ) ) + 𝑐 ) = ( 𝑎 + 𝑐 ) )
33 16 19 addcld ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( 𝑎 + ( i · 𝑏 ) ) ∈ ℂ )
34 33 11 13 addassd ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( ( ( 𝑎 + ( i · 𝑏 ) ) + ( i · 𝑑 ) ) + 𝑐 ) = ( ( 𝑎 + ( i · 𝑏 ) ) + ( ( i · 𝑑 ) + 𝑐 ) ) )
35 32 34 eqtr3d ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( 𝑎 + 𝑐 ) = ( ( 𝑎 + ( i · 𝑏 ) ) + ( ( i · 𝑑 ) + 𝑐 ) ) )
36 simprl ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( 𝑎 + 𝑐 ) = 0 )
37 35 36 eqtr3d ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ( ( 𝑎 + ( i · 𝑏 ) ) + ( ( i · 𝑑 ) + 𝑐 ) ) = 0 )
38 oveq2 ( 𝑥 = ( ( i · 𝑑 ) + 𝑐 ) → ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) = ( ( 𝑎 + ( i · 𝑏 ) ) + ( ( i · 𝑑 ) + 𝑐 ) ) )
39 38 eqeq1d ( 𝑥 = ( ( i · 𝑑 ) + 𝑐 ) → ( ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) = 0 ↔ ( ( 𝑎 + ( i · 𝑏 ) ) + ( ( i · 𝑑 ) + 𝑐 ) ) = 0 ) )
40 39 rspcev ( ( ( ( i · 𝑑 ) + 𝑐 ) ∈ ℂ ∧ ( ( 𝑎 + ( i · 𝑏 ) ) + ( ( i · 𝑑 ) + 𝑐 ) ) = 0 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) = 0 )
41 14 37 40 syl2anc ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) ) → ∃ 𝑥 ∈ ℂ ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) = 0 )
42 41 ex ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) = 0 ) )
43 42 rexlimdvva ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( ( 𝑎 + 𝑐 ) = 0 ∧ ( 𝑏 + 𝑑 ) = 0 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) = 0 ) )
44 6 43 mpd ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ∃ 𝑥 ∈ ℂ ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) = 0 )
45 oveq1 ( 𝐴 = ( 𝑎 + ( i · 𝑏 ) ) → ( 𝐴 + 𝑥 ) = ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) )
46 45 eqeq1d ( 𝐴 = ( 𝑎 + ( i · 𝑏 ) ) → ( ( 𝐴 + 𝑥 ) = 0 ↔ ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) = 0 ) )
47 46 rexbidv ( 𝐴 = ( 𝑎 + ( i · 𝑏 ) ) → ( ∃ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 ↔ ∃ 𝑥 ∈ ℂ ( ( 𝑎 + ( i · 𝑏 ) ) + 𝑥 ) = 0 ) )
48 44 47 syl5ibrcom ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝐴 = ( 𝑎 + ( i · 𝑏 ) ) → ∃ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 ) )
49 48 rexlimivv ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝐴 = ( 𝑎 + ( i · 𝑏 ) ) → ∃ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 )
50 1 49 syl ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 )