Metamath Proof Explorer

Theorem crreczi

Description: Reciprocal of a complex number in terms of real and imaginary components. Remark in Apostol p. 361. (Contributed by NM, 29-Apr-2005) (Proof shortened by Jeff Hankins, 16-Dec-2013)

Ref Expression
Hypotheses crrecz.1 
|- A e. RR
crrecz.2 
|- B e. RR
Assertion crreczi 
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 crrecz.1 
 |-  A e. RR
2 crrecz.2 
 |-  B e. RR
3 1 recni 
 |-  A e. CC
4 3 sqcli 
 |-  ( A ^ 2 ) e. CC
5 ax-icn 
 |-  _i e. CC
6 2 recni 
 |-  B e. CC
7 5 6 mulcli 
 |-  ( _i x. B ) e. CC
8 7 sqcli 
 |-  ( ( _i x. B ) ^ 2 ) e. CC
9 4 8 negsubi 
 |-  ( ( A ^ 2 ) + -u ( ( _i x. B ) ^ 2 ) ) = ( ( A ^ 2 ) - ( ( _i x. B ) ^ 2 ) )
10 5 6 sqmuli 
 |-  ( ( _i x. B ) ^ 2 ) = ( ( _i ^ 2 ) x. ( B ^ 2 ) )
11 i2 
 |-  ( _i ^ 2 ) = -u 1
12 11 oveq1i 
 |-  ( ( _i ^ 2 ) x. ( B ^ 2 ) ) = ( -u 1 x. ( B ^ 2 ) )
13 ax-1cn 
 |-  1 e. CC
14 6 sqcli 
 |-  ( B ^ 2 ) e. CC
15 13 14 mulneg1i 
 |-  ( -u 1 x. ( B ^ 2 ) ) = -u ( 1 x. ( B ^ 2 ) )
16 10 12 15 3eqtri 
 |-  ( ( _i x. B ) ^ 2 ) = -u ( 1 x. ( B ^ 2 ) )
17 16 negeqi 
 |-  -u ( ( _i x. B ) ^ 2 ) = -u -u ( 1 x. ( B ^ 2 ) )
18 13 14 mulcli 
 |-  ( 1 x. ( B ^ 2 ) ) e. CC
19 18 negnegi 
 |-  -u -u ( 1 x. ( B ^ 2 ) ) = ( 1 x. ( B ^ 2 ) )
20 14 mullidi 
 |-  ( 1 x. ( B ^ 2 ) ) = ( B ^ 2 )
21 17 19 20 3eqtri 
 |-  -u ( ( _i x. B ) ^ 2 ) = ( B ^ 2 )
22 21 oveq2i 
 |-  ( ( A ^ 2 ) + -u ( ( _i x. B ) ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) )
23 3 7 subsqi 
 |-  ( ( A ^ 2 ) - ( ( _i x. B ) ^ 2 ) ) = ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) )
24 9 22 23 3eqtr3ri 
 |-  ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) )
25 24 oveq1i 
 |-  ( ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) )
26 neorian 
 |-  ( ( A =/= 0 \/ B =/= 0 ) <-> -. ( A = 0 /\ B = 0 ) )
27 sumsqeq0 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A = 0 /\ B = 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) = 0 ) )
28 1 2 27 mp2an 
 |-  ( ( A = 0 /\ B = 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) = 0 )
29 28 necon3bbii 
 |-  ( -. ( A = 0 /\ B = 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 )
30 26 29 bitri 
 |-  ( ( A =/= 0 \/ B =/= 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 )
31 3 7 addcli 
 |-  ( A + ( _i x. B ) ) e. CC
32 3 7 subcli 
 |-  ( A - ( _i x. B ) ) e. CC
33 4 14 addcli 
 |-  ( ( A ^ 2 ) + ( B ^ 2 ) ) e. CC
34 31 32 33 divasszi 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 -> ( ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) )
35 30 34 sylbi 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) )
36 divid 
 |-  ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) e. CC /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = 1 )
37 33 36 mpan 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = 1 )
38 30 37 sylbi 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = 1 )
39 25 35 38 3eqtr3a 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) = 1 )
40 32 33 divclzi 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 -> ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) e. CC )
41 30 40 sylbi 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) e. CC )
42 31 a1i 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( A + ( _i x. B ) ) e. CC )
43 crne0 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A =/= 0 \/ B =/= 0 ) <-> ( A + ( _i x. B ) ) =/= 0 ) )
44 1 2 43 mp2an 
 |-  ( ( A =/= 0 \/ B =/= 0 ) <-> ( A + ( _i x. B ) ) =/= 0 )
45 44 biimpi 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( A + ( _i x. B ) ) =/= 0 )
46 divmul 
 |-  ( ( 1 e. CC /\ ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) e. CC /\ ( ( A + ( _i x. B ) ) e. CC /\ ( A + ( _i x. B ) ) =/= 0 ) ) -> ( ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) <-> ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) = 1 ) )
47 13 46 mp3an1 
 |-  ( ( ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) e. CC /\ ( ( A + ( _i x. B ) ) e. CC /\ ( A + ( _i x. B ) ) =/= 0 ) ) -> ( ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) <-> ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) = 1 ) )
48 41 42 45 47 syl12anc 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) <-> ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) = 1 ) )
49 39 48 mpbird 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )