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 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2 expval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) = if ( 𝑁 = 0 , 1 , if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ) )
3 1 2 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = if ( 𝑁 = 0 , 1 , if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ) )
4 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
5 4 neneqd ⊢ ( 𝑁 ∈ ℕ → ¬ 𝑁 = 0 )
6 5 iffalsed ⊢ ( 𝑁 ∈ ℕ → if ( 𝑁 = 0 , 1 , if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ) = if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) )
7 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
8 7 iftrued ⊢ ( 𝑁 ∈ ℕ → if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
9 6 8 eqtrd ⊢ ( 𝑁 ∈ ℕ → if ( 𝑁 = 0 , 1 , if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
10 9 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → if ( 𝑁 = 0 , 1 , if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
11 3 10 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )