Metamath Proof Explorer


Theorem ackvalsuc1

Description: The Ackermann function at a successor of the first argument and an arbitrary second argument. (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 4-May-2024)

Ref Expression
Assertion ackvalsuc1 M 0 N 0 Ack M + 1 N = IterComp Ack M N + 1 1

Proof

Step Hyp Ref Expression
1 ackvalsuc1mpt M 0 Ack M + 1 = n 0 IterComp Ack M n + 1 1
2 1 adantr M 0 N 0 Ack M + 1 = n 0 IterComp Ack M n + 1 1
3 fvoveq1 n = N IterComp Ack M n + 1 = IterComp Ack M N + 1
4 3 fveq1d n = N IterComp Ack M n + 1 1 = IterComp Ack M N + 1 1
5 4 adantl M 0 N 0 n = N IterComp Ack M n + 1 1 = IterComp Ack M N + 1 1
6 simpr M 0 N 0 N 0
7 fvexd M 0 N 0 IterComp Ack M N + 1 1 V
8 2 5 6 7 fvmptd M 0 N 0 Ack M + 1 N = IterComp Ack M N + 1 1