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 )