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 \in ℝ$
	crrecz.2	$⊢ B \in ℝ$
Assertion	crreczi	$⊢ (A \neq 0 \lor B \neq 0) \to \frac{1}{A + i B} = \frac{A - i B}{A^{2} + B^{2}}$

Proof

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

Metamath Proof Explorer

Theorem crreczi

Proof