Theorem abslem2

Description: Lemma involving absolute values. (Contributed by NM, 11-Oct-1999) (Revised by Mario Carneiro, 29-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		absvalsq	$$⊢A\in ℂ\to {\left|A\right|}^2=A\bar{A}$$
2	1	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\left|A\right|}^2=A\bar{A}$$
3		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
4	3	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in ℝ$$
5	4	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in ℂ$$
6	5	sqvald	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\left|A\right|}^2=\left|A\right|\left|A\right|$$
7	2 6	eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A\bar{A}=\left|A\right|\left|A\right|$$
8	7	oveq1d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{A\bar{A}}{\left|A\right|}=\frac{\left|A\right|\left|A\right|}{\left|A\right|}$$
9		simpl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A\in ℂ$$
10	9	cjcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \bar{A}\in ℂ$$
11		abs00	$$⊢A\in ℂ\to \left(\left|A\right|=0\leftrightarrow A=0\right)$$
12	11	necon3bid	$$⊢A\in ℂ\to \left(\left|A\right|\ne 0\leftrightarrow A\ne 0\right)$$
13	12	biimpar	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\ne 0$$
14	9 10 5 13	div23d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{A\bar{A}}{\left|A\right|}=\left(\frac{A}{\left|A\right|}\right)\bar{A}$$
15	5 5 13	divcan3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{\left|A\right|\left|A\right|}{\left|A\right|}=\left|A\right|$$
16	8 14 15	3eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(\frac{A}{\left|A\right|}\right)\bar{A}=\left|A\right|$$
17	16	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \overline{\left(\frac{A}{\left|A\right|}\right)\stackrel{‾}{A}}=\overline{\left|A\right|}$$
18	9 5 13	divcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{A}{\left|A\right|}\in ℂ$$
19	18 10	cjmuld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \overline{\left(\frac{A}{\left|A\right|}\right)\stackrel{‾}{A}}=\overline{\frac{A}{\left|A\right|}}\overline{\stackrel{‾}{A}}$$
20	9	cjcjd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \overline{\stackrel{‾}{A}}=A$$
21	20	oveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \overline{\frac{A}{\left|A\right|}}\overline{\stackrel{‾}{A}}=\overline{\frac{A}{\left|A\right|}}A$$
22	19 21	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \overline{\left(\frac{A}{\left|A\right|}\right)\stackrel{‾}{A}}=\overline{\frac{A}{\left|A\right|}}A$$
23	4	cjred	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \overline{\left|A\right|}=\left|A\right|$$
24	17 22 23	3eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \overline{\frac{A}{\left|A\right|}}A=\left|A\right|$$
25	24 16	oveq12d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \overline{\frac{A}{\left|A\right|}}A+\left(\frac{A}{\left|A\right|}\right)\bar{A}=\left|A\right|+\left|A\right|$$
26	5	2timesd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to 2\left|A\right|=\left|A\right|+\left|A\right|$$
27	25 26	eqtr4d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \overline{\frac{A}{\left|A\right|}}A+\left(\frac{A}{\left|A\right|}\right)\bar{A}=2\left|A\right|$$