Theorem ackval40

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

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

Proof

Step	Hyp	Ref	Expression
1		df-4	$$⊢4=3+1$$
2	1	fveq2i	Could not format ( Ack ` 4 ) = ( Ack ` ( 3 + 1 ) ) : No typesetting found for |- ( Ack ` 4 ) = ( Ack ` ( 3 + 1 ) ) with typecode |-
3	2	fveq1i	Could not format ( ( Ack ` 4 ) ` 0 ) = ( ( Ack ` ( 3 + 1 ) ) ` 0 ) : No typesetting found for |- ( ( Ack ` 4 ) ` 0 ) = ( ( Ack ` ( 3 + 1 ) ) ` 0 ) with typecode |-
4		3nn0	$$⊢3\in {\mathbb{N}}_0$$
5		ackvalsuc0val	Could not format ( 3 e. NN0 -> ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ( ( Ack ` 3 ) ` 1 ) ) : No typesetting found for |- ( 3 e. NN0 -> ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ( ( Ack ` 3 ) ` 1 ) ) with typecode |-
6	4 5	ax-mp	Could not format ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ( ( Ack ` 3 ) ` 1 ) : No typesetting found for |- ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ( ( Ack ` 3 ) ` 1 ) with typecode |-
7		ackval3012	Could not format <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. : No typesetting found for |- <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. with typecode |-
8		fvex	Could not format ( ( Ack ` 3 ) ` 0 ) e. _V : No typesetting found for |- ( ( Ack ` 3 ) ` 0 ) e. _V with typecode |-
9		fvex	Could not format ( ( Ack ` 3 ) ` 1 ) e. _V : No typesetting found for |- ( ( Ack ` 3 ) ` 1 ) e. _V with typecode |-
10		fvex	Could not format ( ( Ack ` 3 ) ` 2 ) e. _V : No typesetting found for |- ( ( Ack ` 3 ) ` 2 ) e. _V with typecode |-
11	8 9 10	otth	Could not format ( <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. <-> ( ( ( Ack ` 3 ) ` 0 ) = 5 /\ ( ( Ack ` 3 ) ` 1 ) = ; 1 3 /\ ( ( Ack ` 3 ) ` 2 ) = ; 2 9 ) ) : No typesetting found for |- ( <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. <-> ( ( ( Ack ` 3 ) ` 0 ) = 5 /\ ( ( Ack ` 3 ) ` 1 ) = ; 1 3 /\ ( ( Ack ` 3 ) ` 2 ) = ; 2 9 ) ) with typecode |-
12	11	simp2bi	Could not format ( <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. -> ( ( Ack ` 3 ) ` 1 ) = ; 1 3 ) : No typesetting found for |- ( <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. -> ( ( Ack ` 3 ) ` 1 ) = ; 1 3 ) with typecode |-
13	7 12	ax-mp	Could not format ( ( Ack ` 3 ) ` 1 ) = ; 1 3 : No typesetting found for |- ( ( Ack ` 3 ) ` 1 ) = ; 1 3 with typecode |-
14	3 6 13	3eqtri	Could not format ( ( Ack ` 4 ) ` 0 ) = ; 1 3 : No typesetting found for |- ( ( Ack ` 4 ) ` 0 ) = ; 1 3 with typecode |-