Proof of Theorem ackval3012
Step | Hyp | Ref
| Expression |
1 | | ackval3 45447 |
. 2
⊢
(Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) |
2 | | oveq1 7150 |
. . . . . . . 8
⊢ (𝑛 = 0 → (𝑛 + 3) = (0 + 3)) |
3 | | 3cn 11740 |
. . . . . . . . 9
⊢ 3 ∈
ℂ |
4 | 3 | addid2i 10851 |
. . . . . . . 8
⊢ (0 + 3) =
3 |
5 | 2, 4 | eqtrdi 2810 |
. . . . . . 7
⊢ (𝑛 = 0 → (𝑛 + 3) = 3) |
6 | 5 | oveq2d 7159 |
. . . . . 6
⊢ (𝑛 = 0 → (2↑(𝑛 + 3)) =
(2↑3)) |
7 | 6 | oveq1d 7158 |
. . . . 5
⊢ (𝑛 = 0 → ((2↑(𝑛 + 3)) − 3) = ((2↑3)
− 3)) |
8 | | cu2 13598 |
. . . . . . 7
⊢
(2↑3) = 8 |
9 | 8 | oveq1i 7153 |
. . . . . 6
⊢
((2↑3) − 3) = (8 − 3) |
10 | | 5cn 11747 |
. . . . . . 7
⊢ 5 ∈
ℂ |
11 | | 5p3e8 11816 |
. . . . . . . 8
⊢ (5 + 3) =
8 |
12 | 11 | eqcomi 2768 |
. . . . . . 7
⊢ 8 = (5 +
3) |
13 | 10, 3, 12 | mvrraddi 10926 |
. . . . . 6
⊢ (8
− 3) = 5 |
14 | 9, 13 | eqtri 2782 |
. . . . 5
⊢
((2↑3) − 3) = 5 |
15 | 7, 14 | eqtrdi 2810 |
. . . 4
⊢ (𝑛 = 0 → ((2↑(𝑛 + 3)) − 3) =
5) |
16 | | 0nn0 11934 |
. . . . 5
⊢ 0 ∈
ℕ0 |
17 | 16 | a1i 11 |
. . . 4
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) → 0 ∈
ℕ0) |
18 | | 5nn0 11939 |
. . . . 5
⊢ 5 ∈
ℕ0 |
19 | 18 | a1i 11 |
. . . 4
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) → 5 ∈
ℕ0) |
20 | 1, 15, 17, 19 | fvmptd3 6775 |
. . 3
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) →
((Ack‘3)‘0) = 5) |
21 | | oveq1 7150 |
. . . . . . . 8
⊢ (𝑛 = 1 → (𝑛 + 3) = (1 + 3)) |
22 | | ax-1cn 10618 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
23 | | 3p1e4 11804 |
. . . . . . . . 9
⊢ (3 + 1) =
4 |
24 | 3, 22, 23 | addcomli 10855 |
. . . . . . . 8
⊢ (1 + 3) =
4 |
25 | 21, 24 | eqtrdi 2810 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝑛 + 3) = 4) |
26 | 25 | oveq2d 7159 |
. . . . . 6
⊢ (𝑛 = 1 → (2↑(𝑛 + 3)) =
(2↑4)) |
27 | 26 | oveq1d 7158 |
. . . . 5
⊢ (𝑛 = 1 → ((2↑(𝑛 + 3)) − 3) = ((2↑4)
− 3)) |
28 | | 2exp4 16461 |
. . . . . . 7
⊢
(2↑4) = ;16 |
29 | 28 | oveq1i 7153 |
. . . . . 6
⊢
((2↑4) − 3) = (;16 − 3) |
30 | | 1nn0 11935 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
31 | | 3nn0 11937 |
. . . . . . . . 9
⊢ 3 ∈
ℕ0 |
32 | 30, 31 | deccl 12137 |
. . . . . . . 8
⊢ ;13 ∈
ℕ0 |
33 | 32 | nn0cni 11931 |
. . . . . . 7
⊢ ;13 ∈ ℂ |
34 | | eqid 2759 |
. . . . . . . . 9
⊢ ;13 = ;13 |
35 | | 3p3e6 11811 |
. . . . . . . . 9
⊢ (3 + 3) =
6 |
36 | 30, 31, 31, 34, 35 | decaddi 12182 |
. . . . . . . 8
⊢ (;13 + 3) = ;16 |
37 | 36 | eqcomi 2768 |
. . . . . . 7
⊢ ;16 = (;13 + 3) |
38 | 33, 3, 37 | mvrraddi 10926 |
. . . . . 6
⊢ (;16 − 3) = ;13 |
39 | 29, 38 | eqtri 2782 |
. . . . 5
⊢
((2↑4) − 3) = ;13 |
40 | 27, 39 | eqtrdi 2810 |
. . . 4
⊢ (𝑛 = 1 → ((2↑(𝑛 + 3)) − 3) = ;13) |
41 | 30 | a1i 11 |
. . . 4
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) → 1 ∈
ℕ0) |
42 | 32 | a1i 11 |
. . . 4
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) → ;13 ∈ ℕ0) |
43 | 1, 40, 41, 42 | fvmptd3 6775 |
. . 3
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) →
((Ack‘3)‘1) = ;13) |
44 | | oveq1 7150 |
. . . . . . . 8
⊢ (𝑛 = 2 → (𝑛 + 3) = (2 + 3)) |
45 | | 2cn 11734 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
46 | | 3p2e5 11810 |
. . . . . . . . 9
⊢ (3 + 2) =
5 |
47 | 3, 45, 46 | addcomli 10855 |
. . . . . . . 8
⊢ (2 + 3) =
5 |
48 | 44, 47 | eqtrdi 2810 |
. . . . . . 7
⊢ (𝑛 = 2 → (𝑛 + 3) = 5) |
49 | 48 | oveq2d 7159 |
. . . . . 6
⊢ (𝑛 = 2 → (2↑(𝑛 + 3)) =
(2↑5)) |
50 | 49 | oveq1d 7158 |
. . . . 5
⊢ (𝑛 = 2 → ((2↑(𝑛 + 3)) − 3) = ((2↑5)
− 3)) |
51 | | 2exp5 16462 |
. . . . . . 7
⊢
(2↑5) = ;32 |
52 | 51 | oveq1i 7153 |
. . . . . 6
⊢
((2↑5) − 3) = (;32 − 3) |
53 | | 2nn0 11936 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
54 | | 9nn0 11943 |
. . . . . . . . 9
⊢ 9 ∈
ℕ0 |
55 | 53, 54 | deccl 12137 |
. . . . . . . 8
⊢ ;29 ∈
ℕ0 |
56 | 55 | nn0cni 11931 |
. . . . . . 7
⊢ ;29 ∈ ℂ |
57 | | eqid 2759 |
. . . . . . . . 9
⊢ ;29 = ;29 |
58 | | 2p1e3 11801 |
. . . . . . . . 9
⊢ (2 + 1) =
3 |
59 | | 9p3e12 12210 |
. . . . . . . . 9
⊢ (9 + 3) =
;12 |
60 | 53, 54, 31, 57, 58, 53, 59 | decaddci 12183 |
. . . . . . . 8
⊢ (;29 + 3) = ;32 |
61 | 60 | eqcomi 2768 |
. . . . . . 7
⊢ ;32 = (;29 + 3) |
62 | 56, 3, 61 | mvrraddi 10926 |
. . . . . 6
⊢ (;32 − 3) = ;29 |
63 | 52, 62 | eqtri 2782 |
. . . . 5
⊢
((2↑5) − 3) = ;29 |
64 | 50, 63 | eqtrdi 2810 |
. . . 4
⊢ (𝑛 = 2 → ((2↑(𝑛 + 3)) − 3) = ;29) |
65 | 53 | a1i 11 |
. . . 4
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) → 2 ∈
ℕ0) |
66 | 55 | a1i 11 |
. . . 4
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) → ;29 ∈ ℕ0) |
67 | 1, 64, 65, 66 | fvmptd3 6775 |
. . 3
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) →
((Ack‘3)‘2) = ;29) |
68 | 20, 43, 67 | oteq123d 4771 |
. 2
⊢
((Ack‘3) = (𝑛
∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) →
〈((Ack‘3)‘0), ((Ack‘3)‘1),
((Ack‘3)‘2)〉 = 〈5, ;13, ;29〉) |
69 | 1, 68 | ax-mp 5 |
1
⊢
〈((Ack‘3)‘0), ((Ack‘3)‘1),
((Ack‘3)‘2)〉 = 〈5, ;13, ;29〉 |