Metamath Proof Explorer

Theorem ackvalsuc1

Description: The Ackermann function at a successor of the first argument and an arbitrary second argument. (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 4-May-2024)

Ref Expression
Assertion ackvalsuc1 ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 → Ack ⁡ M + 1 ⁡ N = IterComp ⁡ Ack ⁡ M ⁡ N + 1 ⁡ 1

Proof

Step Hyp Ref Expression
1 ackvalsuc1mpt ⊢ M ∈ ℕ 0 → Ack ⁡ M + 1 = n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1
2 1 adantr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 → Ack ⁡ M + 1 = n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1
3 fvoveq1 ⊢ n = N → IterComp ⁡ Ack ⁡ M ⁡ n + 1 = IterComp ⁡ Ack ⁡ M ⁡ N + 1
4 3 fveq1d ⊢ n = N → IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1 = IterComp ⁡ Ack ⁡ M ⁡ N + 1 ⁡ 1
5 4 adantl ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ n = N → IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1 = IterComp ⁡ Ack ⁡ M ⁡ N + 1 ⁡ 1
6 simpr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 → N ∈ ℕ 0
7 fvexd ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 → IterComp ⁡ Ack ⁡ M ⁡ N + 1 ⁡ 1 ∈ V
8 2 5 6 7 fvmptd ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 → Ack ⁡ M + 1 ⁡ N = IterComp ⁡ Ack ⁡ M ⁡ N + 1 ⁡ 1