Theorem abslem2

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

	Ref	Expression
Assertion	abslem2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) + ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( 2 · ( abs ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		absvalsq	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
3		abscl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
5	4	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
6	5	sqvald	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) )
7	2 6	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) )
8	7	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) = ( ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) )
9		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
10	9	cjcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
11		abs00	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
12	11	necon3bid	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
13	12	biimpar	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
14	9 10 5 13	div23d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) = ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) )
15	5 5 13	divcan3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
16	8 14 15	3eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
17	16	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( ∗ ‘ ( abs ‘ 𝐴 ) ) )
18	9 5 13	divcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 / ( abs ‘ 𝐴 ) ) ∈ ℂ )
19	18 10	cjmuld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ) )
20	9	cjcjd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) = 𝐴 )
21	20	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) )
22	19 21	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) )
23	4	cjred	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
24	17 22 23	3eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) = ( abs ‘ 𝐴 ) )
25	24 16	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) + ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐴 ) ) )
26	5	2timesd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 2 · ( abs ‘ 𝐴 ) ) = ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐴 ) ) )
27	25 26	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) + ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( 2 · ( abs ‘ 𝐴 ) ) )