Theorem recval

Description: Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015)

	Ref	Expression
Assertion	recval	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{1}{A}=\frac{\bar{A}}{{\left|A\right|}^2}$$

Proof

Step	Hyp	Ref	Expression
1		cjcl	$$⊢A\in ℂ\to \bar{A}\in ℂ$$
2	1	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \bar{A}\in ℂ$$
3		simpl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A\in ℂ$$
4	2 3	mulcomd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \bar{A}A=A\bar{A}$$
5		absvalsq	$$⊢A\in ℂ\to {\left|A\right|}^2=A\bar{A}$$
6	5	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\left|A\right|}^2=A\bar{A}$$
7	4 6	eqtr4d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \bar{A}A={\left|A\right|}^2$$
8		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
9	8	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in ℝ$$
10	9	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in ℂ$$
11	10	sqcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\left|A\right|}^2\in ℂ$$
12		cjne0	$$⊢A\in ℂ\to \left(A\ne 0\leftrightarrow \bar{A}\ne 0\right)$$
13	12	biimpa	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \bar{A}\ne 0$$
14	11 2 3 13	divmuld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(\frac{{\left|A\right|}^2}{\bar{A}}=A\leftrightarrow \bar{A}A={\left|A\right|}^2\right)$$
15	7 14	mpbird	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{{\left|A\right|}^2}{\bar{A}}=A$$
16	15	oveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{1}{\frac{{\left|A\right|}^2}{\bar{A}}}=\frac{1}{A}$$
17		abs00	$$⊢A\in ℂ\to \left(\left|A\right|=0\leftrightarrow A=0\right)$$
18	17	necon3bid	$$⊢A\in ℂ\to \left(\left|A\right|\ne 0\leftrightarrow A\ne 0\right)$$
19	18	biimpar	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\ne 0$$
20		sqne0	$$⊢\left|A\right|\in ℂ\to \left({\left|A\right|}^2\ne 0\leftrightarrow \left|A\right|\ne 0\right)$$
21	10 20	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left({\left|A\right|}^2\ne 0\leftrightarrow \left|A\right|\ne 0\right)$$
22	19 21	mpbird	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\left|A\right|}^2\ne 0$$
23	11 2 22 13	recdivd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{1}{\frac{{\left|A\right|}^2}{\bar{A}}}=\frac{\bar{A}}{{\left|A\right|}^2}$$
24	16 23	eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{1}{A}=\frac{\bar{A}}{{\left|A\right|}^2}$$