Metamath Proof Explorer

Theorem ackval42

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

Ref Expression
Assertion ackval42 ( ( Ack ‘ 4 ) ‘ 2 ) = ( ( 2 ↑ 6 5 5 3 6 ) − 3 )

Proof

Step Hyp Ref Expression
1 df-4 ⊢ 4 = ( 3 + 1 )
2 1 fveq2i ⊢ ( Ack ‘ 4 ) = ( Ack ‘ ( 3 + 1 ) )
3 df-2 ⊢ 2 = ( 1 + 1 )
4 2 3 fveq12i ⊢ ( ( Ack ‘ 4 ) ‘ 2 ) = ( ( Ack ‘ ( 3 + 1 ) ) ‘ ( 1 + 1 ) )
5 3nn0 ⊢ 3 ∈ ℕ0
6 1nn0 ⊢ 1 ∈ ℕ0
7 ackvalsucsucval ⊢ ( ( 3 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( Ack ‘ ( 3 + 1 ) ) ‘ ( 1 + 1 ) ) = ( ( Ack ‘ 3 ) ‘ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 1 ) ) )
8 5 6 7 mp2an ⊢ ( ( Ack ‘ ( 3 + 1 ) ) ‘ ( 1 + 1 ) ) = ( ( Ack ‘ 3 ) ‘ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 1 ) )
9 3p1e4 ⊢ ( 3 + 1 ) = 4
10 9 fveq2i ⊢ ( Ack ‘ ( 3 + 1 ) ) = ( Ack ‘ 4 )
11 10 fveq1i ⊢ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 1 ) = ( ( Ack ‘ 4 ) ‘ 1 )
12 ackval41a ⊢ ( ( Ack ‘ 4 ) ‘ 1 ) = ( ( 2 ↑ 1 6 ) − 3 )
13 11 12 eqtri ⊢ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 1 ) = ( ( 2 ↑ 1 6 ) − 3 )
14 13 fveq2i ⊢ ( ( Ack ‘ 3 ) ‘ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 1 ) ) = ( ( Ack ‘ 3 ) ‘ ( ( 2 ↑ 1 6 ) − 3 ) )
15 2cn ⊢ 2 ∈ ℂ
16 6nn0 ⊢ 6 ∈ ℕ0
17 6 16 deccl ⊢ 1 6 ∈ ℕ0
18 expcl ⊢ ( ( 2 ∈ ℂ ∧ 1 6 ∈ ℕ0 ) → ( 2 ↑ 1 6 ) ∈ ℂ )
19 15 17 18 mp2an ⊢ ( 2 ↑ 1 6 ) ∈ ℂ
20 3cn ⊢ 3 ∈ ℂ
21 ackval3 ⊢ ( Ack ‘ 3 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) )
22 oveq1 ⊢ ( 𝑛 = ( ( 2 ↑ 1 6 ) − 3 ) → ( 𝑛 + 3 ) = ( ( ( 2 ↑ 1 6 ) − 3 ) + 3 ) )
23 npcan ⊢ ( ( ( 2 ↑ 1 6 ) ∈ ℂ ∧ 3 ∈ ℂ ) → ( ( ( 2 ↑ 1 6 ) − 3 ) + 3 ) = ( 2 ↑ 1 6 ) )
24 22 23 sylan9eqr ⊢ ( ( ( ( 2 ↑ 1 6 ) ∈ ℂ ∧ 3 ∈ ℂ ) ∧ 𝑛 = ( ( 2 ↑ 1 6 ) − 3 ) ) → ( 𝑛 + 3 ) = ( 2 ↑ 1 6 ) )
25 24 oveq2d ⊢ ( ( ( ( 2 ↑ 1 6 ) ∈ ℂ ∧ 3 ∈ ℂ ) ∧ 𝑛 = ( ( 2 ↑ 1 6 ) − 3 ) ) → ( 2 ↑ ( 𝑛 + 3 ) ) = ( 2 ↑ ( 2 ↑ 1 6 ) ) )
26 25 oveq1d ⊢ ( ( ( ( 2 ↑ 1 6 ) ∈ ℂ ∧ 3 ∈ ℂ ) ∧ 𝑛 = ( ( 2 ↑ 1 6 ) − 3 ) ) → ( ( 2 ↑ ( 𝑛 + 3 ) ) − 3 ) = ( ( 2 ↑ ( 2 ↑ 1 6 ) ) − 3 ) )
27 3re ⊢ 3 ∈ ℝ
28 4re ⊢ 4 ∈ ℝ
29 3lt4 ⊢ 3 < 4
30 27 28 29 ltleii ⊢ 3 ≤ 4
31 sq2 ⊢ ( 2 ↑ 2 ) = 4
32 30 31 breqtrri ⊢ 3 ≤ ( 2 ↑ 2 )
33 2re ⊢ 2 ∈ ℝ
34 1le2 ⊢ 1 ≤ 2
35 17 nn0zi ⊢ 1 6 ∈ ℤ
36 1nn ⊢ 1 ∈ ℕ
37 2nn0 ⊢ 2 ∈ ℕ0
38 9re ⊢ 9 ∈ ℝ
39 2lt9 ⊢ 2 < 9
40 33 38 39 ltleii ⊢ 2 ≤ 9
41 36 16 37 40 declei ⊢ 2 ≤ 1 6
42 2z ⊢ 2 ∈ ℤ
43 42 eluz1i ⊢ ( 1 6 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 1 6 ∈ ℤ ∧ 2 ≤ 1 6 ) )
44 35 41 43 mpbir2an ⊢ 1 6 ∈ ( ℤ≥ ‘ 2 )
45 leexp2a ⊢ ( ( 2 ∈ ℝ ∧ 1 ≤ 2 ∧ 1 6 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑ 2 ) ≤ ( 2 ↑ 1 6 ) )
46 33 34 44 45 mp3an ⊢ ( 2 ↑ 2 ) ≤ ( 2 ↑ 1 6 )
47 4nn0 ⊢ 4 ∈ ℕ0
48 31 47 eqeltri ⊢ ( 2 ↑ 2 ) ∈ ℕ0
49 48 nn0rei ⊢ ( 2 ↑ 2 ) ∈ ℝ
50 37 17 nn0expcli ⊢ ( 2 ↑ 1 6 ) ∈ ℕ0
51 50 nn0rei ⊢ ( 2 ↑ 1 6 ) ∈ ℝ
52 27 49 51 letri ⊢ ( ( 3 ≤ ( 2 ↑ 2 ) ∧ ( 2 ↑ 2 ) ≤ ( 2 ↑ 1 6 ) ) → 3 ≤ ( 2 ↑ 1 6 ) )
53 32 46 52 mp2an ⊢ 3 ≤ ( 2 ↑ 1 6 )
54 nn0sub ⊢ ( ( 3 ∈ ℕ0 ∧ ( 2 ↑ 1 6 ) ∈ ℕ0 ) → ( 3 ≤ ( 2 ↑ 1 6 ) ↔ ( ( 2 ↑ 1 6 ) − 3 ) ∈ ℕ0 ) )
55 5 50 54 mp2an ⊢ ( 3 ≤ ( 2 ↑ 1 6 ) ↔ ( ( 2 ↑ 1 6 ) − 3 ) ∈ ℕ0 )
56 53 55 mpbi ⊢ ( ( 2 ↑ 1 6 ) − 3 ) ∈ ℕ0
57 56 a1i ⊢ ( ( ( 2 ↑ 1 6 ) ∈ ℂ ∧ 3 ∈ ℂ ) → ( ( 2 ↑ 1 6 ) − 3 ) ∈ ℕ0 )
58 ovexd ⊢ ( ( ( 2 ↑ 1 6 ) ∈ ℂ ∧ 3 ∈ ℂ ) → ( ( 2 ↑ ( 2 ↑ 1 6 ) ) − 3 ) ∈ V )
59 21 26 57 58 fvmptd2 ⊢ ( ( ( 2 ↑ 1 6 ) ∈ ℂ ∧ 3 ∈ ℂ ) → ( ( Ack ‘ 3 ) ‘ ( ( 2 ↑ 1 6 ) − 3 ) ) = ( ( 2 ↑ ( 2 ↑ 1 6 ) ) − 3 ) )
60 19 20 59 mp2an ⊢ ( ( Ack ‘ 3 ) ‘ ( ( 2 ↑ 1 6 ) − 3 ) ) = ( ( 2 ↑ ( 2 ↑ 1 6 ) ) − 3 )
61 2exp16 ⊢ ( 2 ↑ 1 6 ) = 6 5 5 3 6
62 61 oveq2i ⊢ ( 2 ↑ ( 2 ↑ 1 6 ) ) = ( 2 ↑ 6 5 5 3 6 )
63 62 oveq1i ⊢ ( ( 2 ↑ ( 2 ↑ 1 6 ) ) − 3 ) = ( ( 2 ↑ 6 5 5 3 6 ) − 3 )
64 14 60 63 3eqtri ⊢ ( ( Ack ‘ 3 ) ‘ ( ( Ack ‘ ( 3 + 1 ) ) ‘ 1 ) ) = ( ( 2 ↑ 6 5 5 3 6 ) − 3 )
65 4 8 64 3eqtri ⊢ ( ( Ack ‘ 4 ) ‘ 2 ) = ( ( 2 ↑ 6 5 5 3 6 ) − 3 )