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

Metamath Proof Explorer

Theorem ackval2012

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

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

Proof

Step Hyp Ref Expression
1 ackval2 ⊢ ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) )
2 oveq2 ⊢ ( 𝑛 = 0 → ( 2 · 𝑛 ) = ( 2 · 0 ) )
3 2 oveq1d ⊢ ( 𝑛 = 0 → ( ( 2 · 𝑛 ) + 3 ) = ( ( 2 · 0 ) + 3 ) )
4 2t0e0 ⊢ ( 2 · 0 ) = 0
5 4 oveq1i ⊢ ( ( 2 · 0 ) + 3 ) = ( 0 + 3 )
6 3cn ⊢ 3 ∈ ℂ
7 6 addlidi ⊢ ( 0 + 3 ) = 3
8 5 7 eqtri ⊢ ( ( 2 · 0 ) + 3 ) = 3
9 3 8 eqtrdi ⊢ ( 𝑛 = 0 → ( ( 2 · 𝑛 ) + 3 ) = 3 )
10 0nn0 ⊢ 0 ∈ ℕ0
11 10 a1i ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → 0 ∈ ℕ0 )
12 3nn0 ⊢ 3 ∈ ℕ0
13 12 a1i ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → 3 ∈ ℕ0 )
14 1 9 11 13 fvmptd3 ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → ( ( Ack ‘ 2 ) ‘ 0 ) = 3 )
15 oveq2 ⊢ ( 𝑛 = 1 → ( 2 · 𝑛 ) = ( 2 · 1 ) )
16 15 oveq1d ⊢ ( 𝑛 = 1 → ( ( 2 · 𝑛 ) + 3 ) = ( ( 2 · 1 ) + 3 ) )
17 2t1e2 ⊢ ( 2 · 1 ) = 2
18 17 oveq1i ⊢ ( ( 2 · 1 ) + 3 ) = ( 2 + 3 )
19 2cn ⊢ 2 ∈ ℂ
20 3p2e5 ⊢ ( 3 + 2 ) = 5
21 6 19 20 addcomli ⊢ ( 2 + 3 ) = 5
22 18 21 eqtri ⊢ ( ( 2 · 1 ) + 3 ) = 5
23 16 22 eqtrdi ⊢ ( 𝑛 = 1 → ( ( 2 · 𝑛 ) + 3 ) = 5 )
24 1nn0 ⊢ 1 ∈ ℕ0
25 24 a1i ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → 1 ∈ ℕ0 )
26 5nn0 ⊢ 5 ∈ ℕ0
27 26 a1i ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → 5 ∈ ℕ0 )
28 1 23 25 27 fvmptd3 ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → ( ( Ack ‘ 2 ) ‘ 1 ) = 5 )
29 oveq2 ⊢ ( 𝑛 = 2 → ( 2 · 𝑛 ) = ( 2 · 2 ) )
30 29 oveq1d ⊢ ( 𝑛 = 2 → ( ( 2 · 𝑛 ) + 3 ) = ( ( 2 · 2 ) + 3 ) )
31 2t2e4 ⊢ ( 2 · 2 ) = 4
32 31 oveq1i ⊢ ( ( 2 · 2 ) + 3 ) = ( 4 + 3 )
33 4p3e7 ⊢ ( 4 + 3 ) = 7
34 32 33 eqtri ⊢ ( ( 2 · 2 ) + 3 ) = 7
35 30 34 eqtrdi ⊢ ( 𝑛 = 2 → ( ( 2 · 𝑛 ) + 3 ) = 7 )
36 2nn0 ⊢ 2 ∈ ℕ0
37 36 a1i ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → 2 ∈ ℕ0 )
38 7nn0 ⊢ 7 ∈ ℕ0
39 38 a1i ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → 7 ∈ ℕ0 )
40 1 35 37 39 fvmptd3 ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → ( ( Ack ‘ 2 ) ‘ 2 ) = 7 )
41 14 28 40 oteq123d ⊢ ( ( Ack ‘ 2 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 3 ) ) → ⟨ ( ( Ack ‘ 2 ) ‘ 0 ) , ( ( Ack ‘ 2 ) ‘ 1 ) , ( ( Ack ‘ 2 ) ‘ 2 ) ⟩ = ⟨ 3 , 5 , 7 ⟩ )
42 1 41 ax-mp ⊢ ⟨ ( ( Ack ‘ 2 ) ‘ 0 ) , ( ( Ack ‘ 2 ) ‘ 1 ) , ( ( Ack ‘ 2 ) ‘ 2 ) ⟩ = ⟨ 3 , 5 , 7 ⟩