Theorem ackval1012

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

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

Proof

Step	Hyp	Ref	Expression
1		ackval1	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)$$
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	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)\to 0\in {\mathbb{N}}_0$$
8		2nn0	$$⊢2\in {\mathbb{N}}_0$$
9	8	a1i	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)\to 2\in {\mathbb{N}}_0$$
10	1 5 7 9	fvmptd3	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)\to \mathrm{Ack}\left(1\right)\left(0\right)=2$$
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	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)\to 1\in {\mathbb{N}}_0$$
16		3nn0	$$⊢3\in {\mathbb{N}}_0$$
17	16	a1i	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)\to 3\in {\mathbb{N}}_0$$
18	1 13 15 17	fvmptd3	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)\to \mathrm{Ack}\left(1\right)\left(1\right)=3$$
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	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)\to 4\in {\mathbb{N}}_0$$
24	1 21 9 23	fvmptd3	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)\to \mathrm{Ack}\left(1\right)\left(2\right)=4$$
25	10 18 24	oteq123d	$$⊢\mathrm{Ack}\left(1\right)=\left(n\in {\mathbb{N}}_0⟼n+2\right)\to ⟨\mathrm{Ack}\left(1\right)\left(0\right),\mathrm{Ack}\left(1\right)\left(1\right),\mathrm{Ack}\left(1\right)\left(2\right)⟩=⟨2,3,4⟩$$
26	1 25	ax-mp	$$⊢⟨\mathrm{Ack}\left(1\right)\left(0\right),\mathrm{Ack}\left(1\right)\left(1\right),\mathrm{Ack}\left(1\right)\left(2\right)⟩=⟨2,3,4⟩$$