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 ⊢ 𝐴 ∈ ℝ
crrecz.2 ⊢ 𝐵 ∈ ℝ
Assertion crreczi ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( 1 / ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 crrecz.1 ⊢ 𝐴 ∈ ℝ
2 crrecz.2 ⊢ 𝐵 ∈ ℝ
3 1 recni ⊢ 𝐴 ∈ ℂ
4 3 sqcli ⊢ ( 𝐴 ↑ 2 ) ∈ ℂ
5 ax-icn ⊢ i ∈ ℂ
6 2 recni ⊢ 𝐵 ∈ ℂ
7 5 6 mulcli ⊢ ( i · 𝐵 ) ∈ ℂ
8 7 sqcli ⊢ ( ( i · 𝐵 ) ↑ 2 ) ∈ ℂ
9 4 8 negsubi ⊢ ( ( 𝐴 ↑ 2 ) + - ( ( i · 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) − ( ( i · 𝐵 ) ↑ 2 ) )
10 5 6 sqmuli ⊢ ( ( i · 𝐵 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐵 ↑ 2 ) )
11 i2 ⊢ ( i ↑ 2 ) = - 1
12 11 oveq1i ⊢ ( ( i ↑ 2 ) · ( 𝐵 ↑ 2 ) ) = ( - 1 · ( 𝐵 ↑ 2 ) )
13 ax-1cn ⊢ 1 ∈ ℂ
14 6 sqcli ⊢ ( 𝐵 ↑ 2 ) ∈ ℂ
15 13 14 mulneg1i ⊢ ( - 1 · ( 𝐵 ↑ 2 ) ) = - ( 1 · ( 𝐵 ↑ 2 ) )
16 10 12 15 3eqtri ⊢ ( ( i · 𝐵 ) ↑ 2 ) = - ( 1 · ( 𝐵 ↑ 2 ) )
17 16 negeqi ⊢ - ( ( i · 𝐵 ) ↑ 2 ) = - - ( 1 · ( 𝐵 ↑ 2 ) )
18 13 14 mulcli ⊢ ( 1 · ( 𝐵 ↑ 2 ) ) ∈ ℂ
19 18 negnegi ⊢ - - ( 1 · ( 𝐵 ↑ 2 ) ) = ( 1 · ( 𝐵 ↑ 2 ) )
20 14 mulid2i ⊢ ( 1 · ( 𝐵 ↑ 2 ) ) = ( 𝐵 ↑ 2 )
21 17 19 20 3eqtri ⊢ - ( ( i · 𝐵 ) ↑ 2 ) = ( 𝐵 ↑ 2 )
22 21 oveq2i ⊢ ( ( 𝐴 ↑ 2 ) + - ( ( i · 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
23 3 7 subsqi ⊢ ( ( 𝐴 ↑ 2 ) − ( ( i · 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐴 − ( i · 𝐵 ) ) )
24 9 22 23 3eqtr3ri ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐴 − ( i · 𝐵 ) ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
25 24 oveq1i ⊢ ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐴 − ( i · 𝐵 ) ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
26 neorian ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
27 sumsqeq0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) ↔ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 0 ) )
28 1 2 27 mp2an ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) ↔ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 0 )
29 28 necon3bbii ⊢ ( ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ↔ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ≠ 0 )
30 26 29 bitri ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ≠ 0 )
31 3 7 addcli ⊢ ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ
32 3 7 subcli ⊢ ( 𝐴 − ( i · 𝐵 ) ) ∈ ℂ
33 4 14 addcli ⊢ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℂ
34 31 32 33 divasszi ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ≠ 0 → ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐴 − ( i · 𝐵 ) ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐴 + ( i · 𝐵 ) ) · ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ) )
35 30 34 sylbi ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐴 − ( i · 𝐵 ) ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐴 + ( i · 𝐵 ) ) · ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ) )
36 divid ⊢ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ≠ 0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = 1 )
37 33 36 mpan ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ≠ 0 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = 1 )
38 30 37 sylbi ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = 1 )
39 25 35 38 3eqtr3a ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( ( 𝐴 + ( i · 𝐵 ) ) · ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ) = 1 )
40 32 33 divclzi ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ≠ 0 → ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ∈ ℂ )
41 30 40 sylbi ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ∈ ℂ )
42 31 a1i ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
43 crne0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) )
44 1 2 43 mp2an ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 )
45 44 biimpi ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 )
46 divmul ⊢ ( ( 1 ∈ ℂ ∧ ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ∈ ℂ ∧ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ ∧ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) ) → ( ( 1 / ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ↔ ( ( 𝐴 + ( i · 𝐵 ) ) · ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ) = 1 ) )
47 13 46 mp3an1 ⊢ ( ( ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ∈ ℂ ∧ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ ∧ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) ) → ( ( 1 / ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ↔ ( ( 𝐴 + ( i · 𝐵 ) ) · ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ) = 1 ) )
48 41 42 45 47 syl12anc ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( ( 1 / ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ↔ ( ( 𝐴 + ( i · 𝐵 ) ) · ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) ) = 1 ) )
49 39 48 mpbird ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( 1 / ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( 𝐴 − ( i · 𝐵 ) ) / ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )