Metamath Proof Explorer

Definition df-ack

Description: Define the Ackermann function (recursively). (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 2-May-2024)

Ref Expression
Assertion df-ack Ack = seq 0 ( ( 𝑓 ∈ V , 𝑗 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cack ⊢ Ack
1 cc0 ⊢ 0
2 vf ⊢ 𝑓
3 cvv ⊢ V
4 vj ⊢ 𝑗
5 vn ⊢ 𝑛
6 cn0 ⊢ ℕ0
7 citco ⊢ IterComp
8 2 cv ⊢ 𝑓
9 8 7 cfv ⊢ ( IterComp ‘ 𝑓 )
10 5 cv ⊢ 𝑛
11 caddc ⊢ +
12 c1 ⊢ 1
13 10 12 11 co ⊢ ( 𝑛 + 1 )
14 13 9 cfv ⊢ ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) )
15 12 14 cfv ⊢ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 )
16 5 6 15 cmpt ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) )
17 2 4 3 3 16 cmpo ⊢ ( 𝑓 ∈ V , 𝑗 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )
18 vi ⊢ 𝑖
19 18 cv ⊢ 𝑖
20 19 1 wceq ⊢ 𝑖 = 0
21 5 6 13 cmpt ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) )
22 20 21 19 cif ⊢ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 )
23 18 6 22 cmpt ⊢ ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) )
24 17 23 1 cseq ⊢ seq 0 ( ( 𝑓 ∈ V , 𝑗 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) )
25 0 24 wceq ⊢ Ack = seq 0 ( ( 𝑓 ∈ V , 𝑗 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) , 𝑖 ) ) )