# 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 ${⊢}\left({A}\in ℂ\wedge {N}\in ℤ\right)\to {{A}}^{{N}}=if\left({N}=0,1,if\left(0<{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right)}\right)\right)$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({x}={A}\wedge {y}={N}\right)\to {y}={N}$
2 1 eqeq1d ${⊢}\left({x}={A}\wedge {y}={N}\right)\to \left({y}=0↔{N}=0\right)$
3 1 breq2d ${⊢}\left({x}={A}\wedge {y}={N}\right)\to \left(0<{y}↔0<{N}\right)$
4 simpl ${⊢}\left({x}={A}\wedge {y}={N}\right)\to {x}={A}$
5 4 sneqd ${⊢}\left({x}={A}\wedge {y}={N}\right)\to \left\{{x}\right\}=\left\{{A}\right\}$
6 5 xpeq2d ${⊢}\left({x}={A}\wedge {y}={N}\right)\to ℕ×\left\{{x}\right\}=ℕ×\left\{{A}\right\}$
7 6 seqeq3d ${⊢}\left({x}={A}\wedge {y}={N}\right)\to seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)$
8 7 1 fveq12d ${⊢}\left({x}={A}\wedge {y}={N}\right)\to seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)\left({y}\right)=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)$
9 1 negeqd ${⊢}\left({x}={A}\wedge {y}={N}\right)\to -{y}=-{N}$
10 7 9 fveq12d ${⊢}\left({x}={A}\wedge {y}={N}\right)\to seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)\left(-{y}\right)=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right)$
11 10 oveq2d ${⊢}\left({x}={A}\wedge {y}={N}\right)\to \frac{1}{seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)\left(-{y}\right)}=\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right)}$
12 3 8 11 ifbieq12d ${⊢}\left({x}={A}\wedge {y}={N}\right)\to if\left(0<{y},seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)\left({y}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)\left(-{y}\right)}\right)=if\left(0<{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right)}\right)$
13 2 12 ifbieq2d ${⊢}\left({x}={A}\wedge {y}={N}\right)\to if\left({y}=0,1,if\left(0<{y},seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)\left({y}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)\left(-{y}\right)}\right)\right)=if\left({N}=0,1,if\left(0<{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right)}\right)\right)$
14 df-exp ${⊢}^=\left({x}\in ℂ,{y}\in ℤ⟼if\left({y}=0,1,if\left(0<{y},seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)\left({y}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{x}\right\}\right)\right)\left(-{y}\right)}\right)\right)\right)$
15 1ex ${⊢}1\in \mathrm{V}$
16 fvex ${⊢}seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)\in \mathrm{V}$
17 ovex ${⊢}\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right)}\in \mathrm{V}$
18 16 17 ifex ${⊢}if\left(0<{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right)}\right)\in \mathrm{V}$
19 15 18 ifex ${⊢}if\left({N}=0,1,if\left(0<{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right)}\right)\right)\in \mathrm{V}$
20 13 14 19 ovmpoa ${⊢}\left({A}\in ℂ\wedge {N}\in ℤ\right)\to {{A}}^{{N}}=if\left({N}=0,1,if\left(0<{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right)}\right)\right)$