Metamath Proof Explorer

Theorem ackval3

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

Ref Expression
Assertion ackval3 ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) )

Proof

Step Hyp Ref Expression
1 df-3 ⊢ 3 = ( 2 + 1 )
2 1 fveq2i ⊢ ( Ack ‘ 3 ) = ( Ack ‘ ( 2 + 1 ) )
3 2nn0 ⊢ 2 ∈ ℕ0
4 ackvalsuc1mpt ⊢ ( 2 ∈ ℕ0 → ( Ack ‘ ( 2 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 2 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )
5 3 4 ax-mp ⊢ ( Ack ‘ ( 2 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 2 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) )
6 peano2nn0 ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 )
7 3nn0 ⊢ 3 ∈ ℕ0
8 ackval2 ⊢ ( Ack ‘ 2 ) = ( 𝑖 ∈ ℕ0 ↦ ( ( 2 · 𝑖 ) + 3 ) )
9 8 itcovalt2 ⊢ ( ( ( 𝑛 + 1 ) ∈ ℕ0 ∧ 3 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 2 ) ) ‘ ( 𝑛 + 1 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 3 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) ) )
10 6 7 9 sylancl ⊢ ( 𝑛 ∈ ℕ0 → ( ( IterComp ‘ ( Ack ‘ 2 ) ) ‘ ( 𝑛 + 1 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 3 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) ) )
11 10 fveq1d ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( IterComp ‘ ( Ack ‘ 2 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 3 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) ) ‘ 1 ) )
12 eqidd ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 3 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 3 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) ) )
13 oveq1 ⊢ ( 𝑖 = 1 → ( 𝑖 + 3 ) = ( 1 + 3 ) )
14 3cn ⊢ 3 ∈ ℂ
15 ax-1cn ⊢ 1 ∈ ℂ
16 3p1e4 ⊢ ( 3 + 1 ) = 4
17 14 15 16 addcomli ⊢ ( 1 + 3 ) = 4
18 13 17 eqtrdi ⊢ ( 𝑖 = 1 → ( 𝑖 + 3 ) = 4 )
19 18 oveq1d ⊢ ( 𝑖 = 1 → ( ( 𝑖 + 3 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) = ( 4 · ( 2 ↑ ( 𝑛 + 1 ) ) ) )
20 19 oveq1d ⊢ ( 𝑖 = 1 → ( ( ( 𝑖 + 3 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) = ( ( 4 · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) )
21 20 adantl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑖 = 1 ) → ( ( ( 𝑖 + 3 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) = ( ( 4 · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) )
22 1nn0 ⊢ 1 ∈ ℕ0
23 22 a1i ⊢ ( 𝑛 ∈ ℕ0 → 1 ∈ ℕ0 )
24 ovexd ⊢ ( 𝑛 ∈ ℕ0 → ( ( 4 · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) ∈ V )
25 12 21 23 24 fvmptd ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 3 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) ) ‘ 1 ) = ( ( 4 · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) )
26 sq2 ⊢ ( 2 ↑ 2 ) = 4
27 26 eqcomi ⊢ 4 = ( 2 ↑ 2 )
28 27 a1i ⊢ ( 𝑛 ∈ ℕ0 → 4 = ( 2 ↑ 2 ) )
29 28 oveq1d ⊢ ( 𝑛 ∈ ℕ0 → ( 4 · ( 2 ↑ ( 𝑛 + 1 ) ) ) = ( ( 2 ↑ 2 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) )
30 2cnd ⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℂ )
31 3 a1i ⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ0 )
32 30 6 31 expaddd ⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ ( 2 + ( 𝑛 + 1 ) ) ) = ( ( 2 ↑ 2 ) · ( 2 ↑ ( 𝑛 + 1 ) ) ) )
33 nn0cn ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
34 1cnd ⊢ ( 𝑛 ∈ ℕ0 → 1 ∈ ℂ )
35 30 33 34 add12d ⊢ ( 𝑛 ∈ ℕ0 → ( 2 + ( 𝑛 + 1 ) ) = ( 𝑛 + ( 2 + 1 ) ) )
36 2p1e3 ⊢ ( 2 + 1 ) = 3
37 36 oveq2i ⊢ ( 𝑛 + ( 2 + 1 ) ) = ( 𝑛 + 3 )
38 35 37 eqtrdi ⊢ ( 𝑛 ∈ ℕ0 → ( 2 + ( 𝑛 + 1 ) ) = ( 𝑛 + 3 ) )
39 38 oveq2d ⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ ( 2 + ( 𝑛 + 1 ) ) ) = ( 2 ↑ ( 𝑛 + 3 ) ) )
40 29 32 39 3eqtr2d ⊢ ( 𝑛 ∈ ℕ0 → ( 4 · ( 2 ↑ ( 𝑛 + 1 ) ) ) = ( 2 ↑ ( 𝑛 + 3 ) ) )
41 40 oveq1d ⊢ ( 𝑛 ∈ ℕ0 → ( ( 4 · ( 2 ↑ ( 𝑛 + 1 ) ) ) − 3 ) = ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) )
42 11 25 41 3eqtrd ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( IterComp ‘ ( Ack ‘ 2 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) = ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) )
43 42 mpteq2ia ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 2 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) )
44 2 5 43 3eqtri ⊢ ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) )