Metamath Proof Explorer


Theorem ackval50

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

Ref Expression
Assertion ackval50 Could not format assertion : No typesetting found for |- ( ( Ack ` 5 ) ` 0 ) = ; ; ; ; 6 5 5 3 3 with typecode |-

Proof

Step Hyp Ref Expression
1 df-5 5 = 4 + 1
2 1 fveq2i Could not format ( Ack ` 5 ) = ( Ack ` ( 4 + 1 ) ) : No typesetting found for |- ( Ack ` 5 ) = ( Ack ` ( 4 + 1 ) ) with typecode |-
3 2 fveq1i Could not format ( ( Ack ` 5 ) ` 0 ) = ( ( Ack ` ( 4 + 1 ) ) ` 0 ) : No typesetting found for |- ( ( Ack ` 5 ) ` 0 ) = ( ( Ack ` ( 4 + 1 ) ) ` 0 ) with typecode |-
4 4nn0 4 0
5 ackvalsuc0val Could not format ( 4 e. NN0 -> ( ( Ack ` ( 4 + 1 ) ) ` 0 ) = ( ( Ack ` 4 ) ` 1 ) ) : No typesetting found for |- ( 4 e. NN0 -> ( ( Ack ` ( 4 + 1 ) ) ` 0 ) = ( ( Ack ` 4 ) ` 1 ) ) with typecode |-
6 4 5 ax-mp Could not format ( ( Ack ` ( 4 + 1 ) ) ` 0 ) = ( ( Ack ` 4 ) ` 1 ) : No typesetting found for |- ( ( Ack ` ( 4 + 1 ) ) ` 0 ) = ( ( Ack ` 4 ) ` 1 ) with typecode |-
7 ackval41 Could not format ( ( Ack ` 4 ) ` 1 ) = ; ; ; ; 6 5 5 3 3 : No typesetting found for |- ( ( Ack ` 4 ) ` 1 ) = ; ; ; ; 6 5 5 3 3 with typecode |-
8 3 6 7 3eqtri Could not format ( ( Ack ` 5 ) ` 0 ) = ; ; ; ; 6 5 5 3 3 : No typesetting found for |- ( ( Ack ` 5 ) ` 0 ) = ; ; ; ; 6 5 5 3 3 with typecode |-