Theorem ackval1

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

	Ref	Expression
Assertion	ackval1	⊢ ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) )

Proof

Step	Hyp	Ref	Expression
1		1e0p1	⊢ 1 = ( 0 + 1 )
2	1	fveq2i	⊢ ( Ack ‘ 1 ) = ( Ack ‘ ( 0 + 1 ) )
3		0nn0	⊢ 0 ∈ ℕ0
4		ackvalsuc1mpt	⊢ ( 0 ∈ ℕ0 → ( Ack ‘ ( 0 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 0 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )
5	3 4	ax-mp	⊢ ( Ack ‘ ( 0 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 0 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) )
6		peano2nn0	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 )
7		1nn0	⊢ 1 ∈ ℕ0
8		ackval0	⊢ ( Ack ‘ 0 ) = ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + 1 ) )
9	8	itcovalpc	⊢ ( ( ( 𝑛 + 1 ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 0 ) ) ‘ ( 𝑛 + 1 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + ( 1 · ( 𝑛 + 1 ) ) ) ) )
10	6 7 9	sylancl	⊢ ( 𝑛 ∈ ℕ0 → ( ( IterComp ‘ ( Ack ‘ 0 ) ) ‘ ( 𝑛 + 1 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + ( 1 · ( 𝑛 + 1 ) ) ) ) )
11		nn0cn	⊢ ( ( 𝑛 + 1 ) ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℂ )
12	6 11	syl	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℂ )
13	12	mullidd	⊢ ( 𝑛 ∈ ℕ0 → ( 1 · ( 𝑛 + 1 ) ) = ( 𝑛 + 1 ) )
14	13	oveq2d	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑖 + ( 1 · ( 𝑛 + 1 ) ) ) = ( 𝑖 + ( 𝑛 + 1 ) ) )
15	14	mpteq2dv	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + ( 1 · ( 𝑛 + 1 ) ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + ( 𝑛 + 1 ) ) ) )
16	10 15	eqtrd	⊢ ( 𝑛 ∈ ℕ0 → ( ( IterComp ‘ ( Ack ‘ 0 ) ) ‘ ( 𝑛 + 1 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + ( 𝑛 + 1 ) ) ) )
17	16	fveq1d	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( IterComp ‘ ( Ack ‘ 0 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + ( 𝑛 + 1 ) ) ) ‘ 1 ) )
18		eqidd	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + ( 𝑛 + 1 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + ( 𝑛 + 1 ) ) ) )
19		oveq1	⊢ ( 𝑖 = 1 → ( 𝑖 + ( 𝑛 + 1 ) ) = ( 1 + ( 𝑛 + 1 ) ) )
20	19	adantl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑖 = 1 ) → ( 𝑖 + ( 𝑛 + 1 ) ) = ( 1 + ( 𝑛 + 1 ) ) )
21	7	a1i	⊢ ( 𝑛 ∈ ℕ0 → 1 ∈ ℕ0 )
22		ovexd	⊢ ( 𝑛 ∈ ℕ0 → ( 1 + ( 𝑛 + 1 ) ) ∈ V )
23	18 20 21 22	fvmptd	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 + ( 𝑛 + 1 ) ) ) ‘ 1 ) = ( 1 + ( 𝑛 + 1 ) ) )
24		1cnd	⊢ ( 𝑛 ∈ ℕ0 → 1 ∈ ℂ )
25		nn0cn	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
26		peano2cn	⊢ ( 𝑛 ∈ ℂ → ( 𝑛 + 1 ) ∈ ℂ )
27	25 26	syl	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℂ )
28	24 27	addcomd	⊢ ( 𝑛 ∈ ℕ0 → ( 1 + ( 𝑛 + 1 ) ) = ( ( 𝑛 + 1 ) + 1 ) )
29	25 24 24	addassd	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 + 1 ) + 1 ) = ( 𝑛 + ( 1 + 1 ) ) )
30		1p1e2	⊢ ( 1 + 1 ) = 2
31	30	oveq2i	⊢ ( 𝑛 + ( 1 + 1 ) ) = ( 𝑛 + 2 )
32	31	a1i	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + ( 1 + 1 ) ) = ( 𝑛 + 2 ) )
33	28 29 32	3eqtrd	⊢ ( 𝑛 ∈ ℕ0 → ( 1 + ( 𝑛 + 1 ) ) = ( 𝑛 + 2 ) )
34	17 23 33	3eqtrd	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( IterComp ‘ ( Ack ‘ 0 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) = ( 𝑛 + 2 ) )
35	34	mpteq2ia	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 0 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) )
36	2 5 35	3eqtri	⊢ ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) )