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 
|- ( A e. CC -> E. x e. CC ( A + x ) = 0 )

Proof

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