Theorem ackval2012

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

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

Proof

Step	Hyp	Ref	Expression
1		ackval2	Could not format ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) : No typesetting found for |- ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) with typecode |-
2		oveq2	$$⊢n=0\to 2n=2\cdot 0$$
3	2	oveq1d	$$⊢n=0\to 2n+3=2\cdot 0+3$$
4		2t0e0	$$⊢2\cdot 0=0$$
5	4	oveq1i	$$⊢2\cdot 0+3=0+3$$
6		3cn	$$⊢3\in ℂ$$
7	6	addid2i	$$⊢0+3=3$$
8	5 7	eqtri	$$⊢2\cdot 0+3=3$$
9	3 8	eqtrdi	$$⊢n=0\to 2n+3=3$$
10		0nn0	$$⊢0\in {\mathbb{N}}_0$$
11	10	a1i	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 0 e. NN0 ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 0 e. NN0 ) with typecode |-
12		3nn0	$$⊢3\in {\mathbb{N}}_0$$
13	12	a1i	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 3 e. NN0 ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 3 e. NN0 ) with typecode |-
14	1 9 11 13	fvmptd3	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> ( ( Ack ` 2 ) ` 0 ) = 3 ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> ( ( Ack ` 2 ) ` 0 ) = 3 ) with typecode |-
15		oveq2	$$⊢n=1\to 2n=2\cdot 1$$
16	15	oveq1d	$$⊢n=1\to 2n+3=2\cdot 1+3$$
17		2t1e2	$$⊢2\cdot 1=2$$
18	17	oveq1i	$$⊢2\cdot 1+3=2+3$$
19		2cn	$$⊢2\in ℂ$$
20		3p2e5	$$⊢3+2=5$$
21	6 19 20	addcomli	$$⊢2+3=5$$
22	18 21	eqtri	$$⊢2\cdot 1+3=5$$
23	16 22	eqtrdi	$$⊢n=1\to 2n+3=5$$
24		1nn0	$$⊢1\in {\mathbb{N}}_0$$
25	24	a1i	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 1 e. NN0 ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 1 e. NN0 ) with typecode |-
26		5nn0	$$⊢5\in {\mathbb{N}}_0$$
27	26	a1i	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 5 e. NN0 ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 5 e. NN0 ) with typecode |-
28	1 23 25 27	fvmptd3	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> ( ( Ack ` 2 ) ` 1 ) = 5 ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> ( ( Ack ` 2 ) ` 1 ) = 5 ) with typecode |-
29		oveq2	$$⊢n=2\to 2n=2\cdot 2$$
30	29	oveq1d	$$⊢n=2\to 2n+3=2\cdot 2+3$$
31		2t2e4	$$⊢2\cdot 2=4$$
32	31	oveq1i	$$⊢2\cdot 2+3=4+3$$
33		4p3e7	$$⊢4+3=7$$
34	32 33	eqtri	$$⊢2\cdot 2+3=7$$
35	30 34	eqtrdi	$$⊢n=2\to 2n+3=7$$
36		2nn0	$$⊢2\in {\mathbb{N}}_0$$
37	36	a1i	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 2 e. NN0 ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 2 e. NN0 ) with typecode |-
38		7nn0	$$⊢7\in {\mathbb{N}}_0$$
39	38	a1i	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 7 e. NN0 ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 7 e. NN0 ) with typecode |-
40	1 35 37 39	fvmptd3	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> ( ( Ack ` 2 ) ` 2 ) = 7 ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> ( ( Ack ` 2 ) ` 2 ) = 7 ) with typecode |-
41	14 28 40	oteq123d	Could not format ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> <. ( ( Ack ` 2 ) ` 0 ) , ( ( Ack ` 2 ) ` 1 ) , ( ( Ack ` 2 ) ` 2 ) >. = <. 3 , 5 , 7 >. ) : No typesetting found for |- ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> <. ( ( Ack ` 2 ) ` 0 ) , ( ( Ack ` 2 ) ` 1 ) , ( ( Ack ` 2 ) ` 2 ) >. = <. 3 , 5 , 7 >. ) with typecode |-
42	1 41	ax-mp	Could not format <. ( ( Ack ` 2 ) ` 0 ) , ( ( Ack ` 2 ) ` 1 ) , ( ( Ack ` 2 ) ` 2 ) >. = <. 3 , 5 , 7 >. : No typesetting found for |- <. ( ( Ack ` 2 ) ` 0 ) , ( ( Ack ` 2 ) ` 1 ) , ( ( Ack ` 2 ) ` 2 ) >. = <. 3 , 5 , 7 >. with typecode |-