Metamath Proof Explorer


Theorem ackval2

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

Ref Expression
Assertion ackval2 Ack 2 = n 0 2 n + 3

Proof

Step Hyp Ref Expression
1 df-2 2 = 1 + 1
2 1 fveq2i Ack 2 = Ack 1 + 1
3 1nn0 1 0
4 ackvalsuc1mpt 1 0 Ack 1 + 1 = n 0 IterComp Ack 1 n + 1 1
5 3 4 ax-mp Ack 1 + 1 = n 0 IterComp Ack 1 n + 1 1
6 peano2nn0 n 0 n + 1 0
7 2nn0 2 0
8 ackval1 Ack 1 = i 0 i + 2
9 8 itcovalpc n + 1 0 2 0 IterComp Ack 1 n + 1 = i 0 i + 2 n + 1
10 6 7 9 sylancl n 0 IterComp Ack 1 n + 1 = i 0 i + 2 n + 1
11 10 fveq1d n 0 IterComp Ack 1 n + 1 1 = i 0 i + 2 n + 1 1
12 eqidd n 0 i 0 i + 2 n + 1 = i 0 i + 2 n + 1
13 oveq1 i = 1 i + 2 n + 1 = 1 + 2 n + 1
14 13 adantl n 0 i = 1 i + 2 n + 1 = 1 + 2 n + 1
15 3 a1i n 0 1 0
16 ovexd n 0 1 + 2 n + 1 V
17 12 14 15 16 fvmptd n 0 i 0 i + 2 n + 1 1 = 1 + 2 n + 1
18 nn0cn n 0 n
19 1cnd n 1
20 2cnd n 2
21 peano2cn n n + 1
22 20 21 mulcld n 2 n + 1
23 19 22 addcomd n 1 + 2 n + 1 = 2 n + 1 + 1
24 id n n
25 20 24 19 adddid n 2 n + 1 = 2 n + 2 1
26 25 oveq1d n 2 n + 1 + 1 = 2 n + 2 1 + 1
27 20 24 mulcld n 2 n
28 20 19 mulcld n 2 1
29 27 28 19 addassd n 2 n + 2 1 + 1 = 2 n + 2 1 + 1
30 2t1e2 2 1 = 2
31 30 oveq1i 2 1 + 1 = 2 + 1
32 2p1e3 2 + 1 = 3
33 31 32 eqtri 2 1 + 1 = 3
34 33 a1i n 2 1 + 1 = 3
35 34 oveq2d n 2 n + 2 1 + 1 = 2 n + 3
36 29 35 eqtrd n 2 n + 2 1 + 1 = 2 n + 3
37 23 26 36 3eqtrd n 1 + 2 n + 1 = 2 n + 3
38 18 37 syl n 0 1 + 2 n + 1 = 2 n + 3
39 11 17 38 3eqtrd n 0 IterComp Ack 1 n + 1 1 = 2 n + 3
40 39 mpteq2ia n 0 IterComp Ack 1 n + 1 1 = n 0 2 n + 3
41 2 5 40 3eqtri Ack 2 = n 0 2 n + 3