Theorem ackval2012

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

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

Proof

Step	Hyp	Ref	Expression
1		ackval2	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)$$
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	addlidi	$$⊢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	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to 0\in {\mathbb{N}}_0$$
12		3nn0	$$⊢3\in {\mathbb{N}}_0$$
13	12	a1i	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to 3\in {\mathbb{N}}_0$$
14	1 9 11 13	fvmptd3	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to \mathrm{Ack}\left(2\right)\left(0\right)=3$$
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	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to 1\in {\mathbb{N}}_0$$
26		5nn0	$$⊢5\in {\mathbb{N}}_0$$
27	26	a1i	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to 5\in {\mathbb{N}}_0$$
28	1 23 25 27	fvmptd3	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to \mathrm{Ack}\left(2\right)\left(1\right)=5$$
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	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to 2\in {\mathbb{N}}_0$$
38		7nn0	$$⊢7\in {\mathbb{N}}_0$$
39	38	a1i	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to 7\in {\mathbb{N}}_0$$
40	1 35 37 39	fvmptd3	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to \mathrm{Ack}\left(2\right)\left(2\right)=7$$
41	14 28 40	oteq123d	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)\to ⟨\mathrm{Ack}\left(2\right)\left(0\right),\mathrm{Ack}\left(2\right)\left(1\right),\mathrm{Ack}\left(2\right)\left(2\right)⟩=⟨3,5,7⟩$$
42	1 41	ax-mp	$$⊢⟨\mathrm{Ack}\left(2\right)\left(0\right),\mathrm{Ack}\left(2\right)\left(1\right),\mathrm{Ack}\left(2\right)\left(2\right)⟩=⟨3,5,7⟩$$