This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Elementary real and complex functions Square root; absolute value abssq
Description: Square can be moved in and out of absolute value. (Contributed by Scott
Fenton , 18-Apr-2014) (Proof shortened by Mario Carneiro , 29-May-2016)
Ref
Expression
Assertion
abssq ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( abs ‘ ( 𝐴 ↑ 2 ) ) )
Proof
Step
Hyp
Ref
Expression
1
2nn0 ⊢ 2 ∈ ℕ0
2
absexp ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 2 ) ) = ( ( abs ‘ 𝐴 ) ↑ 2 ) )
3
1 2
mpan2 ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( 𝐴 ↑ 2 ) ) = ( ( abs ‘ 𝐴 ) ↑ 2 ) )
4
3
eqcomd ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( abs ‘ ( 𝐴 ↑ 2 ) ) )