Theorem ackval42

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

	Ref	Expression
Assertion	ackval42	$$⊢\mathrm{Ack}\left(4\right)\left(2\right)=2^{65536}-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		df-2	$$⊢2=1+1$$
4	2 3	fveq12i	$$⊢\mathrm{Ack}\left(4\right)\left(2\right)=\mathrm{Ack}\left(3+1\right)\left(1+1\right)$$
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7		ackvalsucsucval	$$⊢\left(3\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\to \mathrm{Ack}\left(3+1\right)\left(1+1\right)=\mathrm{Ack}\left(3\right)\left(\mathrm{Ack}\left(3+1\right)\left(1\right)\right)$$
8	5 6 7	mp2an	$$⊢\mathrm{Ack}\left(3+1\right)\left(1+1\right)=\mathrm{Ack}\left(3\right)\left(\mathrm{Ack}\left(3+1\right)\left(1\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(1\right)=\mathrm{Ack}\left(4\right)\left(1\right)$$
12		ackval41a	$$⊢\mathrm{Ack}\left(4\right)\left(1\right)=2^{16}-3$$
13	11 12	eqtri	$$⊢\mathrm{Ack}\left(3+1\right)\left(1\right)=2^{16}-3$$
14	13	fveq2i	$$⊢\mathrm{Ack}\left(3\right)\left(\mathrm{Ack}\left(3+1\right)\left(1\right)\right)=\mathrm{Ack}\left(3\right)\left(2^{16}-3\right)$$
15		2cn	$$⊢2\in ℂ$$
16		6nn0	$$⊢6\in {\mathbb{N}}_0$$
17	6 16	deccl	$$⊢16\in {\mathbb{N}}_0$$
18		expcl	$$⊢\left(2\in ℂ\wedge 16\in {\mathbb{N}}_0\right)\to 2^{16}\in ℂ$$
19	15 17 18	mp2an	$$⊢2^{16}\in ℂ$$
20		3cn	$$⊢3\in ℂ$$
21		ackval3	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)$$
22		oveq1	$$⊢n=2^{16}-3\to n+3=2^{16}-3+3$$
23		npcan	$$⊢\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\to 2^{16}-3+3=2^{16}$$
24	22 23	sylan9eqr	$$⊢\left(\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\wedge n=2^{16}-3\right)\to n+3=2^{16}$$
25	24	oveq2d	$$⊢\left(\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\wedge n=2^{16}-3\right)\to 2^{n+3}=2^{2^{16}}$$
26	25	oveq1d	$$⊢\left(\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\wedge n=2^{16}-3\right)\to 2^{n+3}-3=2^{2^{16}}-3$$
27		3re	$$⊢3\in ℝ$$
28		4re	$$⊢4\in ℝ$$
29		3lt4	$$⊢3<4$$
30	27 28 29	ltleii	$$⊢3\le 4$$
31		sq2	$$⊢2^2=4$$
32	30 31	breqtrri	$$⊢3\le 2^2$$
33		2re	$$⊢2\in ℝ$$
34		1le2	$$⊢1\le 2$$
35	17	nn0zi	$$⊢16\in \mathbb{Z}$$
36		1nn	$$⊢1\in \mathbb{N}$$
37		2nn0	$$⊢2\in {\mathbb{N}}_0$$
38		9re	$$⊢9\in ℝ$$
39		2lt9	$$⊢2<9$$
40	33 38 39	ltleii	$$⊢2\le 9$$
41	36 16 37 40	declei	$$⊢2\le 16$$
42		2z	$$⊢2\in \mathbb{Z}$$
43	42	eluz1i	$$⊢16\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(16\in \mathbb{Z}\wedge 2\le 16\right)$$
44	35 41 43	mpbir2an	$$⊢16\in {\mathbb{Z}}_{\ge 2}$$
45		leexp2a	$$⊢\left(2\in ℝ\wedge 1\le 2\wedge 16\in {\mathbb{Z}}_{\ge 2}\right)\to 2^2\le 2^{16}$$
46	33 34 44 45	mp3an	$$⊢2^2\le 2^{16}$$
47		4nn0	$$⊢4\in {\mathbb{N}}_0$$
48	31 47	eqeltri	$$⊢2^2\in {\mathbb{N}}_0$$
49	48	nn0rei	$$⊢2^2\in ℝ$$
50	37 17	nn0expcli	$$⊢2^{16}\in {\mathbb{N}}_0$$
51	50	nn0rei	$$⊢2^{16}\in ℝ$$
52	27 49 51	letri	$$⊢\left(3\le 2^2\wedge 2^2\le 2^{16}\right)\to 3\le 2^{16}$$
53	32 46 52	mp2an	$$⊢3\le 2^{16}$$
54		nn0sub	$$⊢\left(3\in {\mathbb{N}}_0\wedge 2^{16}\in {\mathbb{N}}_0\right)\to \left(3\le 2^{16}\leftrightarrow 2^{16}-3\in {\mathbb{N}}_0\right)$$
55	5 50 54	mp2an	$$⊢3\le 2^{16}\leftrightarrow 2^{16}-3\in {\mathbb{N}}_0$$
56	53 55	mpbi	$$⊢2^{16}-3\in {\mathbb{N}}_0$$
57	56	a1i	$$⊢\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\to 2^{16}-3\in {\mathbb{N}}_0$$
58		ovexd	$$⊢\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\to 2^{2^{16}}-3\in \mathrm{V}$$
59	21 26 57 58	fvmptd2	$$⊢\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\to \mathrm{Ack}\left(3\right)\left(2^{16}-3\right)=2^{2^{16}}-3$$
60	19 20 59	mp2an	$$⊢\mathrm{Ack}\left(3\right)\left(2^{16}-3\right)=2^{2^{16}}-3$$
61		2exp16	$$⊢2^{16}=65536$$
62	61	oveq2i	$$⊢2^{2^{16}}=2^{65536}$$
63	62	oveq1i	$$⊢2^{2^{16}}-3=2^{65536}-3$$
64	14 60 63	3eqtri	$$⊢\mathrm{Ack}\left(3\right)\left(\mathrm{Ack}\left(3+1\right)\left(1\right)\right)=2^{65536}-3$$
65	4 8 64	3eqtri	$$⊢\mathrm{Ack}\left(4\right)\left(2\right)=2^{65536}-3$$