Theorem absresq

Description: Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006)

	Ref	Expression
Assertion	absresq	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		cjre	⊢ ( 𝐴 ∈ ℝ → ( ∗ ‘ 𝐴 ) = 𝐴 )
2	1	oveq2d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) = ( 𝐴 · 𝐴 ) )
3		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4		absvalsq	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
5	3 4	syl	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
6	3	sqvald	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
7	2 5 6	3eqtr4d	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )