Theorem numexpp1

Description: Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015)

	Ref	Expression
Hypotheses	numexp.1	⊢ 𝐴 ∈ ℕ0
	numexpp1.2	⊢ 𝑀 ∈ ℕ0
	numexpp1.3	⊢ ( 𝑀 + 1 ) = 𝑁
	numexpp1.4	⊢ ( ( 𝐴 ↑ 𝑀 ) · 𝐴 ) = 𝐶
Assertion	numexpp1	⊢ ( 𝐴 ↑ 𝑁 ) = 𝐶

Proof

Step	Hyp	Ref	Expression
1		numexp.1	⊢ 𝐴 ∈ ℕ0
2		numexpp1.2	⊢ 𝑀 ∈ ℕ0
3		numexpp1.3	⊢ ( 𝑀 + 1 ) = 𝑁
4		numexpp1.4	⊢ ( ( 𝐴 ↑ 𝑀 ) · 𝐴 ) = 𝐶
5	1	nn0cni	⊢ 𝐴 ∈ ℂ
6		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 1 ) ) = ( ( 𝐴 ↑ 𝑀 ) · 𝐴 ) )
7	5 2 6	mp2an	⊢ ( 𝐴 ↑ ( 𝑀 + 1 ) ) = ( ( 𝐴 ↑ 𝑀 ) · 𝐴 )
8	3	oveq2i	⊢ ( 𝐴 ↑ ( 𝑀 + 1 ) ) = ( 𝐴 ↑ 𝑁 )
9	7 8 4	3eqtr3i	⊢ ( 𝐴 ↑ 𝑁 ) = 𝐶