Metamath Proof Explorer

Theorem recex

Description: Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007)

Ref Expression
Assertion recex 
|- ( ( A e. CC /\ A =/= 0 ) -> E. x e. CC ( A x. x ) = 1 )

Proof

Step Hyp Ref Expression
1 cnre 
 |-  ( A e. CC -> E. a e. RR E. b e. RR A = ( a + ( _i x. b ) ) )
2 recextlem2 
 |-  ( ( a e. RR /\ b e. RR /\ ( a + ( _i x. b ) ) =/= 0 ) -> ( ( a x. a ) + ( b x. b ) ) =/= 0 )
3 2 3expia 
 |-  ( ( a e. RR /\ b e. RR ) -> ( ( a + ( _i x. b ) ) =/= 0 -> ( ( a x. a ) + ( b x. b ) ) =/= 0 ) )
4 remulcl 
 |-  ( ( a e. RR /\ a e. RR ) -> ( a x. a ) e. RR )
5 4 anidms 
 |-  ( a e. RR -> ( a x. a ) e. RR )
6 remulcl 
 |-  ( ( b e. RR /\ b e. RR ) -> ( b x. b ) e. RR )
7 6 anidms 
 |-  ( b e. RR -> ( b x. b ) e. RR )
8 readdcl 
 |-  ( ( ( a x. a ) e. RR /\ ( b x. b ) e. RR ) -> ( ( a x. a ) + ( b x. b ) ) e. RR )
9 5 7 8 syl2an 
 |-  ( ( a e. RR /\ b e. RR ) -> ( ( a x. a ) + ( b x. b ) ) e. RR )
10 ax-rrecex 
 |-  ( ( ( ( a x. a ) + ( b x. b ) ) e. RR /\ ( ( a x. a ) + ( b x. b ) ) =/= 0 ) -> E. y e. RR ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 )
11 9 10 sylan 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( ( a x. a ) + ( b x. b ) ) =/= 0 ) -> E. y e. RR ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 )
12 recn 
 |-  ( a e. RR -> a e. CC )
13 recn 
 |-  ( b e. RR -> b e. CC )
14 recn 
 |-  ( y e. RR -> y e. CC )
15 ax-icn 
 |-  _i e. CC
16 mulcl 
 |-  ( ( _i e. CC /\ b e. CC ) -> ( _i x. b ) e. CC )
17 15 16 mpan 
 |-  ( b e. CC -> ( _i x. b ) e. CC )
18 subcl 
 |-  ( ( a e. CC /\ ( _i x. b ) e. CC ) -> ( a - ( _i x. b ) ) e. CC )
19 17 18 sylan2 
 |-  ( ( a e. CC /\ b e. CC ) -> ( a - ( _i x. b ) ) e. CC )
20 mulcl 
 |-  ( ( ( a - ( _i x. b ) ) e. CC /\ y e. CC ) -> ( ( a - ( _i x. b ) ) x. y ) e. CC )
21 19 20 sylan 
 |-  ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) -> ( ( a - ( _i x. b ) ) x. y ) e. CC )
22 addcl 
 |-  ( ( a e. CC /\ ( _i x. b ) e. CC ) -> ( a + ( _i x. b ) ) e. CC )
23 17 22 sylan2 
 |-  ( ( a e. CC /\ b e. CC ) -> ( a + ( _i x. b ) ) e. CC )
24 23 adantr 
 |-  ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) -> ( a + ( _i x. b ) ) e. CC )
25 19 adantr 
 |-  ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) -> ( a - ( _i x. b ) ) e. CC )
26 simpr 
 |-  ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) -> y e. CC )
27 24 25 26 mulassd 
 |-  ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) -> ( ( ( a + ( _i x. b ) ) x. ( a - ( _i x. b ) ) ) x. y ) = ( ( a + ( _i x. b ) ) x. ( ( a - ( _i x. b ) ) x. y ) ) )
28 recextlem1 
 |-  ( ( a e. CC /\ b e. CC ) -> ( ( a + ( _i x. b ) ) x. ( a - ( _i x. b ) ) ) = ( ( a x. a ) + ( b x. b ) ) )
29 28 adantr 
 |-  ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) -> ( ( a + ( _i x. b ) ) x. ( a - ( _i x. b ) ) ) = ( ( a x. a ) + ( b x. b ) ) )
30 29 oveq1d 
 |-  ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) -> ( ( ( a + ( _i x. b ) ) x. ( a - ( _i x. b ) ) ) x. y ) = ( ( ( a x. a ) + ( b x. b ) ) x. y ) )
31 27 30 eqtr3d 
 |-  ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) -> ( ( a + ( _i x. b ) ) x. ( ( a - ( _i x. b ) ) x. y ) ) = ( ( ( a x. a ) + ( b x. b ) ) x. y ) )
32 id 
 |-  ( ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 -> ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 )
33 31 32 sylan9eq 
 |-  ( ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) /\ ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 ) -> ( ( a + ( _i x. b ) ) x. ( ( a - ( _i x. b ) ) x. y ) ) = 1 )
34 oveq2 
 |-  ( x = ( ( a - ( _i x. b ) ) x. y ) -> ( ( a + ( _i x. b ) ) x. x ) = ( ( a + ( _i x. b ) ) x. ( ( a - ( _i x. b ) ) x. y ) ) )
35 34 eqeq1d 
 |-  ( x = ( ( a - ( _i x. b ) ) x. y ) -> ( ( ( a + ( _i x. b ) ) x. x ) = 1 <-> ( ( a + ( _i x. b ) ) x. ( ( a - ( _i x. b ) ) x. y ) ) = 1 ) )
36 35 rspcev 
 |-  ( ( ( ( a - ( _i x. b ) ) x. y ) e. CC /\ ( ( a + ( _i x. b ) ) x. ( ( a - ( _i x. b ) ) x. y ) ) = 1 ) -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 )
37 21 33 36 syl2an2r 
 |-  ( ( ( ( a e. CC /\ b e. CC ) /\ y e. CC ) /\ ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 ) -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 )
38 37 exp31 
 |-  ( ( a e. CC /\ b e. CC ) -> ( y e. CC -> ( ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) ) )
39 14 38 syl5 
 |-  ( ( a e. CC /\ b e. CC ) -> ( y e. RR -> ( ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) ) )
40 39 rexlimdv 
 |-  ( ( a e. CC /\ b e. CC ) -> ( E. y e. RR ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) )
41 12 13 40 syl2an 
 |-  ( ( a e. RR /\ b e. RR ) -> ( E. y e. RR ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) )
42 41 adantr 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( ( a x. a ) + ( b x. b ) ) =/= 0 ) -> ( E. y e. RR ( ( ( a x. a ) + ( b x. b ) ) x. y ) = 1 -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) )
43 11 42 mpd 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( ( a x. a ) + ( b x. b ) ) =/= 0 ) -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 )
44 43 ex 
 |-  ( ( a e. RR /\ b e. RR ) -> ( ( ( a x. a ) + ( b x. b ) ) =/= 0 -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) )
45 3 44 syld 
 |-  ( ( a e. RR /\ b e. RR ) -> ( ( a + ( _i x. b ) ) =/= 0 -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) )
46 45 adantr 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ A = ( a + ( _i x. b ) ) ) -> ( ( a + ( _i x. b ) ) =/= 0 -> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) )
47 neeq1 
 |-  ( A = ( a + ( _i x. b ) ) -> ( A =/= 0 <-> ( a + ( _i x. b ) ) =/= 0 ) )
48 47 adantl 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ A = ( a + ( _i x. b ) ) ) -> ( A =/= 0 <-> ( a + ( _i x. b ) ) =/= 0 ) )
49 oveq1 
 |-  ( A = ( a + ( _i x. b ) ) -> ( A x. x ) = ( ( a + ( _i x. b ) ) x. x ) )
50 49 eqeq1d 
 |-  ( A = ( a + ( _i x. b ) ) -> ( ( A x. x ) = 1 <-> ( ( a + ( _i x. b ) ) x. x ) = 1 ) )
51 50 rexbidv 
 |-  ( A = ( a + ( _i x. b ) ) -> ( E. x e. CC ( A x. x ) = 1 <-> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) )
52 51 adantl 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ A = ( a + ( _i x. b ) ) ) -> ( E. x e. CC ( A x. x ) = 1 <-> E. x e. CC ( ( a + ( _i x. b ) ) x. x ) = 1 ) )
53 46 48 52 3imtr4d 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ A = ( a + ( _i x. b ) ) ) -> ( A =/= 0 -> E. x e. CC ( A x. x ) = 1 ) )
54 53 ex 
 |-  ( ( a e. RR /\ b e. RR ) -> ( A = ( a + ( _i x. b ) ) -> ( A =/= 0 -> E. x e. CC ( A x. x ) = 1 ) ) )
55 54 rexlimivv 
 |-  ( E. a e. RR E. b e. RR A = ( a + ( _i x. b ) ) -> ( A =/= 0 -> E. x e. CC ( A x. x ) = 1 ) )
56 1 55 syl 
 |-  ( A e. CC -> ( A =/= 0 -> E. x e. CC ( A x. x ) = 1 ) )
57 56 imp 
 |-  ( ( A e. CC /\ A =/= 0 ) -> E. x e. CC ( A x. x ) = 1 )