Metamath Proof Explorer

Theorem ackval41a

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

Ref Expression
Assertion ackval41a ( ( Ack ‘ 4 ) ‘ 1 ) = ( ( 2 ↑ 1 6 ) − 3 )

Proof

Step Hyp Ref Expression
1 df-4 ⊢ 4 = ( 3 + 1 )
2 1 fveq2i ⊢ ( Ack ‘ 4 ) = ( Ack ‘ ( 3 + 1 ) )
3 1e0p1 ⊢ 1 = ( 0 + 1 )
4 2 3 fveq12i ⊢ ( ( Ack ‘ 4 ) ‘ 1 ) = ( ( Ack ‘ ( 3 + 1 ) ) ‘ ( 0 + 1 ) )
5 3nn0 ⊢ 3 ∈ ℕ0
6 0nn0 ⊢ 0 ∈ ℕ0
7 ackvalsucsucval ⊢ ( ( 3 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ( Ack ‘ ( 3 + 1 ) ) ‘ ( 0 + 1 ) ) = ( ( Ack ‘ 3 ) ‘ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 0 ) ) )
8 5 6 7 mp2an ⊢ ( ( Ack ‘ ( 3 + 1 ) ) ‘ ( 0 + 1 ) ) = ( ( Ack ‘ 3 ) ‘ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 0 ) )
9 3p1e4 ⊢ ( 3 + 1 ) = 4
10 9 fveq2i ⊢ ( Ack ‘ ( 3 + 1 ) ) = ( Ack ‘ 4 )
11 10 fveq1i ⊢ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 0 ) = ( ( Ack ‘ 4 ) ‘ 0 )
12 ackval40 ⊢ ( ( Ack ‘ 4 ) ‘ 0 ) = 1 3
13 11 12 eqtri ⊢ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 0 ) = 1 3
14 13 fveq2i ⊢ ( ( Ack ‘ 3 ) ‘ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 0 ) ) = ( ( Ack ‘ 3 ) ‘ 1 3 )
15 1nn0 ⊢ 1 ∈ ℕ0
16 15 5 deccl ⊢ 1 3 ∈ ℕ0
17 oveq1 ⊢ ( 𝑛 = 1 3 → ( 𝑛 + 3 ) = ( 1 3 + 3 ) )
18 17 oveq2d ⊢ ( 𝑛 = 1 3 → ( 2 ↑ ( 𝑛 + 3 ) ) = ( 2 ↑ ( 1 3 + 3 ) ) )
19 18 oveq1d ⊢ ( 𝑛 = 1 3 → ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) = ( ( 2 ↑ ( 1 3 + 3 ) ) − 3 ) )
20 eqid ⊢ 1 3 = 1 3
21 3p3e6 ⊢ ( 3 + 3 ) = 6
22 15 5 5 20 21 decaddi ⊢ ( 1 3 + 3 ) = 1 6
23 22 oveq2i ⊢ ( 2 ↑ ( 1 3 + 3 ) ) = ( 2 ↑ 1 6 )
24 23 oveq1i ⊢ ( ( 2 ↑ ( 1 3 + 3 ) ) − 3 ) = ( ( 2 ↑ 1 6 ) − 3 )
25 19 24 eqtrdi ⊢ ( 𝑛 = 1 3 → ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) = ( ( 2 ↑ 1 6 ) − 3 ) )
26 ackval3 ⊢ ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) )
27 ovex ⊢ ( ( 2 ↑ 1 6 ) − 3 ) ∈ V
28 25 26 27 fvmpt ⊢ ( 1 3 ∈ ℕ0 → ( ( Ack ‘ 3 ) ‘ 1 3 ) = ( ( 2 ↑ 1 6 ) − 3 ) )
29 16 28 ax-mp ⊢ ( ( Ack ‘ 3 ) ‘ 1 3 ) = ( ( 2 ↑ 1 6 ) − 3 )
30 14 29 eqtri ⊢ ( ( Ack ‘ 3 ) ‘ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 0 ) ) = ( ( 2 ↑ 1 6 ) − 3 )
31 8 30 eqtri ⊢ ( ( Ack ‘ ( 3 + 1 ) ) ‘ ( 0 + 1 ) ) = ( ( 2 ↑ 1 6 ) − 3 )
32 4 31 eqtri ⊢ ( ( Ack ‘ 4 ) ‘ 1 ) = ( ( 2 ↑ 1 6 ) − 3 )