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 ⊢ A ∈ ℂ ∧ N ∈ ℤ → A N = if N = 0 1 if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N

Proof

Step Hyp Ref Expression
1 simpr ⊢ x = A ∧ y = N → y = N
2 1 eqeq1d ⊢ x = A ∧ y = N → y = 0 ↔ N = 0
3 1 breq2d ⊢ x = A ∧ y = N → 0 < y ↔ 0 < N
4 simpl ⊢ x = A ∧ y = N → x = A
5 4 sneqd ⊢ x = A ∧ y = N → x = A
6 5 xpeq2d ⊢ x = A ∧ y = N → ℕ × x = ℕ × A
7 6 seqeq3d ⊢ x = A ∧ y = N → seq 1 × ℕ × x = seq 1 × ℕ × A
8 7 1 fveq12d ⊢ x = A ∧ y = N → seq 1 × ℕ × x ⁡ y = seq 1 × ℕ × A ⁡ N
9 1 negeqd ⊢ x = A ∧ y = N → − y = − N
10 7 9 fveq12d ⊢ x = A ∧ y = N → seq 1 × ℕ × x ⁡ − y = seq 1 × ℕ × A ⁡ − N
11 10 oveq2d ⊢ x = A ∧ y = N → 1 seq 1 × ℕ × x ⁡ − y = 1 seq 1 × ℕ × A ⁡ − N
12 3 8 11 ifbieq12d ⊢ x = A ∧ y = N → if 0 < y seq 1 × ℕ × x ⁡ y 1 seq 1 × ℕ × x ⁡ − y = if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N
13 2 12 ifbieq2d ⊢ x = A ∧ y = N → if y = 0 1 if 0 < y seq 1 × ℕ × x ⁡ y 1 seq 1 × ℕ × x ⁡ − y = if N = 0 1 if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N
14 df-exp ⊢ ^ = x ∈ ℂ , y ∈ ℤ ⟼ if y = 0 1 if 0 < y seq 1 × ℕ × x ⁡ y 1 seq 1 × ℕ × x ⁡ − y
15 1ex ⊢ 1 ∈ V
16 fvex ⊢ seq 1 × ℕ × A ⁡ N ∈ V
17 ovex ⊢ 1 seq 1 × ℕ × A ⁡ − N ∈ V
18 16 17 ifex ⊢ if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N ∈ V
19 15 18 ifex ⊢ if N = 0 1 if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N ∈ V
20 13 14 19 ovmpoa ⊢ A ∈ ℂ ∧ N ∈ ℤ → A N = if N = 0 1 if 0 < N seq 1 × ℕ × A ⁡ N 1 seq 1 × ℕ × A ⁡ − N