HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem cnegext 5320
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
StepHypRef Expression
1 axcnre 5258 . 2 |- (A e. CC -> E.a e. RR E.b e. RR A = (a + (i x. b)))
2 opreq1 3953 . . . . . 6 |- (A = (a + (i x. b)) -> (A + x) = ((a + (i x. b)) + x))
32eqeq1d 1475 . . . . 5 |- (A = (a + (i x. b)) -> ((A + x) = 0 <-> ((a + (i x. b)) + x) = 0))
43rexbidv 1656 . . . 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 5318 . . . . 5 |- E.y e. RR (i x. y) e. RR
6 cnegextlem3 5319 . . . . . . . . 9 |- ((b e. RR /\ y e. RR) -> E.c e. RR (b + c) = y)
76ad2ant2lr 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 5244 . . . . . . . . . . . . . 14 |- ((a e. RR /\ (i x. y) e. RR) -> (a + (i x. y)) e. RR)
9 axrnegex 5255 . . . . . . . . . . . . . 14 |- ((a + (i x. y)) e. RR -> E.d e. RR ((a + (i x. y)) + d) = 0)
108, 9syl 10 . . . . . . . . . . . . 13 |- ((a e. RR /\ (i x. y) e. RR) -> E.d e. RR ((a + (i x. y)) + d) = 0)
1110ad2ant2rl 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)
1211adantr 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 3954 . . . . . . . . . . . . . . . 16 |- (x = ((i x. c) + d) -> ((a + (i x. b)) + x) = ((a + (i x. b)) + ((i x. c) + d)))
1413eqeq1d 1475 . . . . . . . . . . . . . . 15 |- (x = ((i x. c) + d) -> (((a + (i x. b)) + x) = 0 <-> ((a + (i x. b)) + ((i x. c) + d)) = 0))
1514rcla4ev 1868 . . . . . . . . . . . . . 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 5243 . . . . . . . . . . . . . . . . . 18 |- (((i x. c) e. CC /\ d e. CC) -> ((i x. c) + d) e. CC)
17 recnt 5285 . . . . . . . . . . . . . . . . . . 19 |- (c e. RR -> c e. CC)
18 axicn 5242 . . . . . . . . . . . . . . . . . . . 20 |- i e. CC
19 axmulcl 5245 . . . . . . . . . . . . . . . . . . . 20 |- ((i e. CC /\ c e. CC) -> (i x. c) e. CC)
2018, 19mpan 693 . . . . . . . . . . . . . . . . . . 19 |- (c e. CC -> (i x. c) e. CC)
2117, 20syl 10 . . . . . . . . . . . . . . . . . 18 |- (c e. RR -> (i x. c) e. CC)
22 recnt 5285 . . . . . . . . . . . . . . . . . 18 |- (d e. RR -> d e. CC)
2316, 21, 22syl2an 454 . . . . . . . . . . . . . . . . 17 |- ((c e. RR /\ d e. RR) -> ((i x. c) + d) e. CC)
2423adantlr 393 . . . . . . . . . . . . . . . 16 |- (((c e. RR /\ (b + c) = y) /\ d e. RR) -> ((i x. c) + d) e. CC)
2524adantll 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)
2625adantr 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 5249 . . . . . . . . . . . . . . . . . . . . . 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 5243 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a e. CC /\ (i x. b) e. CC) -> (a + (i x. b)) e. CC)
29 axmulcl 5245 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((i e. CC /\ b e. CC) -> (i x. b) e. CC)
3018, 29mpan 693 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (b e. CC -> (i x. b) e. CC)
3128, 30sylan2 451 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((a e. CC /\ b e. CC) -> (a + (i x. b)) e. CC)
3231ad2antrr 404 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((a e. CC /\ b e. CC) /\ c e. CC) /\ d e. CC) -> (a + (i x. b)) e. CC)
3320ad2antlr 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)
3527, 32, 33, 34syl3anc 856 . . . . . . . . . . . . . . . . . . . . 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 5249 . . . . . . . . . . . . . . . . . . . . . . . . 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)
3830ad2antlr 405 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> (i x. b) e. CC)
3920adantl 388 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> (i x. c) e. CC)
4036, 37, 38, 39syl3anc 856 . . . . . . . . . . . . . . . . . . . . . . . 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 5251 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((i e. CC /\ b e. CC /\ c e. CC) -> (i x. (b + c)) = ((i x. b) + (i x. c)))
4218, 41mp3an1 900 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((b e. CC /\ c e. CC) -> (i x. (b + c)) = ((i x. b) + (i x. c)))
4342adantll 392 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> (i x. (b + c)) = ((i x. b) + (i x. c)))
4443opreq2d 3961 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> (a + (i x. (b + c))) = (a + ((i x. b) + (i x. c))))
4540, 44eqtr4d 1502 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((a e. CC /\ b e. CC) /\ c e. CC) -> ((a + (i x. b)) + (i x. c)) = (a + (i x. (b + c))))
4645adantr 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))))
4746opreq1d 3960 . . . . . . . . . . . . . . . . . . . . 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))
4835, 47eqtr3d 1501 . . . . . . . . . . . . . . . . . . . 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 5285 . . . . . . . . . . . . . . . . . . . . . 22 |- (a e. RR -> a e. CC)
50 recnt 5285 . . . . . . . . . . . . . . . . . . . . . 22 |- (b e. RR -> b e. CC)
5149, 50anim12i 333 . . . . . . . . . . . . . . . . . . . . 21 |- ((a e. RR /\ b e. RR) -> (a e. CC /\ b e. CC))
5251, 17anim12i 333 . . . . . . . . . . . . . . . . . . . 20 |- (((a e. RR /\ b e. RR) /\ c e. RR) -> ((a e. CC /\ b e. CC) /\ c e. CC))
5348, 52, 22syl2an 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))
5453adantlrr 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 +