Metamath Proof Explorer


Theorem ackval3

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

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

Proof

Step Hyp Ref Expression
1 df-3 3 = 2 + 1
2 1 fveq2i Ack 3 = Ack 2 + 1
3 2nn0 2 0
4 ackvalsuc1mpt 2 0 Ack 2 + 1 = n 0 IterComp Ack 2 n + 1 1
5 3 4 ax-mp Ack 2 + 1 = n 0 IterComp Ack 2 n + 1 1
6 peano2nn0 n 0 n + 1 0
7 3nn0 3 0
8 ackval2 Ack 2 = i 0 2 i + 3
9 8 itcovalt2 n + 1 0 3 0 IterComp Ack 2 n + 1 = i 0 i + 3 2 n + 1 3
10 6 7 9 sylancl n 0 IterComp Ack 2 n + 1 = i 0 i + 3 2 n + 1 3
11 10 fveq1d n 0 IterComp Ack 2 n + 1 1 = i 0 i + 3 2 n + 1 3 1
12 eqidd n 0 i 0 i + 3 2 n + 1 3 = i 0 i + 3 2 n + 1 3
13 oveq1 i = 1 i + 3 = 1 + 3
14 3cn 3
15 ax-1cn 1
16 3p1e4 3 + 1 = 4
17 14 15 16 addcomli 1 + 3 = 4
18 13 17 eqtrdi i = 1 i + 3 = 4
19 18 oveq1d i = 1 i + 3 2 n + 1 = 4 2 n + 1
20 19 oveq1d i = 1 i + 3 2 n + 1 3 = 4 2 n + 1 3
21 20 adantl n 0 i = 1 i + 3 2 n + 1 3 = 4 2 n + 1 3
22 1nn0 1 0
23 22 a1i n 0 1 0
24 ovexd n 0 4 2 n + 1 3 V
25 12 21 23 24 fvmptd n 0 i 0 i + 3 2 n + 1 3 1 = 4 2 n + 1 3
26 sq2 2 2 = 4
27 26 eqcomi 4 = 2 2
28 27 a1i n 0 4 = 2 2
29 28 oveq1d n 0 4 2 n + 1 = 2 2 2 n + 1
30 2cnd n 0 2
31 3 a1i n 0 2 0
32 30 6 31 expaddd n 0 2 2 + n + 1 = 2 2 2 n + 1
33 nn0cn n 0 n
34 1cnd n 0 1
35 30 33 34 add12d n 0 2 + n + 1 = n + 2 + 1
36 2p1e3 2 + 1 = 3
37 36 oveq2i n + 2 + 1 = n + 3
38 35 37 eqtrdi n 0 2 + n + 1 = n + 3
39 38 oveq2d n 0 2 2 + n + 1 = 2 n + 3
40 29 32 39 3eqtr2d n 0 4 2 n + 1 = 2 n + 3
41 40 oveq1d n 0 4 2 n + 1 3 = 2 n + 3 3
42 11 25 41 3eqtrd n 0 IterComp Ack 2 n + 1 1 = 2 n + 3 3
43 42 mpteq2ia n 0 IterComp Ack 2 n + 1 1 = n 0 2 n + 3 3
44 2 5 43 3eqtri Ack 3 = n 0 2 n + 3 3