Metamath Proof Explorer


Theorem 0exp0e1

Description: The zeroth power of zero equals one. See comment of exp0 . (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion 0exp0e1 ⊢ 0 0 = 1

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 exp0 ⊢ 0 ∈ ℂ → 0 0 = 1
3 1 2 ax-mp ⊢ 0 0 = 1