Theorem cnegext 5348

Description: Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007.)

Assertion

Ref	Expression
cnegext	|- (A e. CC -> E.x e. CC (A + x) = 0)

Distinct variable group:   x,A

Proof of Theorem cnegext

Step	Hyp	Ref	Expression
1		axcnre 5286	. 2 |- (A e. CC -> E.a e. RR E.b e. RR A = (a + (i x. b)))
2		opreq1 3968	. . . . . 6 |- (A = (a + (i x. b)) -> (A + x) = ((a + (i x. b)) + x))
3	2	eqeq1d 1483	. . . . 5 |- (A = (a + (i x. b)) -> ((A + x) = 0 <-> ((a + (i x. b)) + x) = 0))
4	3	rexbidv 1664	. . . 4 |- (A = (a + (i x. b)) -> (E.x e. CC (A + x) = 0 <-> E.x e. CC ((a + (i x. b)) + x) = 0))
5		cnegextlem2 5346	. . . . 5 |- E.y e. RR (i x. y) e. RR
6		cnegextlem3 5347	. . . . . . . . 9 |- ((b e. RR /\ y e. RR) -> E.c e. RR (b + c) = y)
7	6	ad2ant2lr 410	. . . . . . . 8 |- (((a e. RR /\ b e. RR) /\ (y e. RR /\ (i x. y) e. RR)) -> E.c e. RR (b + c) = y)
8		axaddrcl 5272	. . . . . . . . . . . . . 14 |- ((a e. RR /\ (i x. y) e. RR) -> (a + (i x. y)) e. RR)
9		axrnegex 5283	. . . . . . . . . . . . . 14 |- ((a + (i x. y)) e. RR -> E.d e. RR ((a + (i x. y)) + d) = 0)
10	8, 9	syl 10	. . . . . . . . . . . . 13 |- ((a e. RR /\ (i x. y) e. RR) -> E.d e. RR ((a + (i x. y)) + d) = 0)
11	10	ad2ant2rl 411	. . . . . . . . . . . 12 |- (((a e. RR /\ b e. RR) /\ (y e. RR /\ (i x. y) e. RR)) -> E.d e. RR ((a + (i x. y)) + d) = 0)
12	11	adantr 389	. . . . . . . . . . 11 |- ((((a e. RR /\ b e. RR) /\ (y e. RR /\ (i x. y) e. RR)) /\ (c e. RR /\ (b + c) = y)) -> E.d e. RR ((a + (i x. y)) + d) = 0)
13		opreq2 3969	. . . . . . . . . . . . . . . 16 |- (x = ((i x. c) + d) -> ((a + (i x. b)) + x) = ((a + (i x. b)) + ((i x. c) + d)))
14	13	eqeq1d 1483	. . . . . . . . . . . . . . 15 |- (x = ((i x. c) + d) -> (((a + (i x. b)) + x) = 0 <-> ((a + (i x. b)) + ((i x. c) + d)) = 0))
15	14	rcla4ev 1877	. . . . . . . . . . . . . 14 |- ((((i x. c) + d) e. CC /\ ((a + (i x. b)) + ((i x. c) + d)) = 0) -> E.x e. CC ((a + (i x. b)) + x) = 0)
16		axaddcl 5271	. . . . . . . . . . . . . . . . . 18 |- (((i x. c) e. CC /\ d e. CC) -> ((i x. c) + d) e. CC)
17		recnt 5313	. . . . . . . . . . . . . . . . . . 19 |- (c e. RR -> c e. CC)
18		axicn 5270	. . . . . . . . . . . . . . . . . . . 20 |- i e. CC
19		axmulcl 5273	. . . . . . . . . . . . . . . . . . . 20 |- ((i e. CC /\ c e. CC) -> (i x. c) e. CC)
20	18, 19	mpan 695	. . . . . . . . . . . . . . . . . . 19 |- (c e. CC -> (i x. c) e. CC)
21	17, 20	syl 10	. . . . . . . . . . . . . . . . . 18 |- (c e. RR -> (i x. c) e. CC)
22		recnt 5313	. . . . . . . . . . . . . . . . . 18 |- (d e. RR -> d e. CC)
23	16, 21, 22	syl2an 454	. . . . . . . . . . . . . . . . 17 |- ((c e. RR /\ d e. RR) -> ((i x. c) + d) e. CC)
24	23	adantlr 393	. . . . . . . . . . . . . . . 16 |- (((c e. RR /\ (b + c) = y) /\ d e. RR) -> ((i x. c) + d) e. CC)
25	24	adantll 392	. . . . . . . . . . . . . . 15 |- (((((a e. RR /\ b e. RR) /\ (y e. RR /\ (i x. y) e. RR)) /\ (c e. RR /\ (b + c) = y)) /\ d e. RR) -> ((i x. c) + d) e. CC)
26	25	adantr 389	. . . . . . . . . . . . . 14 |- ((((((a e. RR /\ b e. RR) /\ (y e. RR /\ (i x. y) e. RR)) /\ (c e. RR /\ (b + c) = y)) /\ d e. RR) /\ ((a + (i x. y)) + d) = 0) -> ((i x. c) + d) e. CC)
27		axaddass 5277	. . . . . . . . . . . . . . . . . . . . . 22 |- (((a + (i x. b)) e. CC /\ (i x. c) e. CC /\ d e. CC) -> (((a + (i x. b)) + (i x. c)) + d) = ((a + (i x. b)) + ((i x. c) + d)))
28		axaddcl 5271	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a e. CC /\ (i x. b) e. CC) -> (a + (i x. b)) e. CC)
29		axmulcl 5273	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((i e. CC /\ b e. CC) -> (i x. b) e. CC)
30	18, 29	mpan 695	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (b e. CC -> (i x. b) e. CC)
31	28, 30	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((a e. CC /\ b e. CC) -> (a + (i x. b)) e. CC)
32	31	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((a e. CC /\ b e. CC) /\ c e. CC) /\ d e. CC) -> (a + (i x. b)) e. CC)
33	20	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((a e. CC /\ b e. CC) /\ c e. CC) /\ d e. CC) -> (i x. c) e. CC)
34		pm3.27 323	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((a e. CC /\ b e. CC) /\ c e. CC) /\ d e. CC) -> d e. CC)
35	27, 32, 33, 34	syl3anc 858	. . . . . . . . . . . . . . . . . . . . 21 |- ((((a e. CC /\ b e. CC) /\ c e. CC) /\ d e. CC) -> (((a + (i x. b)) + (i x. c)) + d) = ((a + (i x. b)) + ((i x. c) + d)))
36		axaddass 5277	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((a e. CC /\ (i x. b) e. CC /\ (i x. c) e. CC) -> ((a + (i x. b)) + (i x. c)) = (a + ((i x. b) + (i x. c))))
37		simpll 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> a e. CC)
38	30	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> (i x. b) e. CC)
39	20	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> (i x. c) e. CC)
40	36, 37, 38, 39	syl3anc 858	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> ((a + (i x. b)) + (i x. c)) = (a + ((i x. b) + (i x. c))))
41		axdistr 5279	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((i e. CC /\ b e. CC /\ c e. CC) -> (i x. (b + c)) = ((i x. b) + (i x. c)))
42	18, 41	mp3an1 903	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((b e. CC /\ c e. CC) -> (i x. (b + c)) = ((i x. b) + (i x. c)))
43	42	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> (i x. (b + c)) = ((i x. b) + (i x. c)))
44	43	opreq2d 3976	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> (a + (i x. (b + c))) = (a + ((i x. b) + (i x. c))))
45	40, 44	eqtr4d 1510	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> ((a + (i x. b)) + (i x. c)) = (a + (i x. (b + c))))
46	45	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((a e. CC /\ b e. CC) /\ c e. CC) /\ d e. CC) -> ((a + (i x. b)) + (i x. c)) = (a + (i x. (b + c))))
47	46	opreq1d 3975	. . . . . . . . . . . . . . . . . . . . 21 |- ((((a e. CC /\ b e. CC) /\ c e. CC) /\ d e. CC) -> (((a + (i x. b)) + (i x. c)) + d) = ((a + (i x. (b + c))) + d))
48	35, 47	eqtr3d 1509	. . . . . . . . . . . . . . . . . . . 20 |- ((((a e. CC /\ b e. CC) /\ c e. CC) /\ d e. CC) -> ((a + (i x. b)) + ((i x. c) + d)) = ((a + (i x. (b + c))) + d))
49		recnt 5313	. . . . . . . . . . . . . . . . . . . . . 22 |- (a e. RR -> a e. CC)
50		recnt 5313	. . . . . . . . . . . . . . . . . . . . . 22 |- (b e. RR -> b e. CC)
51	49, 50	anim12i 333	. . . . . . . . . . . . . . . . . . . . 21 |- ((a e. RR /\ b e. RR) -> (a e. CC /\ b e. CC))
52	51, 17	anim12i 333	. . . . . . . . . . . . . . . . . . . 20 |- (((a e. RR /\ b e. RR) /\ c e. RR) -> ((a e. CC /\ b e. CC) /\ c e. CC))
53	48, 52, 22	syl2an 454	. . . . . . . . . . . . . . . . . . 19 |- ((((a e. RR /\ b e. RR) /\ c e. RR) /\ d e. RR) -> ((a + (i x. b)) + ((i x. c) + d)) = ((a + (i x. (b + c))) + d))
54	53	adantlrr 399	. . . . . . . . . . . . . . . . . 18 |- ((((a e. RR /\ b e. RR) /\ (c e. RR /\ (b + c) = y)) /\ d e. RR) -> ((a + (i x. b)) + ((i x. c) + d)) = ((a + (i x. (b