Theorem ackval3

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

	Ref	Expression
Assertion	ackval3	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-3	$$⊢3=2+1$$
2	1	fveq2i	$$⊢\mathrm{Ack}\left(3\right)=\mathrm{Ack}\left(2+1\right)$$
3		2nn0	$$⊢2\in {\mathbb{N}}_0$$
4		ackvalsuc1mpt	$$⊢2\in {\mathbb{N}}_0\to \mathrm{Ack}\left(2+1\right)=\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(2\right)\right)\left(n+1\right)\left(1\right)\right)$$
5	3 4	ax-mp	$$⊢\mathrm{Ack}\left(2+1\right)=\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(2\right)\right)\left(n+1\right)\left(1\right)\right)$$
6		peano2nn0	$$⊢n\in {\mathbb{N}}_0\to n+1\in {\mathbb{N}}_0$$
7		3nn0	$$⊢3\in {\mathbb{N}}_0$$
8		ackval2	$$⊢\mathrm{Ack}\left(2\right)=\left(i\in {\mathbb{N}}_0⟼2i+3\right)$$
9	8	itcovalt2	$$⊢\left(n+1\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\to \mathrm{IterComp}\left(\mathrm{Ack}\left(2\right)\right)\left(n+1\right)=\left(i\in {\mathbb{N}}_0⟼\left(i+3\right)2^{n+1}-3\right)$$
10	6 7 9	sylancl	$$⊢n\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(\mathrm{Ack}\left(2\right)\right)\left(n+1\right)=\left(i\in {\mathbb{N}}_0⟼\left(i+3\right)2^{n+1}-3\right)$$
11	10	fveq1d	$$⊢n\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(\mathrm{Ack}\left(2\right)\right)\left(n+1\right)\left(1\right)=\left(i\in {\mathbb{N}}_0⟼\left(i+3\right)2^{n+1}-3\right)\left(1\right)$$
12		eqidd	$$⊢n\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼\left(i+3\right)2^{n+1}-3\right)=\left(i\in {\mathbb{N}}_0⟼\left(i+3\right)2^{n+1}-3\right)$$
13		oveq1	$$⊢i=1\to i+3=1+3$$
14		3cn	$$⊢3\in ℂ$$
15		ax-1cn	$$⊢1\in ℂ$$
16		3p1e4	$$⊢3+1=4$$
17	14 15 16	addcomli	$$⊢1+3=4$$
18	13 17	eqtrdi	$$⊢i=1\to i+3=4$$
19	18	oveq1d	$$⊢i=1\to \left(i+3\right)2^{n+1}=42^{n+1}$$
20	19	oveq1d	$$⊢i=1\to \left(i+3\right)2^{n+1}-3=42^{n+1}-3$$
21	20	adantl	$$⊢\left(n\in {\mathbb{N}}_0\wedge i=1\right)\to \left(i+3\right)2^{n+1}-3=42^{n+1}-3$$
22		1nn0	$$⊢1\in {\mathbb{N}}_0$$
23	22	a1i	$$⊢n\in {\mathbb{N}}_0\to 1\in {\mathbb{N}}_0$$
24		ovexd	$$⊢n\in {\mathbb{N}}_0\to 42^{n+1}-3\in \mathrm{V}$$
25	12 21 23 24	fvmptd	$$⊢n\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼\left(i+3\right)2^{n+1}-3\right)\left(1\right)=42^{n+1}-3$$
26		sq2	$$⊢2^2=4$$
27	26	eqcomi	$$⊢4=2^2$$
28	27	a1i	$$⊢n\in {\mathbb{N}}_0\to 4=2^2$$
29	28	oveq1d	$$⊢n\in {\mathbb{N}}_0\to 42^{n+1}=2^2{2}^{n+1}$$
30		2cnd	$$⊢n\in {\mathbb{N}}_0\to 2\in ℂ$$
31	3	a1i	$$⊢n\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
32	30 6 31	expaddd	$$⊢n\in {\mathbb{N}}_0\to 2^{2+n+1}=2^2{2}^{n+1}$$
33		nn0cn	$$⊢n\in {\mathbb{N}}_0\to n\in ℂ$$
34		1cnd	$$⊢n\in {\mathbb{N}}_0\to 1\in ℂ$$
35	30 33 34	add12d	$$⊢n\in {\mathbb{N}}_0\to 2+n+1=n+2+1$$
36		2p1e3	$$⊢2+1=3$$
37	36	oveq2i	$$⊢n+2+1=n+3$$
38	35 37	eqtrdi	$$⊢n\in {\mathbb{N}}_0\to 2+n+1=n+3$$
39	38	oveq2d	$$⊢n\in {\mathbb{N}}_0\to 2^{2+n+1}=2^{n+3}$$
40	29 32 39	3eqtr2d	$$⊢n\in {\mathbb{N}}_0\to 42^{n+1}=2^{n+3}$$
41	40	oveq1d	$$⊢n\in {\mathbb{N}}_0\to 42^{n+1}-3=2^{n+3}-3$$
42	11 25 41	3eqtrd	$$⊢n\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(\mathrm{Ack}\left(2\right)\right)\left(n+1\right)\left(1\right)=2^{n+3}-3$$
43	42	mpteq2ia	$$⊢\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(2\right)\right)\left(n+1\right)\left(1\right)\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)$$
44	2 5 43	3eqtri	$$⊢\mathrm{Ack}\left(3\right)=\left(n\in {\mathbb{N}}_0⟼2^{n+3}-3\right)$$