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