Metamath Proof Explorer

Theorem ackval2

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

Ref Expression
Assertion ackval2 ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) )

Proof

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