Theorem ackval2

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

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

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2	1	fveq2i	$$⊢\mathrm{Ack}\left(2\right)=\mathrm{Ack}\left(1+1\right)$$
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4		ackvalsuc1mpt	$$⊢1\in {\mathbb{N}}_0\to \mathrm{Ack}\left(1+1\right)=\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(1\right)\right)\left(n+1\right)\left(1\right)\right)$$
5	3 4	ax-mp	$$⊢\mathrm{Ack}\left(1+1\right)=\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(1\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		2nn0	$$⊢2\in {\mathbb{N}}_0$$
8		ackval1	$$⊢\mathrm{Ack}\left(1\right)=\left(i\in {\mathbb{N}}_0⟼i+2\right)$$
9	8	itcovalpc	$$⊢\left(n+1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\to \mathrm{IterComp}\left(\mathrm{Ack}\left(1\right)\right)\left(n+1\right)=\left(i\in {\mathbb{N}}_0⟼i+2\left(n+1\right)\right)$$
10	6 7 9	sylancl	$$⊢n\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(\mathrm{Ack}\left(1\right)\right)\left(n+1\right)=\left(i\in {\mathbb{N}}_0⟼i+2\left(n+1\right)\right)$$
11	10	fveq1d	$$⊢n\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(\mathrm{Ack}\left(1\right)\right)\left(n+1\right)\left(1\right)=\left(i\in {\mathbb{N}}_0⟼i+2\left(n+1\right)\right)\left(1\right)$$
12		eqidd	$$⊢n\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼i+2\left(n+1\right)\right)=\left(i\in {\mathbb{N}}_0⟼i+2\left(n+1\right)\right)$$
13		oveq1	$$⊢i=1\to i+2\left(n+1\right)=1+2\left(n+1\right)$$
14	13	adantl	$$⊢\left(n\in {\mathbb{N}}_0\wedge i=1\right)\to i+2\left(n+1\right)=1+2\left(n+1\right)$$
15	3	a1i	$$⊢n\in {\mathbb{N}}_0\to 1\in {\mathbb{N}}_0$$
16		ovexd	$$⊢n\in {\mathbb{N}}_0\to 1+2\left(n+1\right)\in \mathrm{V}$$
17	12 14 15 16	fvmptd	$$⊢n\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼i+2\left(n+1\right)\right)\left(1\right)=1+2\left(n+1\right)$$
18		nn0cn	$$⊢n\in {\mathbb{N}}_0\to n\in ℂ$$
19		1cnd	$$⊢n\in ℂ\to 1\in ℂ$$
20		2cnd	$$⊢n\in ℂ\to 2\in ℂ$$
21		peano2cn	$$⊢n\in ℂ\to n+1\in ℂ$$
22	20 21	mulcld	$$⊢n\in ℂ\to 2\left(n+1\right)\in ℂ$$
23	19 22	addcomd	$$⊢n\in ℂ\to 1+2\left(n+1\right)=2\left(n+1\right)+1$$
24		id	$$⊢n\in ℂ\to n\in ℂ$$
25	20 24 19	adddid	$$⊢n\in ℂ\to 2\left(n+1\right)=2n+2\cdot 1$$
26	25	oveq1d	$$⊢n\in ℂ\to 2\left(n+1\right)+1=2n+2\cdot 1+1$$
27	20 24	mulcld	$$⊢n\in ℂ\to 2n\in ℂ$$
28	20 19	mulcld	$$⊢n\in ℂ\to 2\cdot 1\in ℂ$$
29	27 28 19	addassd	$$⊢n\in ℂ\to 2n+2\cdot 1+1=2n+2\cdot 1+1$$
30		2t1e2	$$⊢2\cdot 1=2$$
31	30	oveq1i	$$⊢2\cdot 1+1=2+1$$
32		2p1e3	$$⊢2+1=3$$
33	31 32	eqtri	$$⊢2\cdot 1+1=3$$
34	33	a1i	$$⊢n\in ℂ\to 2\cdot 1+1=3$$
35	34	oveq2d	$$⊢n\in ℂ\to 2n+2\cdot 1+1=2n+3$$
36	29 35	eqtrd	$$⊢n\in ℂ\to 2n+2\cdot 1+1=2n+3$$
37	23 26 36	3eqtrd	$$⊢n\in ℂ\to 1+2\left(n+1\right)=2n+3$$
38	18 37	syl	$$⊢n\in {\mathbb{N}}_0\to 1+2\left(n+1\right)=2n+3$$
39	11 17 38	3eqtrd	$$⊢n\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(\mathrm{Ack}\left(1\right)\right)\left(n+1\right)\left(1\right)=2n+3$$
40	39	mpteq2ia	$$⊢\left(n\in {\mathbb{N}}_0⟼\mathrm{IterComp}\left(\mathrm{Ack}\left(1\right)\right)\left(n+1\right)\left(1\right)\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)$$
41	2 5 40	3eqtri	$$⊢\mathrm{Ack}\left(2\right)=\left(n\in {\mathbb{N}}_0⟼2n+3\right)$$