Theorem ackval0012

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

	Ref	Expression
Assertion	ackval0012	Could not format assertion : No typesetting found for |- <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ackval0	Could not format ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) : No typesetting found for |- ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) with typecode |-
2		oveq1	$$⊢n=0\to n+1=0+1$$
3		0p1e1	$$⊢0+1=1$$
4	2 3	eqtrdi	$$⊢n=0\to n+1=1$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	5	a1i	Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 0 e. NN0 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 0 e. NN0 ) with typecode |-
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8	7	a1i	Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 1 e. NN0 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 1 e. NN0 ) with typecode |-
9	1 4 6 8	fvmptd3	Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 0 ) = 1 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 0 ) = 1 ) with typecode |-
10		oveq1	$$⊢n=1\to n+1=1+1$$
11		1p1e2	$$⊢1+1=2$$
12	10 11	eqtrdi	$$⊢n=1\to n+1=2$$
13		2nn0	$$⊢2\in {\mathbb{N}}_0$$
14	13	a1i	Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 2 e. NN0 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 2 e. NN0 ) with typecode |-
15	1 12 8 14	fvmptd3	Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 1 ) = 2 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 1 ) = 2 ) with typecode |-
16		oveq1	$$⊢n=2\to n+1=2+1$$
17		2p1e3	$$⊢2+1=3$$
18	16 17	eqtrdi	$$⊢n=2\to n+1=3$$
19		3nn0	$$⊢3\in {\mathbb{N}}_0$$
20	19	a1i	Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 3 e. NN0 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 3 e. NN0 ) with typecode |-
21	1 18 14 20	fvmptd3	Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 2 ) = 3 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 2 ) = 3 ) with typecode |-
22	9 15 21	oteq123d	Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. ) with typecode |-
23	1 22	ax-mp	Could not format <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. : No typesetting found for |- <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. with typecode |-