Metamath Proof Explorer

Theorem ackval1012

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

Ref Expression
Assertion ackval1012 ⟨ ( ( Ack ‘ 1 ) ‘ 0 ) , ( ( Ack ‘ 1 ) ‘ 1 ) , ( ( Ack ‘ 1 ) ‘ 2 ) ⟩ = ⟨ 2 , 3 , 4 ⟩

Proof

Step Hyp Ref Expression
1 ackval1 ⊢ ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) )
2 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 + 2 ) = ( 0 + 2 ) )
3 2cn ⊢ 2 ∈ ℂ
4 3 addid2i ⊢ ( 0 + 2 ) = 2
5 2 4 eqtrdi ⊢ ( 𝑛 = 0 → ( 𝑛 + 2 ) = 2 )
6 0nn0 ⊢ 0 ∈ ℕ0
7 6 a1i ⊢ ( ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) ) → 0 ∈ ℕ0 )
8 2nn0 ⊢ 2 ∈ ℕ0
9 8 a1i ⊢ ( ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) ) → 2 ∈ ℕ0 )
10 1 5 7 9 fvmptd3 ⊢ ( ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) ) → ( ( Ack ‘ 1 ) ‘ 0 ) = 2 )
11 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 + 2 ) = ( 1 + 2 ) )
12 1p2e3 ⊢ ( 1 + 2 ) = 3
13 11 12 eqtrdi ⊢ ( 𝑛 = 1 → ( 𝑛 + 2 ) = 3 )
14 1nn0 ⊢ 1 ∈ ℕ0
15 14 a1i ⊢ ( ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) ) → 1 ∈ ℕ0 )
16 3nn0 ⊢ 3 ∈ ℕ0
17 16 a1i ⊢ ( ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) ) → 3 ∈ ℕ0 )
18 1 13 15 17 fvmptd3 ⊢ ( ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) ) → ( ( Ack ‘ 1 ) ‘ 1 ) = 3 )
19 oveq1 ⊢ ( 𝑛 = 2 → ( 𝑛 + 2 ) = ( 2 + 2 ) )
20 2p2e4 ⊢ ( 2 + 2 ) = 4
21 19 20 eqtrdi ⊢ ( 𝑛 = 2 → ( 𝑛 + 2 ) = 4 )
22 4nn0 ⊢ 4 ∈ ℕ0
23 22 a1i ⊢ ( ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) ) → 4 ∈ ℕ0 )
24 1 21 9 23 fvmptd3 ⊢ ( ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) ) → ( ( Ack ‘ 1 ) ‘ 2 ) = 4 )
25 10 18 24 oteq123d ⊢ ( ( Ack ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 2 ) ) → ⟨ ( ( Ack ‘ 1 ) ‘ 0 ) , ( ( Ack ‘ 1 ) ‘ 1 ) , ( ( Ack ‘ 1 ) ‘ 2 ) ⟩ = ⟨ 2 , 3 , 4 ⟩ )
26 1 25 ax-mp ⊢ ⟨ ( ( Ack ‘ 1 ) ‘ 0 ) , ( ( Ack ‘ 1 ) ‘ 1 ) , ( ( Ack ‘ 1 ) ‘ 2 ) ⟩ = ⟨ 2 , 3 , 4 ⟩