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

Metamath Proof Explorer

Theorem expval

Description: Value of exponentiation to integer powers. (Contributed by NM, 20-May-2004) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expval ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) = if ( 𝑁 = 0 , 1 , if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → 𝑦 = 𝑁 )
2 1 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → ( 𝑦 = 0 ↔ 𝑁 = 0 ) )
3 1 breq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → ( 0 < 𝑦 ↔ 0 < 𝑁 ) )
4 simpl ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → 𝑥 = 𝐴 )
5 4 sneqd ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → { 𝑥 } = { 𝐴 } )
6 5 xpeq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → ( ℕ × { 𝑥 } ) = ( ℕ × { 𝐴 } ) )
7 6 seqeq3d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → seq 1 ( · , ( ℕ × { 𝑥 } ) ) = seq 1 ( · , ( ℕ × { 𝐴 } ) ) )
8 7 1 fveq12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
9 1 negeqd ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → - 𝑦 = - 𝑁 )
10 7 9 fveq12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) )
11 10 oveq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) ) = ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) )
12 3 8 11 ifbieq12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → if ( 0 < 𝑦 , ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) ) ) = if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) )
13 2 12 ifbieq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝑁 ) → if ( 𝑦 = 0 , 1 , if ( 0 < 𝑦 , ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) ) ) ) = if ( 𝑁 = 0 , 1 , if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ) )
14 df-exp ⊢ ↑ = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℤ ↦ if ( 𝑦 = 0 , 1 , if ( 0 < 𝑦 , ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) ) ) ) )
15 1ex ⊢ 1 ∈ V
16 fvex ⊢ ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) ∈ V
17 ovex ⊢ ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ∈ V
18 16 17 ifex ⊢ if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ∈ V
19 15 18 ifex ⊢ if ( 𝑁 = 0 , 1 , if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ) ∈ V
20 13 14 19 ovmpoa ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) = if ( 𝑁 = 0 , 1 , if ( 0 < 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) ) ) ) )