Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
The Ackermann function
ackval0
Next ⟩
ackval1
Metamath Proof Explorer
Ascii
Unicode
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