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 ) = 1 3

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 , 1 3 , 2 9 ⟩
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 , 1 3 , 2 9 ⟩ ↔ ( ( ( Ack ‘ 3 ) ‘ 0 ) = 5 ∧ ( ( Ack ‘ 3 ) ‘ 1 ) = 1 3 ∧ ( ( Ack ‘ 3 ) ‘ 2 ) = 2 9 ) )
12 11 simp2bi ⊢ ( ⟨ ( ( Ack ‘ 3 ) ‘ 0 ) , ( ( Ack ‘ 3 ) ‘ 1 ) , ( ( Ack ‘ 3 ) ‘ 2 ) ⟩ = ⟨ 5 , 1 3 , 2 9 ⟩ → ( ( Ack ‘ 3 ) ‘ 1 ) = 1 3 )
13 7 12 ax-mp ⊢ ( ( Ack ‘ 3 ) ‘ 1 ) = 1 3
14 3 6 13 3eqtri ⊢ ( ( Ack ‘ 4 ) ‘ 0 ) = 1 3