This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )