Theorem absvalsq

Description: Square of value of absolute value function. (Contributed by NM, 16-Jan-2006)

	Ref	Expression
Assertion	absvalsq	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		absval	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
2	1	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ↑ 2 ) )
3		cjmulrcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ )
4		cjmulge0	⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
5		resqrtth	⊢ ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) → ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
6	3 4 5	syl2anc	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
7	2 6	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )