Theorem ackval1

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

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

Proof

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