Theorem ackval1012

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

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

Proof

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