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

Metamath Proof Explorer

Theorem numexpp1

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

Ref Expression
Hypotheses numexp.1 ⊢ A ∈ ℕ 0
numexpp1.2 ⊢ M ∈ ℕ 0
numexpp1.3 ⊢ M + 1 = N
numexpp1.4 ⊢ A M ⁢ A = C
Assertion numexpp1 ⊢ A N = C

Proof

Step Hyp Ref Expression
1 numexp.1 ⊢ A ∈ ℕ 0
2 numexpp1.2 ⊢ M ∈ ℕ 0
3 numexpp1.3 ⊢ M + 1 = N
4 numexpp1.4 ⊢ A M ⁢ A = C
5 1 nn0cni ⊢ A ∈ ℂ
6 expp1 ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 → A M + 1 = A M ⁢ A
7 5 2 6 mp2an ⊢ A M + 1 = A M ⁢ A
8 3 oveq2i ⊢ A M + 1 = A N
9 7 8 4 3eqtr3i ⊢ A N = C