Metamath Proof Explorer


Theorem ackvalsuc0val

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

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

Proof

Step Hyp Ref Expression
1 0nn0 0 0
2 ackvalsuc1 M 0 0 0 Ack M + 1 0 = IterComp Ack M 0 + 1 1
3 1 2 mpan2 M 0 Ack M + 1 0 = IterComp Ack M 0 + 1 1
4 0p1e1 0 + 1 = 1
5 4 a1i M 0 0 + 1 = 1
6 5 fveq2d M 0 IterComp Ack M 0 + 1 = IterComp Ack M 1
7 ackfnnn0 M 0 Ack M Fn 0
8 fnfun Ack M Fn 0 Fun Ack M
9 funrel Fun Ack M Rel Ack M
10 7 8 9 3syl M 0 Rel Ack M
11 fvex Ack M V
12 itcoval1 Rel Ack M Ack M V IterComp Ack M 1 = Ack M
13 10 11 12 sylancl M 0 IterComp Ack M 1 = Ack M
14 6 13 eqtrd M 0 IterComp Ack M 0 + 1 = Ack M
15 14 fveq1d M 0 IterComp Ack M 0 + 1 1 = Ack M 1
16 3 15 eqtrd M 0 Ack M + 1 0 = Ack M 1