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