Metamath Proof Explorer

Theorem ackval3012

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

Ref Expression
Assertion ackval3012 ⟨ ( ( Ack ‘ 3 ) ‘ 0 ) , ( ( Ack ‘ 3 ) ‘ 1 ) , ( ( Ack ‘ 3 ) ‘ 2 ) ⟩ = ⟨ 5 , 1 3 , 2 9 ⟩

Proof

Step Hyp Ref Expression
1 ackval3 ⊢ ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) )
2 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 + 3 ) = ( 0 + 3 ) )
3 3cn ⊢ 3 ∈ ℂ
4 3 addlidi ⊢ ( 0 + 3 ) = 3
5 2 4 eqtrdi ⊢ ( 𝑛 = 0 → ( 𝑛 + 3 ) = 3 )
6 5 oveq2d ⊢ ( 𝑛 = 0 → ( 2 ↑ ( 𝑛 + 3 ) ) = ( 2 ↑ 3 ) )
7 6 oveq1d ⊢ ( 𝑛 = 0 → ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) = ( ( 2 ↑ 3 ) − 3 ) )
8 cu2 ⊢ ( 2 ↑ 3 ) = 8
9 8 oveq1i ⊢ ( ( 2 ↑ 3 ) − 3 ) = ( 8 − 3 )
10 5cn ⊢ 5 ∈ ℂ
11 5p3e8 ⊢ ( 5 + 3 ) = 8
12 11 eqcomi ⊢ 8 = ( 5 + 3 )
13 10 3 12 mvrraddi ⊢ ( 8 − 3 ) = 5
14 9 13 eqtri ⊢ ( ( 2 ↑ 3 ) − 3 ) = 5
15 7 14 eqtrdi ⊢ ( 𝑛 = 0 → ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) = 5 )
16 0nn0 ⊢ 0 ∈ ℕ0
17 16 a1i ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → 0 ∈ ℕ0 )
18 5nn0 ⊢ 5 ∈ ℕ0
19 18 a1i ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → 5 ∈ ℕ0 )
20 1 15 17 19 fvmptd3 ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → ( ( Ack ‘ 3 ) ‘ 0 ) = 5 )
21 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 + 3 ) = ( 1 + 3 ) )
22 ax-1cn ⊢ 1 ∈ ℂ
23 3p1e4 ⊢ ( 3 + 1 ) = 4
24 3 22 23 addcomli ⊢ ( 1 + 3 ) = 4
25 21 24 eqtrdi ⊢ ( 𝑛 = 1 → ( 𝑛 + 3 ) = 4 )
26 25 oveq2d ⊢ ( 𝑛 = 1 → ( 2 ↑ ( 𝑛 + 3 ) ) = ( 2 ↑ 4 ) )
27 26 oveq1d ⊢ ( 𝑛 = 1 → ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) = ( ( 2 ↑ 4 ) − 3 ) )
28 2exp4 ⊢ ( 2 ↑ 4 ) = 1 6
29 28 oveq1i ⊢ ( ( 2 ↑ 4 ) − 3 ) = ( 1 6 − 3 )
30 1nn0 ⊢ 1 ∈ ℕ0
31 3nn0 ⊢ 3 ∈ ℕ0
32 30 31 deccl ⊢ 1 3 ∈ ℕ0
33 32 nn0cni ⊢ 1 3 ∈ ℂ
34 eqid ⊢ 1 3 = 1 3
35 3p3e6 ⊢ ( 3 + 3 ) = 6
36 30 31 31 34 35 decaddi ⊢ ( 1 3 + 3 ) = 1 6
37 36 eqcomi ⊢ 1 6 = ( 1 3 + 3 )
38 33 3 37 mvrraddi ⊢ ( 1 6 − 3 ) = 1 3
39 29 38 eqtri ⊢ ( ( 2 ↑ 4 ) − 3 ) = 1 3
40 27 39 eqtrdi ⊢ ( 𝑛 = 1 → ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) = 1 3 )
41 30 a1i ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → 1 ∈ ℕ0 )
42 32 a1i ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → 1 3 ∈ ℕ0 )
43 1 40 41 42 fvmptd3 ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → ( ( Ack ‘ 3 ) ‘ 1 ) = 1 3 )
44 oveq1 ⊢ ( 𝑛 = 2 → ( 𝑛 + 3 ) = ( 2 + 3 ) )
45 2cn ⊢ 2 ∈ ℂ
46 3p2e5 ⊢ ( 3 + 2 ) = 5
47 3 45 46 addcomli ⊢ ( 2 + 3 ) = 5
48 44 47 eqtrdi ⊢ ( 𝑛 = 2 → ( 𝑛 + 3 ) = 5 )
49 48 oveq2d ⊢ ( 𝑛 = 2 → ( 2 ↑ ( 𝑛 + 3 ) ) = ( 2 ↑ 5 ) )
50 49 oveq1d ⊢ ( 𝑛 = 2 → ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) = ( ( 2 ↑ 5 ) − 3 ) )
51 2exp5 ⊢ ( 2 ↑ 5 ) = 3 2
52 51 oveq1i ⊢ ( ( 2 ↑ 5 ) − 3 ) = ( 3 2 − 3 )
53 2nn0 ⊢ 2 ∈ ℕ0
54 9nn0 ⊢ 9 ∈ ℕ0
55 53 54 deccl ⊢ 2 9 ∈ ℕ0
56 55 nn0cni ⊢ 2 9 ∈ ℂ
57 eqid ⊢ 2 9 = 2 9
58 2p1e3 ⊢ ( 2 + 1 ) = 3
59 9p3e12 ⊢ ( 9 + 3 ) = 1 2
60 53 54 31 57 58 53 59 decaddci ⊢ ( 2 9 + 3 ) = 3 2
61 60 eqcomi ⊢ 3 2 = ( 2 9 + 3 )
62 56 3 61 mvrraddi ⊢ ( 3 2 − 3 ) = 2 9
63 52 62 eqtri ⊢ ( ( 2 ↑ 5 ) − 3 ) = 2 9
64 50 63 eqtrdi ⊢ ( 𝑛 = 2 → ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) = 2 9 )
65 53 a1i ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → 2 ∈ ℕ0 )
66 55 a1i ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → 2 9 ∈ ℕ0 )
67 1 64 65 66 fvmptd3 ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → ( ( Ack ‘ 3 ) ‘ 2 ) = 2 9 )
68 20 43 67 oteq123d ⊢ ( ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) ) → ⟨ ( ( Ack ‘ 3 ) ‘ 0 ) , ( ( Ack ‘ 3 ) ‘ 1 ) , ( ( Ack ‘ 3 ) ‘ 2 ) ⟩ = ⟨ 5 , 1 3 , 2 9 ⟩ )
69 1 68 ax-mp ⊢ ⟨ ( ( Ack ‘ 3 ) ‘ 0 ) , ( ( Ack ‘ 3 ) ‘ 1 ) , ( ( Ack ‘ 3 ) ‘ 2 ) ⟩ = ⟨ 5 , 1 3 , 2 9 ⟩