Theorem ackval3012

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

	Ref	Expression
Assertion	ackval3012	$$⊢⟨\mathrm{Ack}\left(3\right)\left(0\right),\mathrm{Ack}\left(3\right)\left(1\right),\mathrm{Ack}\left(3\right)\left(2\right)⟩=⟨5,13,29⟩$$

Proof

Step	Hyp	Ref	Expression
1		ackval3	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)$$
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	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to 0\in {\mathbb{N}}_0$$
18		5nn0	$$⊢5\in {\mathbb{N}}_0$$
19	18	a1i	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to 5\in {\mathbb{N}}_0$$
20	1 15 17 19	fvmptd3	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to \mathrm{Ack}\left(3\right)\left(0\right)=5$$
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	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to 1\in {\mathbb{N}}_0$$
42	32	a1i	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to 13\in {\mathbb{N}}_0$$
43	1 40 41 42	fvmptd3	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to \mathrm{Ack}\left(3\right)\left(1\right)=13$$
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	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to 2\in {\mathbb{N}}_0$$
66	55	a1i	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to 29\in {\mathbb{N}}_0$$
67	1 64 65 66	fvmptd3	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to \mathrm{Ack}\left(3\right)\left(2\right)=29$$
68	20 43 67	oteq123d	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)\to ⟨\mathrm{Ack}\left(3\right)\left(0\right),\mathrm{Ack}\left(3\right)\left(1\right),\mathrm{Ack}\left(3\right)\left(2\right)⟩=⟨5,13,29⟩$$
69	1 68	ax-mp	$$⊢⟨\mathrm{Ack}\left(3\right)\left(0\right),\mathrm{Ack}\left(3\right)\left(1\right),\mathrm{Ack}\left(3\right)\left(2\right)⟩=⟨5,13,29⟩$$