This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ackvalsuc0val

Description: The Ackermann function at a successor (of the first argument). This is the second equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024)

Ref Expression
Assertion ackvalsuc0val ⊢ M ∈ ℕ 0 → Ack ⁡ M + 1 ⁡ 0 = Ack ⁡ M ⁡ 1

Proof

Step Hyp Ref Expression
1 0nn0 ⊢ 0 ∈ ℕ 0
2 ackvalsuc1 ⊢ M ∈ ℕ 0 ∧ 0 ∈ ℕ 0 → Ack ⁡ M + 1 ⁡ 0 = IterComp ⁡ Ack ⁡ M ⁡ 0 + 1 ⁡ 1
3 1 2 mpan2 ⊢ M ∈ ℕ 0 → Ack ⁡ M + 1 ⁡ 0 = IterComp ⁡ Ack ⁡ M ⁡ 0 + 1 ⁡ 1
4 0p1e1 ⊢ 0 + 1 = 1
5 4 a1i ⊢ M ∈ ℕ 0 → 0 + 1 = 1
6 5 fveq2d ⊢ M ∈ ℕ 0 → IterComp ⁡ Ack ⁡ M ⁡ 0 + 1 = IterComp ⁡ Ack ⁡ M ⁡ 1
7 ackfnnn0 ⊢ M ∈ ℕ 0 → Ack ⁡ M Fn ℕ 0
8 fnfun ⊢ Ack ⁡ M Fn ℕ 0 → Fun ⁡ Ack ⁡ M
9 funrel ⊢ Fun ⁡ Ack ⁡ M → Rel ⁡ Ack ⁡ M
10 7 8 9 3syl ⊢ M ∈ ℕ 0 → Rel ⁡ Ack ⁡ M
11 fvex ⊢ Ack ⁡ M ∈ V
12 itcoval1 ⊢ Rel ⁡ Ack ⁡ M ∧ Ack ⁡ M ∈ V → IterComp ⁡ Ack ⁡ M ⁡ 1 = Ack ⁡ M
13 10 11 12 sylancl ⊢ M ∈ ℕ 0 → IterComp ⁡ Ack ⁡ M ⁡ 1 = Ack ⁡ M
14 6 13 eqtrd ⊢ M ∈ ℕ 0 → IterComp ⁡ Ack ⁡ M ⁡ 0 + 1 = Ack ⁡ M
15 14 fveq1d ⊢ M ∈ ℕ 0 → IterComp ⁡ Ack ⁡ M ⁡ 0 + 1 ⁡ 1 = Ack ⁡ M ⁡ 1
16 3 15 eqtrd ⊢ M ∈ ℕ 0 → Ack ⁡ M + 1 ⁡ 0 = Ack ⁡ M ⁡ 1