Metamath Proof Explorer

Theorem ackval40

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

Ref Expression
Assertion ackval40 ⊢ Ack ⁡ 4 ⁡ 0 = 13

Proof

Step Hyp Ref Expression
1 df-4 ⊢ 4 = 3 + 1
2 1 fveq2i ⊢ Ack ⁡ 4 = Ack ⁡ 3 + 1
3 2 fveq1i ⊢ Ack ⁡ 4 ⁡ 0 = Ack ⁡ 3 + 1 ⁡ 0
4 3nn0 ⊢ 3 ∈ ℕ 0
5 ackvalsuc0val ⊢ 3 ∈ ℕ 0 → Ack ⁡ 3 + 1 ⁡ 0 = Ack ⁡ 3 ⁡ 1
6 4 5 ax-mp ⊢ Ack ⁡ 3 + 1 ⁡ 0 = Ack ⁡ 3 ⁡ 1
7 ackval3012 ⊢ Ack ⁡ 3 ⁡ 0 Ack ⁡ 3 ⁡ 1 Ack ⁡ 3 ⁡ 2 = 5 13 29
8 fvex ⊢ Ack ⁡ 3 ⁡ 0 ∈ V
9 fvex ⊢ Ack ⁡ 3 ⁡ 1 ∈ V
10 fvex ⊢ Ack ⁡ 3 ⁡ 2 ∈ V
11 8 9 10 otth ⊢ Ack ⁡ 3 ⁡ 0 Ack ⁡ 3 ⁡ 1 Ack ⁡ 3 ⁡ 2 = 5 13 29 ↔ Ack ⁡ 3 ⁡ 0 = 5 ∧ Ack ⁡ 3 ⁡ 1 = 13 ∧ Ack ⁡ 3 ⁡ 2 = 29
12 11 simp2bi ⊢ Ack ⁡ 3 ⁡ 0 Ack ⁡ 3 ⁡ 1 Ack ⁡ 3 ⁡ 2 = 5 13 29 → Ack ⁡ 3 ⁡ 1 = 13
13 7 12 ax-mp ⊢ Ack ⁡ 3 ⁡ 1 = 13
14 3 6 13 3eqtri ⊢ Ack ⁡ 4 ⁡ 0 = 13