Metamath Proof Explorer


Theorem ackvalsucsucval

Description: The Ackermann function at the successors. This is the third equation of Péter's definition of the Ackermann function. (Contributed by AV, 8-May-2024)

Ref Expression
Assertion ackvalsucsucval M 0 N 0 Ack M + 1 N + 1 = Ack M Ack M + 1 N

Proof

Step Hyp Ref Expression
1 peano2nn0 N 0 N + 1 0
2 ackvalsuc1 M 0 N + 1 0 Ack M + 1 N + 1 = IterComp Ack M N + 1 + 1 1
3 1 2 sylan2 M 0 N 0 Ack M + 1 N + 1 = IterComp Ack M N + 1 + 1 1
4 fvexd M 0 N 0 Ack M V
5 1 adantl M 0 N 0 N + 1 0
6 eqidd M 0 N 0 IterComp Ack M N + 1 = IterComp Ack M N + 1
7 itcovalsucov Ack M V N + 1 0 IterComp Ack M N + 1 = IterComp Ack M N + 1 IterComp Ack M N + 1 + 1 = Ack M IterComp Ack M N + 1
8 4 5 6 7 syl3anc M 0 N 0 IterComp Ack M N + 1 + 1 = Ack M IterComp Ack M N + 1
9 8 fveq1d M 0 N 0 IterComp Ack M N + 1 + 1 1 = Ack M IterComp Ack M N + 1 1
10 ackfnnn0 M 0 Ack M Fn 0
11 10 adantr M 0 N 0 Ack M Fn 0
12 nn0ex 0 V
13 12 a1i M 0 N 0 0 V
14 ackendofnn0 M 0 Ack M : 0 0
15 14 adantr M 0 N 0 Ack M : 0 0
16 simpr M 0 N 0 N 0
17 13 15 16 itcovalendof M 0 N 0 IterComp Ack M N : 0 0
18 17 ffnd M 0 N 0 IterComp Ack M N Fn 0
19 17 frnd M 0 N 0 ran IterComp Ack M N 0
20 fnco Ack M Fn 0 IterComp Ack M N Fn 0 ran IterComp Ack M N 0 Ack M IterComp Ack M N Fn 0
21 11 18 19 20 syl3anc M 0 N 0 Ack M IterComp Ack M N Fn 0
22 eqidd M 0 N 0 IterComp Ack M N = IterComp Ack M N
23 itcovalsucov Ack M V N 0 IterComp Ack M N = IterComp Ack M N IterComp Ack M N + 1 = Ack M IterComp Ack M N
24 4 16 22 23 syl3anc M 0 N 0 IterComp Ack M N + 1 = Ack M IterComp Ack M N
25 24 fneq1d M 0 N 0 IterComp Ack M N + 1 Fn 0 Ack M IterComp Ack M N Fn 0
26 21 25 mpbird M 0 N 0 IterComp Ack M N + 1 Fn 0
27 1nn0 1 0
28 fvco2 IterComp Ack M N + 1 Fn 0 1 0 Ack M IterComp Ack M N + 1 1 = Ack M IterComp Ack M N + 1 1
29 26 27 28 sylancl M 0 N 0 Ack M IterComp Ack M N + 1 1 = Ack M IterComp Ack M N + 1 1
30 9 29 eqtrd M 0 N 0 IterComp Ack M N + 1 + 1 1 = Ack M IterComp Ack M N + 1 1
31 ackvalsuc1 M 0 N 0 Ack M + 1 N = IterComp Ack M N + 1 1
32 31 eqcomd M 0 N 0 IterComp Ack M N + 1 1 = Ack M + 1 N
33 32 fveq2d M 0 N 0 Ack M IterComp Ack M N + 1 1 = Ack M Ack M + 1 N
34 3 30 33 3eqtrd M 0 N 0 Ack M + 1 N + 1 = Ack M Ack M + 1 N