Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
The Ackermann function
ackfnnn0
Metamath Proof Explorer
Description: The Ackermann function at any nonnegative integer is a function on the
nonnegative integers. (Contributed by AV , 4-May-2024) (Proof shortened by AV , 8-May-2024)
Ref
Expression
Assertion
ackfnnn0
⊢ M ∈ ℕ 0 → Ack ⁡ M Fn ℕ 0
Proof
Step
Hyp
Ref
Expression
1
ackendofnn0
⊢ M ∈ ℕ 0 → Ack ⁡ M : ℕ 0 ⟶ ℕ 0
2
ffn
⊢ Ack ⁡ M : ℕ 0 ⟶ ℕ 0 → Ack ⁡ M Fn ℕ 0
3
1 2
syl
⊢ M ∈ ℕ 0 → Ack ⁡ M Fn ℕ 0