Metamath Proof Explorer


Theorem ackval0

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

Ref Expression
Assertion ackval0 Ack 0 = n 0 n + 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 0 = seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i 0
3 0z 0
4 seq1 0 seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i 0 = i 0 if i = 0 n 0 n + 1 i 0
5 3 4 ax-mp seq 0 f V , j V n 0 IterComp f n + 1 1 i 0 if i = 0 n 0 n + 1 i 0 = i 0 if i = 0 n 0 n + 1 i 0
6 0nn0 0 0
7 iftrue i = 0 if i = 0 n 0 n + 1 i = n 0 n + 1
8 eqid i 0 if i = 0 n 0 n + 1 i = i 0 if i = 0 n 0 n + 1 i
9 nn0ex 0 V
10 9 mptex n 0 n + 1 V
11 7 8 10 fvmpt 0 0 i 0 if i = 0 n 0 n + 1 i 0 = n 0 n + 1
12 6 11 ax-mp i 0 if i = 0 n 0 n + 1 i 0 = n 0 n + 1
13 2 5 12 3eqtri Ack 0 = n 0 n + 1