Theorem absre

Description: Absolute value of a real number. (Contributed by NM, 17-Mar-2005)

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

Proof

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