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 ( 𝑀 ∈ ℕ0 → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 0 ) = ( ( Ack ‘ 𝑀 ) ‘ 1 ) )

Proof

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