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