# Metamath Proof Explorer

## Theorem exp0

Description: Value of a complex number raised to the 0th power. Note that under our definition, 0 ^ 0 = 1 , following the convention used by Gleason. Part of Definition 10-4.1 of Gleason p. 134. (Contributed by NM, 20-May-2004) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion exp0 ${⊢}{A}\in ℂ\to {{A}}^{0}=1$

### Proof

Step Hyp Ref Expression
1 0z ${⊢}0\in ℤ$
2 expval ${⊢}\left({A}\in ℂ\wedge 0\in ℤ\right)\to {{A}}^{0}=if\left(0=0,1,if\left(0<0,seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(0\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-0\right)}\right)\right)$
3 1 2 mpan2 ${⊢}{A}\in ℂ\to {{A}}^{0}=if\left(0=0,1,if\left(0<0,seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(0\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-0\right)}\right)\right)$
4 eqid ${⊢}0=0$
5 4 iftruei ${⊢}if\left(0=0,1,if\left(0<0,seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(0\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-0\right)}\right)\right)=1$
6 3 5 syl6eq ${⊢}{A}\in ℂ\to {{A}}^{0}=1$