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

Metamath Proof Explorer

Theorem expnnval

Description: Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expnnval ⊢ A ∈ ℂ ∧ N ∈ ℕ → A N = seq 1 × ℕ × A ⁡ N

Proof

Step Hyp Ref Expression
1 nnz ⊢ N ∈ ℕ → N ∈ ℤ
2 expval ⊢ A ∈ ℂ ∧ N ∈ ℤ → A N = if N = 0 1 if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ N ∈ ℕ → A N = if N = 0 1 if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N
4 nnne0 ⊢ N ∈ ℕ → N ≠ 0
5 4 neneqd ⊢ N ∈ ℕ → ¬ N = 0
6 5 iffalsed ⊢ N ∈ ℕ → if N = 0 1 if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N = if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N
7 nngt0 ⊢ N ∈ ℕ → 0 < N
8 7 iftrued ⊢ N ∈ ℕ → if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N = seq 1 × ℕ × A ⁡ N
9 6 8 eqtrd ⊢ N ∈ ℕ → if N = 0 1 if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N = seq 1 × ℕ × A ⁡ N
10 9 adantl ⊢ A ∈ ℂ ∧ N ∈ ℕ → if N = 0 1 if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N = seq 1 × ℕ × A ⁡ N
11 3 10 eqtrd ⊢ A ∈ ℂ ∧ N ∈ ℕ → A N = seq 1 × ℕ × A ⁡ N