Metamath Proof Explorer


Theorem ackval50

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

Ref Expression
Assertion ackval50 ( ( Ack ‘ 5 ) ‘ 0 ) = 6 5 5 3 3

Proof

Step Hyp Ref Expression
1 df-5 5 = ( 4 + 1 )
2 1 fveq2i ( Ack ‘ 5 ) = ( Ack ‘ ( 4 + 1 ) )
3 2 fveq1i ( ( Ack ‘ 5 ) ‘ 0 ) = ( ( Ack ‘ ( 4 + 1 ) ) ‘ 0 )
4 4nn0 4 ∈ ℕ0
5 ackvalsuc0val ( 4 ∈ ℕ0 → ( ( Ack ‘ ( 4 + 1 ) ) ‘ 0 ) = ( ( Ack ‘ 4 ) ‘ 1 ) )
6 4 5 ax-mp ( ( Ack ‘ ( 4 + 1 ) ) ‘ 0 ) = ( ( Ack ‘ 4 ) ‘ 1 )
7 ackval41 ( ( Ack ‘ 4 ) ‘ 1 ) = 6 5 5 3 3
8 3 6 7 3eqtri ( ( Ack ‘ 5 ) ‘ 0 ) = 6 5 5 3 3