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 e. NN0
5 ackvalsuc0val 
 |-  ( 4 e. NN0 -> ( ( 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