Metamath Proof Explorer


Theorem ackvalsuc1mpt

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

Ref Expression
Assertion ackvalsuc1mpt M 0 Ack M + 1 = n 0 IterComp Ack M n + 1 1

Proof

Step Hyp Ref Expression
1 df-ack Ack = seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i
2 1 fveq1i Ack M + 1 = seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i M + 1
3 nn0uz 0 = 0
4 id M 0 M 0
5 eqid M + 1 = M + 1
6 1 eqcomi seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i = Ack
7 6 fveq1i seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i M = Ack M
8 7 a1i M 0 seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i M = Ack M
9 eqidd M 0 i 0 if i = 0 n 0 n + 1 i = i 0 if i = 0 n 0 n + 1 i
10 nn0p1gt0 M 0 0 < M + 1
11 10 gt0ne0d M 0 M + 1 0
12 11 adantr M 0 i = M + 1 M + 1 0
13 neeq1 i = M + 1 i 0 M + 1 0
14 13 adantl M 0 i = M + 1 i 0 M + 1 0
15 12 14 mpbird M 0 i = M + 1 i 0
16 15 neneqd M 0 i = M + 1 ¬ i = 0
17 16 iffalsed M 0 i = M + 1 if i = 0 n 0 n + 1 i = i
18 simpr M 0 i = M + 1 i = M + 1
19 17 18 eqtrd M 0 i = M + 1 if i = 0 n 0 n + 1 i = M + 1
20 peano2nn0 M 0 M + 1 0
21 9 19 20 20 fvmptd M 0 i 0 if i = 0 n 0 n + 1 i M + 1 = M + 1
22 3 4 5 8 21 seqp1d M 0 seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i M + 1 = Ack M f V , j V n 0 IterComp f n + 1 1 M + 1
23 eqidd M 0 f V , j V n 0 IterComp f n + 1 1 = f V , j V n 0 IterComp f n + 1 1
24 fveq2 f = Ack M IterComp f = IterComp Ack M
25 24 fveq1d f = Ack M IterComp f n + 1 = IterComp Ack M n + 1
26 25 fveq1d f = Ack M IterComp f n + 1 1 = IterComp Ack M n + 1 1
27 26 mpteq2dv f = Ack M n 0 IterComp f n + 1 1 = n 0 IterComp Ack M n + 1 1
28 27 ad2antrl M 0 f = Ack M j = M + 1 n 0 IterComp f n + 1 1 = n 0 IterComp Ack M n + 1 1
29 fvexd M 0 Ack M V
30 ovexd M 0 M + 1 V
31 nn0ex 0 V
32 31 mptex n 0 IterComp Ack M n + 1 1 V
33 32 a1i M 0 n 0 IterComp Ack M n + 1 1 V
34 23 28 29 30 33 ovmpod M 0 Ack M f V , j V n 0 IterComp f n + 1 1 M + 1 = n 0 IterComp Ack M n + 1 1
35 22 34 eqtrd M 0 seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i M + 1 = n 0 IterComp Ack M n + 1 1
36 2 35 eqtrid M 0 Ack M + 1 = n 0 IterComp Ack M n + 1 1