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	$⊢ A \in ℂ \to \exists x \in ℂ A + x = 0$

Proof

Step	Hyp	Ref	Expression
1		cnre	$⊢ A \in ℂ \to \exists a \in ℝ \exists b \in ℝ A = a + i b$
2		ax-rnegex	$⊢ a \in ℝ \to \exists c \in ℝ a + c = 0$
3		ax-rnegex	$⊢ b \in ℝ \to \exists d \in ℝ b + d = 0$
4	2 3	anim12i	$⊢ (a \in ℝ \land b \in ℝ) \to (\exists c \in ℝ a + c = 0 \land \exists d \in ℝ b + d = 0)$
5		reeanv	$⊢ \exists c \in ℝ \exists d \in ℝ (a + c = 0 \land b + d = 0) \leftrightarrow (\exists c \in ℝ a + c = 0 \land \exists d \in ℝ b + d = 0)$
6	4 5	sylibr	$⊢ (a \in ℝ \land b \in ℝ) \to \exists c \in ℝ \exists d \in ℝ (a + c = 0 \land b + d = 0)$
7		ax-icn	$⊢ i \in ℂ$
8	7	a1i	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to i \in ℂ$
9		simplrr	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to d \in ℝ$
10	9	recnd	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to d \in ℂ$
11	8 10	mulcld	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to i d \in ℂ$
12		simplrl	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to c \in ℝ$
13	12	recnd	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to c \in ℂ$
14	11 13	addcld	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to i d + c \in ℂ$
15		simplll	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a \in ℝ$
16	15	recnd	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a \in ℂ$
17		simpllr	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to b \in ℝ$
18	17	recnd	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to b \in ℂ$
19	8 18	mulcld	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to i b \in ℂ$
20	16 19 11	addassd	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a + i b + i d = a + i b + i d$
21	8 18 10	adddid	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to i (b + d) = i b + i d$
22		simprr	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to b + d = 0$
23	22	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to i (b + d) = i \cdot 0$
24		mul01	$⊢ i \in ℂ \to i \cdot 0 = 0$
25	7 24	ax-mp	$⊢ i \cdot 0 = 0$
26	23 25	syl6eq	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to i (b + d) = 0$
27	21 26	eqtr3d	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to i b + i d = 0$
28	27	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a + i b + i d = a + 0$
29		addid1	$⊢ a \in ℂ \to a + 0 = a$
30	16 29	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a + 0 = a$
31	20 28 30	3eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a + i b + i d = a$
32	31	oveq1d	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to (a + i b) + i d + c = a + c$
33	16 19	addcld	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a + i b \in ℂ$
34	33 11 13	addassd	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to (a + i b) + i d + c = a + i b + i d + c$
35	32 34	eqtr3d	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a + c = a + i b + i d + c$
36		simprl	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a + c = 0$
37	35 36	eqtr3d	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to a + i b + i d + c = 0$
38		oveq2	$⊢ x = i d + c \to a + i b + x = a + i b + i d + c$
39	38	eqeq1d	$⊢ x = i d + c \to (a + i b + x = 0 \leftrightarrow a + i b + i d + c = 0)$
40	39	rspcev	$⊢ (i d + c \in ℂ \land a + i b + i d + c = 0) \to \exists x \in ℂ a + i b + x = 0$
41	14 37 40	syl2anc	$⊢ (((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \land (a + c = 0 \land b + d = 0)) \to \exists x \in ℂ a + i b + x = 0$
42	41	ex	$⊢ ((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \to ((a + c = 0 \land b + d = 0) \to \exists x \in ℂ a + i b + x = 0)$
43	42	rexlimdvva	$⊢ (a \in ℝ \land b \in ℝ) \to (\exists c \in ℝ \exists d \in ℝ (a + c = 0 \land b + d = 0) \to \exists x \in ℂ a + i b + x = 0)$
44	6 43	mpd	$⊢ (a \in ℝ \land b \in ℝ) \to \exists x \in ℂ a + i b + x = 0$
45		oveq1	$⊢ A = a + i b \to A + x = a + i b + x$
46	45	eqeq1d	$⊢ A = a + i b \to (A + x = 0 \leftrightarrow a + i b + x = 0)$
47	46	rexbidv	$⊢ A = a + i b \to (\exists x \in ℂ A + x = 0 \leftrightarrow \exists x \in ℂ a + i b + x = 0)$
48	44 47	syl5ibrcom	$⊢ (a \in ℝ \land b \in ℝ) \to (A = a + i b \to \exists x \in ℂ A + x = 0)$
49	48	rexlimivv	$⊢ \exists a \in ℝ \exists b \in ℝ A = a + i b \to \exists x \in ℂ A + x = 0$
50	1 49	syl	$⊢ A \in ℂ \to \exists x \in ℂ A + x = 0$

Metamath Proof Explorer

Theorem cnegex

Proof