Theorem ackval41a

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

	Ref	Expression
Assertion	ackval41a	$$⊢\mathrm{Ack}\left(4\right)\left(1\right)=2^{16}-3$$

Proof

Step	Hyp	Ref	Expression
1		df-4	$$⊢4=3+1$$
2	1	fveq2i	$$⊢\mathrm{Ack}\left(4\right)=\mathrm{Ack}\left(3+1\right)$$
3		1e0p1	$$⊢1=0+1$$
4	2 3	fveq12i	$$⊢\mathrm{Ack}\left(4\right)\left(1\right)=\mathrm{Ack}\left(3+1\right)\left(0+1\right)$$
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7		ackvalsucsucval	$$⊢\left(3\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to \mathrm{Ack}\left(3+1\right)\left(0+1\right)=\mathrm{Ack}\left(3\right)\left(\mathrm{Ack}\left(3+1\right)\left(0\right)\right)$$
8	5 6 7	mp2an	$$⊢\mathrm{Ack}\left(3+1\right)\left(0+1\right)=\mathrm{Ack}\left(3\right)\left(\mathrm{Ack}\left(3+1\right)\left(0\right)\right)$$
9		3p1e4	$$⊢3+1=4$$
10	9	fveq2i	$$⊢\mathrm{Ack}\left(3+1\right)=\mathrm{Ack}\left(4\right)$$
11	10	fveq1i	$$⊢\mathrm{Ack}\left(3+1\right)\left(0\right)=\mathrm{Ack}\left(4\right)\left(0\right)$$
12		ackval40	$$⊢\mathrm{Ack}\left(4\right)\left(0\right)=13$$
13	11 12	eqtri	$$⊢\mathrm{Ack}\left(3+1\right)\left(0\right)=13$$
14	13	fveq2i	$$⊢\mathrm{Ack}\left(3\right)\left(\mathrm{Ack}\left(3+1\right)\left(0\right)\right)=\mathrm{Ack}\left(3\right)\left(13\right)$$
15		1nn0	$$⊢1\in {\mathbb{N}}_0$$
16	15 5	deccl	$$⊢13\in {\mathbb{N}}_0$$
17		oveq1	$$⊢n=13\to n+3=13+3$$
18	17	oveq2d	$$⊢n=13\to 2^{n+3}=2^{13+3}$$
19	18	oveq1d	$$⊢n=13\to 2^{n+3}-3=2^{13+3}-3$$
20		eqid	$$⊢13=13$$
21		3p3e6	$$⊢3+3=6$$
22	15 5 5 20 21	decaddi	$$⊢13+3=16$$
23	22	oveq2i	$$⊢2^{13+3}=2^{16}$$
24	23	oveq1i	$$⊢2^{13+3}-3=2^{16}-3$$
25	19 24	eqtrdi	$$⊢n=13\to 2^{n+3}-3=2^{16}-3$$
26		ackval3	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)$$
27		ovex	$$⊢2^{16}-3\in \mathrm{V}$$
28	25 26 27	fvmpt	$$⊢13\in {\mathbb{N}}_0\to \mathrm{Ack}\left(3\right)\left(13\right)=2^{16}-3$$
29	16 28	ax-mp	$$⊢\mathrm{Ack}\left(3\right)\left(13\right)=2^{16}-3$$
30	14 29	eqtri	$$⊢\mathrm{Ack}\left(3\right)\left(\mathrm{Ack}\left(3+1\right)\left(0\right)\right)=2^{16}-3$$
31	8 30	eqtri	$$⊢\mathrm{Ack}\left(3+1\right)\left(0+1\right)=2^{16}-3$$
32	4 31	eqtri	$$⊢\mathrm{Ack}\left(4\right)\left(1\right)=2^{16}-3$$