Theorem ackval3012

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

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

Proof

Step	Hyp	Ref	Expression
1		ackval3	Could not format ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) : No typesetting found for |- ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) with typecode |-
2		oveq1	$$⊢n=0\to n+3=0+3$$
3		3cn	$$⊢3\in ℂ$$
4	3	addlidi	$$⊢0+3=3$$
5	2 4	eqtrdi	$$⊢n=0\to n+3=3$$
6	5	oveq2d	$$⊢n=0\to 2^{n+3}=2^3$$
7	6	oveq1d	$$⊢n=0\to 2^{n+3}-3=2^3-3$$
8		cu2	$$⊢2^3=8$$
9	8	oveq1i	$$⊢2^3-3=8-3$$
10		5cn	$$⊢5\in ℂ$$
11		5p3e8	$$⊢5+3=8$$
12	11	eqcomi	$$⊢8=5+3$$
13	10 3 12	mvrraddi	$$⊢8-3=5$$
14	9 13	eqtri	$$⊢2^3-3=5$$
15	7 14	eqtrdi	$$⊢n=0\to 2^{n+3}-3=5$$
16		0nn0	$$⊢0\in {\mathbb{N}}_0$$
17	16	a1i	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 0 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 0 e. NN0 ) with typecode |-
18		5nn0	$$⊢5\in {\mathbb{N}}_0$$
19	18	a1i	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 5 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 5 e. NN0 ) with typecode |-
20	1 15 17 19	fvmptd3	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 0 ) = 5 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 0 ) = 5 ) with typecode |-
21		oveq1	$$⊢n=1\to n+3=1+3$$
22		ax-1cn	$$⊢1\in ℂ$$
23		3p1e4	$$⊢3+1=4$$
24	3 22 23	addcomli	$$⊢1+3=4$$
25	21 24	eqtrdi	$$⊢n=1\to n+3=4$$
26	25	oveq2d	$$⊢n=1\to 2^{n+3}=2^4$$
27	26	oveq1d	$$⊢n=1\to 2^{n+3}-3=2^4-3$$
28		2exp4	$$⊢2^4=16$$
29	28	oveq1i	$$⊢2^4-3=16-3$$
30		1nn0	$$⊢1\in {\mathbb{N}}_0$$
31		3nn0	$$⊢3\in {\mathbb{N}}_0$$
32	30 31	deccl	$$⊢13\in {\mathbb{N}}_0$$
33	32	nn0cni	$$⊢13\in ℂ$$
34		eqid	$$⊢13=13$$
35		3p3e6	$$⊢3+3=6$$
36	30 31 31 34 35	decaddi	$$⊢13+3=16$$
37	36	eqcomi	$$⊢16=13+3$$
38	33 3 37	mvrraddi	$$⊢16-3=13$$
39	29 38	eqtri	$$⊢2^4-3=13$$
40	27 39	eqtrdi	$$⊢n=1\to 2^{n+3}-3=13$$
41	30	a1i	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 1 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 1 e. NN0 ) with typecode |-
42	32	a1i	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 1 3 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 1 3 e. NN0 ) with typecode |-
43	1 40 41 42	fvmptd3	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 1 ) = ; 1 3 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 1 ) = ; 1 3 ) with typecode |-
44		oveq1	$$⊢n=2\to n+3=2+3$$
45		2cn	$$⊢2\in ℂ$$
46		3p2e5	$$⊢3+2=5$$
47	3 45 46	addcomli	$$⊢2+3=5$$
48	44 47	eqtrdi	$$⊢n=2\to n+3=5$$
49	48	oveq2d	$$⊢n=2\to 2^{n+3}=2^5$$
50	49	oveq1d	$$⊢n=2\to 2^{n+3}-3=2^5-3$$
51		2exp5	$$⊢2^5=32$$
52	51	oveq1i	$$⊢2^5-3=32-3$$
53		2nn0	$$⊢2\in {\mathbb{N}}_0$$
54		9nn0	$$⊢9\in {\mathbb{N}}_0$$
55	53 54	deccl	$$⊢29\in {\mathbb{N}}_0$$
56	55	nn0cni	$$⊢29\in ℂ$$
57		eqid	$$⊢29=29$$
58		2p1e3	$$⊢2+1=3$$
59		9p3e12	$$⊢9+3=12$$
60	53 54 31 57 58 53 59	decaddci	$$⊢29+3=32$$
61	60	eqcomi	$$⊢32=29+3$$
62	56 3 61	mvrraddi	$$⊢32-3=29$$
63	52 62	eqtri	$$⊢2^5-3=29$$
64	50 63	eqtrdi	$$⊢n=2\to 2^{n+3}-3=29$$
65	53	a1i	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 2 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 2 e. NN0 ) with typecode |-
66	55	a1i	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 2 9 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 2 9 e. NN0 ) with typecode |-
67	1 64 65 66	fvmptd3	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 2 ) = ; 2 9 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 2 ) = ; 2 9 ) with typecode |-
68	20 43 67	oteq123d	Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. ) with typecode |-
69	1 68	ax-mp	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 |-