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	mullidi	⊢ ( 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 ) ) ) )