This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )