Proof of Theorem ackval42
Step | Hyp | Ref
| Expression |
1 | | df-4 11724 |
. . . 4
⊢ 4 = (3 +
1) |
2 | 1 | fveq2i 6654 |
. . 3
⊢
(Ack‘4) = (Ack‘(3 + 1)) |
3 | | df-2 11722 |
. . 3
⊢ 2 = (1 +
1) |
4 | 2, 3 | fveq12i 6657 |
. 2
⊢
((Ack‘4)‘2) = ((Ack‘(3 + 1))‘(1 +
1)) |
5 | | 3nn0 11937 |
. . 3
⊢ 3 ∈
ℕ0 |
6 | | 1nn0 11935 |
. . 3
⊢ 1 ∈
ℕ0 |
7 | | ackvalsucsucval 45452 |
. . 3
⊢ ((3
∈ ℕ0 ∧ 1 ∈ ℕ0) →
((Ack‘(3 + 1))‘(1 + 1)) = ((Ack‘3)‘((Ack‘(3 +
1))‘1))) |
8 | 5, 6, 7 | mp2an 692 |
. 2
⊢
((Ack‘(3 + 1))‘(1 + 1)) =
((Ack‘3)‘((Ack‘(3 + 1))‘1)) |
9 | | 3p1e4 11804 |
. . . . . . 7
⊢ (3 + 1) =
4 |
10 | 9 | fveq2i 6654 |
. . . . . 6
⊢
(Ack‘(3 + 1)) = (Ack‘4) |
11 | 10 | fveq1i 6652 |
. . . . 5
⊢
((Ack‘(3 + 1))‘1) = ((Ack‘4)‘1) |
12 | | ackval41a 45458 |
. . . . 5
⊢
((Ack‘4)‘1) = ((2↑;16) − 3) |
13 | 11, 12 | eqtri 2782 |
. . . 4
⊢
((Ack‘(3 + 1))‘1) = ((2↑;16) − 3) |
14 | 13 | fveq2i 6654 |
. . 3
⊢
((Ack‘3)‘((Ack‘(3 + 1))‘1)) =
((Ack‘3)‘((2↑;16)
− 3)) |
15 | | 2cn 11734 |
. . . . 5
⊢ 2 ∈
ℂ |
16 | | 6nn0 11940 |
. . . . . 6
⊢ 6 ∈
ℕ0 |
17 | 6, 16 | deccl 12137 |
. . . . 5
⊢ ;16 ∈
ℕ0 |
18 | | expcl 13482 |
. . . . 5
⊢ ((2
∈ ℂ ∧ ;16 ∈
ℕ0) → (2↑;16) ∈ ℂ) |
19 | 15, 17, 18 | mp2an 692 |
. . . 4
⊢
(2↑;16) ∈
ℂ |
20 | | 3cn 11740 |
. . . 4
⊢ 3 ∈
ℂ |
21 | | ackval3 45447 |
. . . . 5
⊢
(Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) |
22 | | oveq1 7150 |
. . . . . . . 8
⊢ (𝑛 = ((2↑;16) − 3) → (𝑛 + 3) = (((2↑;16) − 3) + 3)) |
23 | | npcan 10918 |
. . . . . . . 8
⊢
(((2↑;16) ∈
ℂ ∧ 3 ∈ ℂ) → (((2↑;16) − 3) + 3) = (2↑;16)) |
24 | 22, 23 | sylan9eqr 2816 |
. . . . . . 7
⊢
((((2↑;16) ∈
ℂ ∧ 3 ∈ ℂ) ∧ 𝑛 = ((2↑;16) − 3)) → (𝑛 + 3) = (2↑;16)) |
25 | 24 | oveq2d 7159 |
. . . . . 6
⊢
((((2↑;16) ∈
ℂ ∧ 3 ∈ ℂ) ∧ 𝑛 = ((2↑;16) − 3)) → (2↑(𝑛 + 3)) = (2↑(2↑;16))) |
26 | 25 | oveq1d 7158 |
. . . . 5
⊢
((((2↑;16) ∈
ℂ ∧ 3 ∈ ℂ) ∧ 𝑛 = ((2↑;16) − 3)) → ((2↑(𝑛 + 3)) − 3) = ((2↑(2↑;16)) − 3)) |
27 | | 3re 11739 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
28 | | 4re 11743 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
29 | | 3lt4 11833 |
. . . . . . . . . 10
⊢ 3 <
4 |
30 | 27, 28, 29 | ltleii 10786 |
. . . . . . . . 9
⊢ 3 ≤
4 |
31 | | sq2 13595 |
. . . . . . . . 9
⊢
(2↑2) = 4 |
32 | 30, 31 | breqtrri 5052 |
. . . . . . . 8
⊢ 3 ≤
(2↑2) |
33 | | 2re 11733 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
34 | | 1le2 11868 |
. . . . . . . . 9
⊢ 1 ≤
2 |
35 | 17 | nn0zi 12031 |
. . . . . . . . . 10
⊢ ;16 ∈ ℤ |
36 | | 1nn 11670 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
37 | | 2nn0 11936 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
38 | | 9re 11758 |
. . . . . . . . . . . 12
⊢ 9 ∈
ℝ |
39 | | 2lt9 11864 |
. . . . . . . . . . . 12
⊢ 2 <
9 |
40 | 33, 38, 39 | ltleii 10786 |
. . . . . . . . . . 11
⊢ 2 ≤
9 |
41 | 36, 16, 37, 40 | declei 12158 |
. . . . . . . . . 10
⊢ 2 ≤
;16 |
42 | | 2z 12038 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
43 | 42 | eluz1i 12275 |
. . . . . . . . . 10
⊢ (;16 ∈
(ℤ≥‘2) ↔ (;16 ∈ ℤ ∧ 2 ≤ ;16)) |
44 | 35, 41, 43 | mpbir2an 711 |
. . . . . . . . 9
⊢ ;16 ∈
(ℤ≥‘2) |
45 | | leexp2a 13571 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ 1 ≤ 2 ∧ ;16 ∈ (ℤ≥‘2)) →
(2↑2) ≤ (2↑;16)) |
46 | 33, 34, 44, 45 | mp3an 1459 |
. . . . . . . 8
⊢
(2↑2) ≤ (2↑;16) |
47 | | 4nn0 11938 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
48 | 31, 47 | eqeltri 2847 |
. . . . . . . . . 10
⊢
(2↑2) ∈ ℕ0 |
49 | 48 | nn0rei 11930 |
. . . . . . . . 9
⊢
(2↑2) ∈ ℝ |
50 | 37, 17 | nn0expcli 13490 |
. . . . . . . . . 10
⊢
(2↑;16) ∈
ℕ0 |
51 | 50 | nn0rei 11930 |
. . . . . . . . 9
⊢
(2↑;16) ∈
ℝ |
52 | 27, 49, 51 | letri 10792 |
. . . . . . . 8
⊢ ((3 ≤
(2↑2) ∧ (2↑2) ≤ (2↑;16)) → 3 ≤ (2↑;16)) |
53 | 32, 46, 52 | mp2an 692 |
. . . . . . 7
⊢ 3 ≤
(2↑;16) |
54 | | nn0sub 11969 |
. . . . . . . 8
⊢ ((3
∈ ℕ0 ∧ (2↑;16) ∈ ℕ0) → (3 ≤
(2↑;16) ↔ ((2↑;16) − 3) ∈
ℕ0)) |
55 | 5, 50, 54 | mp2an 692 |
. . . . . . 7
⊢ (3 ≤
(2↑;16) ↔ ((2↑;16) − 3) ∈
ℕ0) |
56 | 53, 55 | mpbi 233 |
. . . . . 6
⊢
((2↑;16) − 3)
∈ ℕ0 |
57 | 56 | a1i 11 |
. . . . 5
⊢
(((2↑;16) ∈
ℂ ∧ 3 ∈ ℂ) → ((2↑;16) − 3) ∈
ℕ0) |
58 | | ovexd 7178 |
. . . . 5
⊢
(((2↑;16) ∈
ℂ ∧ 3 ∈ ℂ) → ((2↑(2↑;16)) − 3) ∈ V) |
59 | 21, 26, 57, 58 | fvmptd2 6760 |
. . . 4
⊢
(((2↑;16) ∈
ℂ ∧ 3 ∈ ℂ) → ((Ack‘3)‘((2↑;16) − 3)) =
((2↑(2↑;16)) −
3)) |
60 | 19, 20, 59 | mp2an 692 |
. . 3
⊢
((Ack‘3)‘((2↑;16) − 3)) = ((2↑(2↑;16)) − 3) |
61 | | 2exp16 16467 |
. . . . 5
⊢
(2↑;16) = ;;;;65536 |
62 | 61 | oveq2i 7154 |
. . . 4
⊢
(2↑(2↑;16)) =
(2↑;;;;65536) |
63 | 62 | oveq1i 7153 |
. . 3
⊢
((2↑(2↑;16))
− 3) = ((2↑;;;;65536)
− 3) |
64 | 14, 60, 63 | 3eqtri 2786 |
. 2
⊢
((Ack‘3)‘((Ack‘(3 + 1))‘1)) = ((2↑;;;;65536) − 3) |
65 | 4, 8, 64 | 3eqtri 2786 |
1
⊢
((Ack‘4)‘2) = ((2↑;;;;65536) − 3) |