Metamath Proof Explorer


Theorem ackval1

Description: The Ackermann function at 1. (Contributed by AV, 4-May-2024)

Ref Expression
Assertion ackval1 Ack 1 = n 0 n + 2

Proof

Step Hyp Ref Expression
1 1e0p1 1 = 0 + 1
2 1 fveq2i Ack 1 = Ack 0 + 1
3 0nn0 0 0
4 ackvalsuc1mpt 0 0 Ack 0 + 1 = n 0 IterComp Ack 0 n + 1 1
5 3 4 ax-mp Ack 0 + 1 = n 0 IterComp Ack 0 n + 1 1
6 peano2nn0 n 0 n + 1 0
7 1nn0 1 0
8 ackval0 Ack 0 = i 0 i + 1
9 8 itcovalpc n + 1 0 1 0 IterComp Ack 0 n + 1 = i 0 i + 1 n + 1
10 6 7 9 sylancl n 0 IterComp Ack 0 n + 1 = i 0 i + 1 n + 1
11 nn0cn n + 1 0 n + 1
12 6 11 syl n 0 n + 1
13 12 mullidd n 0 1 n + 1 = n + 1
14 13 oveq2d n 0 i + 1 n + 1 = i + n + 1
15 14 mpteq2dv n 0 i 0 i + 1 n + 1 = i 0 i + n + 1
16 10 15 eqtrd n 0 IterComp Ack 0 n + 1 = i 0 i + n + 1
17 16 fveq1d n 0 IterComp Ack 0 n + 1 1 = i 0 i + n + 1 1
18 eqidd n 0 i 0 i + n + 1 = i 0 i + n + 1
19 oveq1 i = 1 i + n + 1 = 1 + n + 1
20 19 adantl n 0 i = 1 i + n + 1 = 1 + n + 1
21 7 a1i n 0 1 0
22 ovexd n 0 1 + n + 1 V
23 18 20 21 22 fvmptd n 0 i 0 i + n + 1 1 = 1 + n + 1
24 1cnd n 0 1
25 nn0cn n 0 n
26 peano2cn n n + 1
27 25 26 syl n 0 n + 1
28 24 27 addcomd n 0 1 + n + 1 = n + 1 + 1
29 25 24 24 addassd n 0 n + 1 + 1 = n + 1 + 1
30 1p1e2 1 + 1 = 2
31 30 oveq2i n + 1 + 1 = n + 2
32 31 a1i n 0 n + 1 + 1 = n + 2
33 28 29 32 3eqtrd n 0 1 + n + 1 = n + 2
34 17 23 33 3eqtrd n 0 IterComp Ack 0 n + 1 1 = n + 2
35 34 mpteq2ia n 0 IterComp Ack 0 n + 1 1 = n 0 n + 2
36 2 5 35 3eqtri Ack 1 = n 0 n + 2