Step |
Hyp |
Ref |
Expression |
1 |
|
df-5 |
|
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 |
|
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 |- |