Metamath Proof Explorer


Theorem ackval0val

Description: The Ackermann function at 0 (for the first argument). This is the first equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024)

Ref Expression
Assertion ackval0val M 0 Ack 0 M = M + 1

Proof

Step Hyp Ref Expression
1 ackval0 Ack 0 = m 0 m + 1
2 1 a1i M 0 Ack 0 = m 0 m + 1
3 oveq1 m = M m + 1 = M + 1
4 3 adantl M 0 m = M m + 1 = M + 1
5 id M 0 M 0
6 peano2nn0 M 0 M + 1 0
7 2 4 5 6 fvmptd M 0 Ack 0 M = M + 1