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\in {\mathbb{N}}_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 |-