Metamath Proof Explorer


Theorem absexpd

Description: Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses abscld.1 ( 𝜑𝐴 ∈ ℂ )
absexpd.2 ( 𝜑𝑁 ∈ ℕ0 )
Assertion absexpd ( 𝜑 → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 abscld.1 ( 𝜑𝐴 ∈ ℂ )
2 absexpd.2 ( 𝜑𝑁 ∈ ℕ0 )
3 absexp ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )
4 1 2 3 syl2anc ( 𝜑 → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )