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 addrid ⊢ ( 𝑎 ∈ ℂ → ( 𝑎 + 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 )