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 eqtrdi
 |-  ( ( ( ( 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 )