Step | Hyp | Ref
| Expression |
1 | | fveq2 6651 |
. . 3
⊢ (𝑥 = 1 → (seq1( · ,
(𝑘 ∈ ℕ ↦
(((2 · 𝑘)↑4) /
(((2 · 𝑘) ·
((2 · 𝑘) −
1))↑2))))‘𝑥) =
(seq1( · , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2))))‘1)) |
2 | | oveq2 7151 |
. . . . . 6
⊢ (𝑥 = 1 → (4 · 𝑥) = (4 ·
1)) |
3 | 2 | oveq2d 7159 |
. . . . 5
⊢ (𝑥 = 1 → (2↑(4 ·
𝑥)) = (2↑(4 ·
1))) |
4 | | fveq2 6651 |
. . . . . 6
⊢ (𝑥 = 1 → (!‘𝑥) =
(!‘1)) |
5 | 4 | oveq1d 7158 |
. . . . 5
⊢ (𝑥 = 1 → ((!‘𝑥)↑4) =
((!‘1)↑4)) |
6 | 3, 5 | oveq12d 7161 |
. . . 4
⊢ (𝑥 = 1 → ((2↑(4 ·
𝑥)) ·
((!‘𝑥)↑4)) =
((2↑(4 · 1)) · ((!‘1)↑4))) |
7 | | oveq2 7151 |
. . . . . 6
⊢ (𝑥 = 1 → (2 · 𝑥) = (2 ·
1)) |
8 | 7 | fveq2d 6655 |
. . . . 5
⊢ (𝑥 = 1 → (!‘(2 ·
𝑥)) = (!‘(2 ·
1))) |
9 | 8 | oveq1d 7158 |
. . . 4
⊢ (𝑥 = 1 → ((!‘(2
· 𝑥))↑2) =
((!‘(2 · 1))↑2)) |
10 | 6, 9 | oveq12d 7161 |
. . 3
⊢ (𝑥 = 1 → (((2↑(4
· 𝑥)) ·
((!‘𝑥)↑4)) /
((!‘(2 · 𝑥))↑2)) = (((2↑(4 · 1))
· ((!‘1)↑4)) / ((!‘(2 ·
1))↑2))) |
11 | 1, 10 | eqeq12d 2775 |
. 2
⊢ (𝑥 = 1 → ((seq1( · ,
(𝑘 ∈ ℕ ↦
(((2 · 𝑘)↑4) /
(((2 · 𝑘) ·
((2 · 𝑘) −
1))↑2))))‘𝑥) =
(((2↑(4 · 𝑥))
· ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) ↔ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) =
(((2↑(4 · 1)) · ((!‘1)↑4)) / ((!‘(2
· 1))↑2)))) |
12 | | fveq2 6651 |
. . 3
⊢ (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2))))‘𝑥) =
(seq1( · , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) |
13 | | oveq2 7151 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (4 · 𝑥) = (4 · 𝑦)) |
14 | 13 | oveq2d 7159 |
. . . . 5
⊢ (𝑥 = 𝑦 → (2↑(4 · 𝑥)) = (2↑(4 · 𝑦))) |
15 | | fveq2 6651 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (!‘𝑥) = (!‘𝑦)) |
16 | 15 | oveq1d 7158 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((!‘𝑥)↑4) = ((!‘𝑦)↑4)) |
17 | 14, 16 | oveq12d 7161 |
. . . 4
⊢ (𝑥 = 𝑦 → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4
· 𝑦)) ·
((!‘𝑦)↑4))) |
18 | | oveq2 7151 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
19 | 18 | fveq2d 6655 |
. . . . 5
⊢ (𝑥 = 𝑦 → (!‘(2 · 𝑥)) = (!‘(2 · 𝑦))) |
20 | 19 | oveq1d 7158 |
. . . 4
⊢ (𝑥 = 𝑦 → ((!‘(2 · 𝑥))↑2) = ((!‘(2
· 𝑦))↑2)) |
21 | 17, 20 | oveq12d 7161 |
. . 3
⊢ (𝑥 = 𝑦 → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2
· 𝑥))↑2)) =
(((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2))) |
22 | 12, 21 | eqeq12d 2775 |
. 2
⊢ (𝑥 = 𝑦 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2))))‘𝑥) =
(((2↑(4 · 𝑥))
· ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) ↔ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2
· 𝑦))↑2)))) |
23 | | fveq2 6651 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2))))‘𝑥) =
(seq1( · , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))) |
24 | | oveq2 7151 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (4 · 𝑥) = (4 · (𝑦 + 1))) |
25 | 24 | oveq2d 7159 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (2↑(4 · 𝑥)) = (2↑(4 · (𝑦 + 1)))) |
26 | | fveq2 6651 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (!‘𝑥) = (!‘(𝑦 + 1))) |
27 | 26 | oveq1d 7158 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((!‘𝑥)↑4) = ((!‘(𝑦 + 1))↑4)) |
28 | 25, 27 | oveq12d 7161 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4
· (𝑦 + 1))) ·
((!‘(𝑦 +
1))↑4))) |
29 | | oveq2 7151 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1))) |
30 | 29 | fveq2d 6655 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (!‘(2 · 𝑥)) = (!‘(2 · (𝑦 + 1)))) |
31 | 30 | oveq1d 7158 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((!‘(2 · 𝑥))↑2) = ((!‘(2
· (𝑦 +
1)))↑2)) |
32 | 28, 31 | oveq12d 7161 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2
· 𝑥))↑2)) =
(((2↑(4 · (𝑦 +
1))) · ((!‘(𝑦
+ 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2))) |
33 | 23, 32 | eqeq12d 2775 |
. 2
⊢ (𝑥 = (𝑦 + 1) → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2))))‘𝑥) =
(((2↑(4 · 𝑥))
· ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) ↔ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = (((2↑(4 ·
(𝑦 + 1))) ·
((!‘(𝑦 + 1))↑4))
/ ((!‘(2 · (𝑦
+ 1)))↑2)))) |
34 | | fveq2 6651 |
. . 3
⊢ (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2))))‘𝑥) =
(seq1( · , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)) |
35 | | oveq2 7151 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (4 · 𝑥) = (4 · 𝑁)) |
36 | 35 | oveq2d 7159 |
. . . . 5
⊢ (𝑥 = 𝑁 → (2↑(4 · 𝑥)) = (2↑(4 · 𝑁))) |
37 | | fveq2 6651 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁)) |
38 | 37 | oveq1d 7158 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((!‘𝑥)↑4) = ((!‘𝑁)↑4)) |
39 | 36, 38 | oveq12d 7161 |
. . . 4
⊢ (𝑥 = 𝑁 → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4
· 𝑁)) ·
((!‘𝑁)↑4))) |
40 | | oveq2 7151 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁)) |
41 | 40 | fveq2d 6655 |
. . . . 5
⊢ (𝑥 = 𝑁 → (!‘(2 · 𝑥)) = (!‘(2 · 𝑁))) |
42 | 41 | oveq1d 7158 |
. . . 4
⊢ (𝑥 = 𝑁 → ((!‘(2 · 𝑥))↑2) = ((!‘(2
· 𝑁))↑2)) |
43 | 39, 42 | oveq12d 7161 |
. . 3
⊢ (𝑥 = 𝑁 → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2
· 𝑥))↑2)) =
(((2↑(4 · 𝑁))
· ((!‘𝑁)↑4)) / ((!‘(2 · 𝑁))↑2))) |
44 | 34, 43 | eqeq12d 2775 |
. 2
⊢ (𝑥 = 𝑁 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2))))‘𝑥) =
(((2↑(4 · 𝑥))
· ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) ↔ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁) = (((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)) / ((!‘(2
· 𝑁))↑2)))) |
45 | | 1z 12036 |
. . . 4
⊢ 1 ∈
ℤ |
46 | | seq1 13416 |
. . . 4
⊢ (1 ∈
ℤ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2)))‘1)) |
47 | 45, 46 | ax-mp 5 |
. . 3
⊢ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = ((𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2)))‘1) |
48 | | 1nn 11670 |
. . . 4
⊢ 1 ∈
ℕ |
49 | | oveq2 7151 |
. . . . . . 7
⊢ (𝑘 = 1 → (2 · 𝑘) = (2 ·
1)) |
50 | 49 | oveq1d 7158 |
. . . . . 6
⊢ (𝑘 = 1 → ((2 · 𝑘)↑4) = ((2 ·
1)↑4)) |
51 | 49 | oveq1d 7158 |
. . . . . . . 8
⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1)
− 1)) |
52 | 49, 51 | oveq12d 7161 |
. . . . . . 7
⊢ (𝑘 = 1 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 1)
· ((2 · 1) − 1))) |
53 | 52 | oveq1d 7158 |
. . . . . 6
⊢ (𝑘 = 1 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2
· 1) · ((2 · 1) − 1))↑2)) |
54 | 50, 53 | oveq12d 7161 |
. . . . 5
⊢ (𝑘 = 1 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2
· 1)↑4) / (((2 · 1) · ((2 · 1) −
1))↑2))) |
55 | | eqid 2759 |
. . . . 5
⊢ (𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2))) = (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) |
56 | | ovex 7176 |
. . . . 5
⊢ (((2
· 1)↑4) / (((2 · 1) · ((2 · 1) −
1))↑2)) ∈ V |
57 | 54, 55, 56 | fvmpt 6752 |
. . . 4
⊢ (1 ∈
ℕ → ((𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1) = (((2
· 1)↑4) / (((2 · 1) · ((2 · 1) −
1))↑2))) |
58 | 48, 57 | ax-mp 5 |
. . 3
⊢ ((𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2)))‘1) = (((2 · 1)↑4) / (((2 · 1) ·
((2 · 1) − 1))↑2)) |
59 | | 2t1e2 11822 |
. . . . . 6
⊢ (2
· 1) = 2 |
60 | 59 | oveq1i 7153 |
. . . . 5
⊢ ((2
· 1)↑4) = (2↑4) |
61 | | 2exp4 16461 |
. . . . . . 7
⊢
(2↑4) = ;16 |
62 | | 1nn0 11935 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
63 | | 6nn0 11940 |
. . . . . . . 8
⊢ 6 ∈
ℕ0 |
64 | | 0nn0 11934 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
65 | | 1t1e1 11821 |
. . . . . . . . . 10
⊢ (1
· 1) = 1 |
66 | 65 | oveq1i 7153 |
. . . . . . . . 9
⊢ ((1
· 1) + 0) = (1 + 0) |
67 | | 1p0e1 11783 |
. . . . . . . . 9
⊢ (1 + 0) =
1 |
68 | 66, 67 | eqtri 2782 |
. . . . . . . 8
⊢ ((1
· 1) + 0) = 1 |
69 | | 6cn 11750 |
. . . . . . . . . 10
⊢ 6 ∈
ℂ |
70 | 69 | mulid1i 10668 |
. . . . . . . . 9
⊢ (6
· 1) = 6 |
71 | 63 | dec0h 12144 |
. . . . . . . . 9
⊢ 6 = ;06 |
72 | 70, 71 | eqtri 2782 |
. . . . . . . 8
⊢ (6
· 1) = ;06 |
73 | 62, 62, 63, 61, 63, 64, 68, 72 | decmul1c 12187 |
. . . . . . 7
⊢
((2↑4) · 1) = ;16 |
74 | 61, 73 | eqtr4i 2785 |
. . . . . 6
⊢
(2↑4) = ((2↑4) · 1) |
75 | | 2nn0 11936 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
76 | | 2t2e4 11823 |
. . . . . . . . 9
⊢ (2
· 2) = 4 |
77 | | sq1 13593 |
. . . . . . . . 9
⊢
(1↑2) = 1 |
78 | 62, 75, 76, 77, 65 | numexp2x 16455 |
. . . . . . . 8
⊢
(1↑4) = 1 |
79 | 78 | eqcomi 2768 |
. . . . . . 7
⊢ 1 =
(1↑4) |
80 | 79 | oveq2i 7154 |
. . . . . 6
⊢
((2↑4) · 1) = ((2↑4) ·
(1↑4)) |
81 | | 4cn 11744 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
82 | 81 | mulid1i 10668 |
. . . . . . . . 9
⊢ (4
· 1) = 4 |
83 | 82 | eqcomi 2768 |
. . . . . . . 8
⊢ 4 = (4
· 1) |
84 | 83 | oveq2i 7154 |
. . . . . . 7
⊢
(2↑4) = (2↑(4 · 1)) |
85 | | fac1 13672 |
. . . . . . . . 9
⊢
(!‘1) = 1 |
86 | 85 | eqcomi 2768 |
. . . . . . . 8
⊢ 1 =
(!‘1) |
87 | 86 | oveq1i 7153 |
. . . . . . 7
⊢
(1↑4) = ((!‘1)↑4) |
88 | 84, 87 | oveq12i 7155 |
. . . . . 6
⊢
((2↑4) · (1↑4)) = ((2↑(4 · 1)) ·
((!‘1)↑4)) |
89 | 74, 80, 88 | 3eqtri 2786 |
. . . . 5
⊢
(2↑4) = ((2↑(4 · 1)) ·
((!‘1)↑4)) |
90 | 60, 89 | eqtri 2782 |
. . . 4
⊢ ((2
· 1)↑4) = ((2↑(4 · 1)) ·
((!‘1)↑4)) |
91 | 59 | oveq1i 7153 |
. . . . . . . 8
⊢ ((2
· 1) − 1) = (2 − 1) |
92 | | 2m1e1 11785 |
. . . . . . . 8
⊢ (2
− 1) = 1 |
93 | 91, 92 | eqtri 2782 |
. . . . . . 7
⊢ ((2
· 1) − 1) = 1 |
94 | 93 | oveq2i 7154 |
. . . . . 6
⊢ ((2
· 1) · ((2 · 1) − 1)) = ((2 · 1) ·
1) |
95 | 59 | oveq1i 7153 |
. . . . . . 7
⊢ ((2
· 1) · 1) = (2 · 1) |
96 | 95, 59 | eqtri 2782 |
. . . . . 6
⊢ ((2
· 1) · 1) = 2 |
97 | 59 | fveq2i 6654 |
. . . . . . . 8
⊢
(!‘(2 · 1)) = (!‘2) |
98 | | fac2 13674 |
. . . . . . . 8
⊢
(!‘2) = 2 |
99 | 97, 98 | eqtri 2782 |
. . . . . . 7
⊢
(!‘(2 · 1)) = 2 |
100 | 99 | eqcomi 2768 |
. . . . . 6
⊢ 2 =
(!‘(2 · 1)) |
101 | 94, 96, 100 | 3eqtri 2786 |
. . . . 5
⊢ ((2
· 1) · ((2 · 1) − 1)) = (!‘(2 ·
1)) |
102 | 101 | oveq1i 7153 |
. . . 4
⊢ (((2
· 1) · ((2 · 1) − 1))↑2) = ((!‘(2
· 1))↑2) |
103 | 90, 102 | oveq12i 7155 |
. . 3
⊢ (((2
· 1)↑4) / (((2 · 1) · ((2 · 1) −
1))↑2)) = (((2↑(4 · 1)) · ((!‘1)↑4)) /
((!‘(2 · 1))↑2)) |
104 | 47, 58, 103 | 3eqtri 2786 |
. 2
⊢ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) =
(((2↑(4 · 1)) · ((!‘1)↑4)) / ((!‘(2
· 1))↑2)) |
105 | | elnnuz 12307 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈
(ℤ≥‘1)) |
106 | 105 | biimpi 219 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
(ℤ≥‘1)) |
107 | 106 | adantr 485 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2
· 𝑦))↑2)))
→ 𝑦 ∈
(ℤ≥‘1)) |
108 | | seqp1 13418 |
. . . . 5
⊢ (𝑦 ∈
(ℤ≥‘1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2))))‘(𝑦 +
1)) = ((seq1( · , (𝑘
∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2)))‘(𝑦 +
1)))) |
109 | 107, 108 | syl 17 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2
· 𝑦))↑2)))
→ (seq1( · , (𝑘
∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = ((seq1( · ,
(𝑘 ∈ ℕ ↦
(((2 · 𝑘)↑4) /
(((2 · 𝑘) ·
((2 · 𝑘) −
1))↑2))))‘𝑦)
· ((𝑘 ∈ ℕ
↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))) |
110 | | simpr 489 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2
· 𝑦))↑2)))
→ (seq1( · , (𝑘
∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2
· 𝑦))↑2))) |
111 | 110 | oveq1d 7158 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2
· 𝑦))↑2)))
→ ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2))))‘𝑦)
· ((𝑘 ∈ ℕ
↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = ((((2↑(4 ·
𝑦)) ·
((!‘𝑦)↑4)) /
((!‘(2 · 𝑦))↑2)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) −
1))↑2)))‘(𝑦 +
1)))) |
112 | | eqidd 2760 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2))) = (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))) |
113 | | oveq2 7151 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1))) |
114 | 113 | oveq1d 7158 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘)↑4) = ((2 · (𝑦 + 1))↑4)) |
115 | 113 | oveq1d 7158 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) −
1)) |
116 | 113, 115 | oveq12d 7161 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) · ((2 ·
(𝑦 + 1)) −
1))) |
117 | 116 | oveq1d 7158 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · (𝑦 + 1)) · ((2 ·
(𝑦 + 1)) −
1))↑2)) |
118 | 114, 117 | oveq12d 7161 |
. . . . . . . . 9
⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 ·
(𝑦 + 1)) · ((2
· (𝑦 + 1)) −
1))↑2))) |
119 | 118 | adantl 486 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2
· (𝑦 + 1))↑4) /
(((2 · (𝑦 + 1))
· ((2 · (𝑦 +
1)) − 1))↑2))) |
120 | | peano2nn 11671 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℕ) |
121 | | 2cnd 11737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 2 ∈
ℂ) |
122 | | nncn 11667 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
123 | | 1cnd 10659 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 1 ∈
ℂ) |
124 | 122, 123 | addcld 10683 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℂ) |
125 | 121, 124 | mulcld 10684 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ∈
ℂ) |
126 | | 4nn0 11938 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
127 | 126 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 4 ∈
ℕ0) |
128 | 125, 127 | expcld 13545 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1))↑4)
∈ ℂ) |
129 | 125, 123 | subcld 11020 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
1) ∈ ℂ) |
130 | 125, 129 | mulcld 10684 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) ·
((2 · (𝑦 + 1))
− 1)) ∈ ℂ) |
131 | 130 | sqcld 13543 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) ·
((2 · (𝑦 + 1))
− 1))↑2) ∈ ℂ) |
132 | | 2pos 11762 |
. . . . . . . . . . . . . 14
⊢ 0 <
2 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 0 <
2) |
134 | 133 | gt0ne0d 11227 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 2 ≠
0) |
135 | 120 | nnne0d 11709 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0) |
136 | 121, 124,
134, 135 | mulne0d 11315 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ≠
0) |
137 | | 1red 10665 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 1 ∈
ℝ) |
138 | | 2re 11733 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
139 | 138 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 2 ∈
ℝ) |
140 | | nnre 11666 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
141 | 140, 137 | readdcld 10693 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℝ) |
142 | | 1lt2 11830 |
. . . . . . . . . . . . . . 15
⊢ 1 <
2 |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 1 <
2) |
144 | | nnrp 12426 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ+) |
145 | 137, 144 | ltaddrp2d 12491 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 1 <
(𝑦 + 1)) |
146 | 139, 141,
143, 145 | mulgt1d 11599 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 1 < (2
· (𝑦 +
1))) |
147 | 137, 146 | gtned 10798 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ≠
1) |
148 | 125, 123,
147 | subne0d 11029 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
1) ≠ 0) |
149 | 125, 129,
136, 148 | mulne0d 11315 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) ·
((2 · (𝑦 + 1))
− 1)) ≠ 0) |
150 | | 2z 12038 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
151 | 150 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 2 ∈
ℤ) |
152 | 130, 149,
151 | expne0d 13551 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) ·
((2 · (𝑦 + 1))
− 1))↑2) ≠ 0) |
153 | 128, 131,
152 | divcld 11439 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1))↑4) /
(((2 · (𝑦 + 1))
· ((2 · (𝑦 +
1)) − 1))↑2)) ∈ ℂ) |
154 | 112, 119,
120, 153 | fvmptd 6759 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2)))‘(𝑦 +
1)) = (((2 · (𝑦 +
1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) −
1))↑2))) |
155 | 154 | oveq2d 7159 |
. . . . . 6
⊢ (𝑦 ∈ ℕ →
((((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · ((𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2)))‘(𝑦 +
1))) = ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · (((2
· (𝑦 + 1))↑4) /
(((2 · (𝑦 + 1))
· ((2 · (𝑦 +
1)) − 1))↑2)))) |
156 | | nnnn0 11926 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
157 | 127, 156 | nn0mulcld 11984 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (4
· 𝑦) ∈
ℕ0) |
158 | 121, 157 | expcld 13545 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(2↑(4 · 𝑦))
∈ ℂ) |
159 | | faccl 13678 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (!‘𝑦) ∈
ℕ) |
160 | | nncn 11667 |
. . . . . . . . . . 11
⊢
((!‘𝑦) ∈
ℕ → (!‘𝑦)
∈ ℂ) |
161 | 156, 159,
160 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(!‘𝑦) ∈
ℂ) |
162 | 161, 127 | expcld 13545 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
((!‘𝑦)↑4) ∈
ℂ) |
163 | 158, 162 | mulcld 10684 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) ∈ ℂ) |
164 | 75 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 2 ∈
ℕ0) |
165 | 164, 156 | nn0mulcld 11984 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℕ0) |
166 | | faccl 13678 |
. . . . . . . . . 10
⊢ ((2
· 𝑦) ∈
ℕ0 → (!‘(2 · 𝑦)) ∈ ℕ) |
167 | | nncn 11667 |
. . . . . . . . . 10
⊢
((!‘(2 · 𝑦)) ∈ ℕ → (!‘(2 ·
𝑦)) ∈
ℂ) |
168 | 165, 166,
167 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(!‘(2 · 𝑦))
∈ ℂ) |
169 | 168 | sqcld 13543 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
((!‘(2 · 𝑦))↑2) ∈ ℂ) |
170 | 165, 166 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(!‘(2 · 𝑦))
∈ ℕ) |
171 | 170 | nnne0d 11709 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(!‘(2 · 𝑦))
≠ 0) |
172 | 168, 171,
151 | expne0d 13551 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
((!‘(2 · 𝑦))↑2) ≠ 0) |
173 | 163, 169,
128, 131, 172, 152 | divmuldivd 11480 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ →
((((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · (((2
· (𝑦 + 1))↑4) /
(((2 · (𝑦 + 1))
· ((2 · (𝑦 +
1)) − 1))↑2))) = ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) / (((!‘(2
· 𝑦))↑2)
· (((2 · (𝑦 +
1)) · ((2 · (𝑦 + 1)) −
1))↑2)))) |
174 | 121, 124,
127 | mulexpd 13560 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1))↑4) =
((2↑4) · ((𝑦 +
1)↑4))) |
175 | 174 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) = (((2↑(4
· 𝑦)) ·
((!‘𝑦)↑4))
· ((2↑4) · ((𝑦 + 1)↑4)))) |
176 | 121, 127 | expcld 13545 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(2↑4) ∈ ℂ) |
177 | 124, 127 | expcld 13545 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((𝑦 + 1)↑4) ∈
ℂ) |
178 | 158, 162,
176, 177 | mul4d 10875 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) · ((2↑4) ·
((𝑦 + 1)↑4))) =
(((2↑(4 · 𝑦))
· (2↑4)) · (((!‘𝑦)↑4) · ((𝑦 + 1)↑4)))) |
179 | 161, 124,
127 | mulexpd 13560 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ →
(((!‘𝑦) ·
(𝑦 + 1))↑4) =
(((!‘𝑦)↑4)
· ((𝑦 +
1)↑4))) |
180 | 179 | eqcomd 2765 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(((!‘𝑦)↑4)
· ((𝑦 + 1)↑4))
= (((!‘𝑦) ·
(𝑦 +
1))↑4)) |
181 | 180 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(((2↑(4 · 𝑦))
· (2↑4)) · (((!‘𝑦)↑4) · ((𝑦 + 1)↑4))) = (((2↑(4 · 𝑦)) · (2↑4)) ·
(((!‘𝑦) ·
(𝑦 +
1))↑4))) |
182 | 175, 178,
181 | 3eqtrd 2798 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
(((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) = (((2↑(4
· 𝑦)) ·
(2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4))) |
183 | 121, 122 | mulcld 10684 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℂ) |
184 | 183, 123 | addcld 10683 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 1) ∈
ℂ) |
185 | 125, 184 | mulcomd 10685 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) ·
((2 · 𝑦) + 1)) =
(((2 · 𝑦) + 1)
· (2 · (𝑦 +
1)))) |
186 | 185 | oveq2d 7159 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ →
((!‘(2 · 𝑦))
· ((2 · (𝑦 +
1)) · ((2 · 𝑦) + 1))) = ((!‘(2 · 𝑦)) · (((2 · 𝑦) + 1) · (2 ·
(𝑦 +
1))))) |
187 | 121, 122,
123 | adddid 10688 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) = ((2
· 𝑦) + (2 ·
1))) |
188 | 187 | oveq1d 7158 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
1) = (((2 · 𝑦) + (2
· 1)) − 1)) |
189 | 59, 121 | eqeltrid 2855 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (2
· 1) ∈ ℂ) |
190 | 183, 189,
123 | addsubassd 11040 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + (2 ·
1)) − 1) = ((2 · 𝑦) + ((2 · 1) −
1))) |
191 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → (2
· 1) = 2) |
192 | 191 | oveq1d 7158 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → ((2
· 1) − 1) = (2 − 1)) |
193 | 192, 92 | eqtrdi 2810 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → ((2
· 1) − 1) = 1) |
194 | 193 | oveq2d 7159 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + ((2 ·
1) − 1)) = ((2 · 𝑦) + 1)) |
195 | 188, 190,
194 | 3eqtrd 2798 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
1) = ((2 · 𝑦) +
1)) |
196 | 195 | oveq2d 7159 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) ·
((2 · (𝑦 + 1))
− 1)) = ((2 · (𝑦 + 1)) · ((2 · 𝑦) + 1))) |
197 | 196 | oveq2d 7159 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ →
((!‘(2 · 𝑦))
· ((2 · (𝑦 +
1)) · ((2 · (𝑦 + 1)) − 1))) = ((!‘(2 ·
𝑦)) · ((2 ·
(𝑦 + 1)) · ((2
· 𝑦) +
1)))) |
198 | 168, 184,
125 | mulassd 10687 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ →
(((!‘(2 · 𝑦))
· ((2 · 𝑦) +
1)) · (2 · (𝑦
+ 1))) = ((!‘(2 · 𝑦)) · (((2 · 𝑦) + 1) · (2 · (𝑦 + 1))))) |
199 | 186, 197,
198 | 3eqtr4d 2804 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
((!‘(2 · 𝑦))
· ((2 · (𝑦 +
1)) · ((2 · (𝑦 + 1)) − 1))) = (((!‘(2 ·
𝑦)) · ((2 ·
𝑦) + 1)) · (2
· (𝑦 +
1)))) |
200 | 199 | oveq1d 7158 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(((!‘(2 · 𝑦))
· ((2 · (𝑦 +
1)) · ((2 · (𝑦 + 1)) − 1)))↑2) = ((((!‘(2
· 𝑦)) · ((2
· 𝑦) + 1)) ·
(2 · (𝑦 +
1)))↑2)) |
201 | 168, 130,
164 | mulexpd 13560 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(((!‘(2 · 𝑦))
· ((2 · (𝑦 +
1)) · ((2 · (𝑦 + 1)) − 1)))↑2) = (((!‘(2
· 𝑦))↑2)
· (((2 · (𝑦 +
1)) · ((2 · (𝑦 + 1)) − 1))↑2))) |
202 | | df-2 11722 |
. . . . . . . . . . . . . . 15
⊢ 2 = (1 +
1) |
203 | 202 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 2 = (1 +
1)) |
204 | 203 | oveq2d 7159 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 2) = ((2
· 𝑦) + (1 +
1))) |
205 | 183, 123,
123 | addassd 10686 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) + 1) = ((2
· 𝑦) + (1 +
1))) |
206 | 204, 205 | eqtr4d 2797 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 2) = (((2
· 𝑦) + 1) +
1)) |
207 | 206 | fveq2d 6655 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ →
(!‘((2 · 𝑦) +
2)) = (!‘(((2 · 𝑦) + 1) + 1))) |
208 | 62 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 1 ∈
ℕ0) |
209 | 165, 208 | nn0addcld 11983 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 1) ∈
ℕ0) |
210 | | facp1 13673 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑦) + 1) ∈
ℕ0 → (!‘(((2 · 𝑦) + 1) + 1)) = ((!‘((2 · 𝑦) + 1)) · (((2 ·
𝑦) + 1) +
1))) |
211 | 209, 210 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ →
(!‘(((2 · 𝑦) +
1) + 1)) = ((!‘((2 · 𝑦) + 1)) · (((2 · 𝑦) + 1) + 1))) |
212 | | facp1 13673 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑦) ∈
ℕ0 → (!‘((2 · 𝑦) + 1)) = ((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1))) |
213 | 165, 212 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ →
(!‘((2 · 𝑦) +
1)) = ((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1))) |
214 | 203 | eqcomd 2765 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (1 + 1) =
2) |
215 | 214 | oveq2d 7159 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + (1 + 1)) =
((2 · 𝑦) +
2)) |
216 | 214, 202,
59 | 3eqtr4g 2819 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 2 = (2
· 1)) |
217 | 216 | oveq2d 7159 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 2) = ((2
· 𝑦) + (2 ·
1))) |
218 | 217, 187 | eqtr4d 2797 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 2) = (2
· (𝑦 +
1))) |
219 | 205, 215,
218 | 3eqtrd 2798 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) + 1) = (2
· (𝑦 +
1))) |
220 | 213, 219 | oveq12d 7161 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ →
((!‘((2 · 𝑦) +
1)) · (((2 · 𝑦) + 1) + 1)) = (((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 ·
(𝑦 + 1)))) |
221 | 207, 211,
220 | 3eqtrrd 2799 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(((!‘(2 · 𝑦))
· ((2 · 𝑦) +
1)) · (2 · (𝑦
+ 1))) = (!‘((2 · 𝑦) + 2))) |
222 | 221 | oveq1d 7158 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
((((!‘(2 · 𝑦))
· ((2 · 𝑦) +
1)) · (2 · (𝑦
+ 1)))↑2) = ((!‘((2 · 𝑦) + 2))↑2)) |
223 | 200, 201,
222 | 3eqtr3d 2802 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
(((!‘(2 · 𝑦))↑2) · (((2 · (𝑦 + 1)) · ((2 ·
(𝑦 + 1)) −
1))↑2)) = ((!‘((2 · 𝑦) + 2))↑2)) |
224 | 182, 223 | oveq12d 7161 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ →
((((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) / (((!‘(2
· 𝑦))↑2)
· (((2 · (𝑦 +
1)) · ((2 · (𝑦 + 1)) − 1))↑2))) = ((((2↑(4
· 𝑦)) ·
(2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) / ((!‘((2 ·
𝑦) +
2))↑2))) |
225 | 173, 224 | eqtrd 2794 |
. . . . . 6
⊢ (𝑦 ∈ ℕ →
((((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · (((2
· (𝑦 + 1))↑4) /
(((2 · (𝑦 + 1))
· ((2 · (𝑦 +
1)) − 1))↑2))) = ((((2↑(4 · 𝑦)) · (2↑4)) ·
(((!‘𝑦) ·
(𝑦 + 1))↑4)) /
((!‘((2 · 𝑦) +
2))↑2))) |
226 | 83 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 4 = (4
· 1)) |
227 | 226 | oveq2d 7159 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((4
· 𝑦) + 4) = ((4
· 𝑦) + (4 ·
1))) |
228 | 227 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(2↑((4 · 𝑦) +
4)) = (2↑((4 · 𝑦) + (4 · 1)))) |
229 | 121, 127,
157 | expaddd 13547 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(2↑((4 · 𝑦) +
4)) = ((2↑(4 · 𝑦)) · (2↑4))) |
230 | 81 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 4 ∈
ℂ) |
231 | 230, 122,
123 | adddid 10688 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (4
· (𝑦 + 1)) = ((4
· 𝑦) + (4 ·
1))) |
232 | 231 | eqcomd 2765 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((4
· 𝑦) + (4 ·
1)) = (4 · (𝑦 +
1))) |
233 | 232 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(2↑((4 · 𝑦) +
(4 · 1))) = (2↑(4 · (𝑦 + 1)))) |
234 | 228, 229,
233 | 3eqtr3d 2802 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
((2↑(4 · 𝑦))
· (2↑4)) = (2↑(4 · (𝑦 + 1)))) |
235 | | facp1 13673 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (!‘(𝑦 + 1)) =
((!‘𝑦) ·
(𝑦 + 1))) |
236 | 156, 235 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(!‘(𝑦 + 1)) =
((!‘𝑦) ·
(𝑦 + 1))) |
237 | 236 | eqcomd 2765 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
((!‘𝑦) ·
(𝑦 + 1)) = (!‘(𝑦 + 1))) |
238 | 237 | oveq1d 7158 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
(((!‘𝑦) ·
(𝑦 + 1))↑4) =
((!‘(𝑦 +
1))↑4)) |
239 | 234, 238 | oveq12d 7161 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ →
(((2↑(4 · 𝑦))
· (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) = ((2↑(4 · (𝑦 + 1))) ·
((!‘(𝑦 +
1))↑4))) |
240 | 218 | fveq2d 6655 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
(!‘((2 · 𝑦) +
2)) = (!‘(2 · (𝑦 + 1)))) |
241 | 240 | oveq1d 7158 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ →
((!‘((2 · 𝑦) +
2))↑2) = ((!‘(2 · (𝑦 + 1)))↑2)) |
242 | 239, 241 | oveq12d 7161 |
. . . . . 6
⊢ (𝑦 ∈ ℕ →
((((2↑(4 · 𝑦))
· (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) / ((!‘((2 ·
𝑦) + 2))↑2)) =
(((2↑(4 · (𝑦 +
1))) · ((!‘(𝑦
+ 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2))) |
243 | 155, 225,
242 | 3eqtrd 2798 |
. . . . 5
⊢ (𝑦 ∈ ℕ →
((((2↑(4 · 𝑦))
· ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · ((𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2)))‘(𝑦 +
1))) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2
· (𝑦 +
1)))↑2))) |
244 | 243 | adantr 485 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2
· 𝑦))↑2)))
→ ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · ((𝑘 ∈ ℕ ↦ (((2
· 𝑘)↑4) / (((2
· 𝑘) · ((2
· 𝑘) −
1))↑2)))‘(𝑦 +
1))) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2
· (𝑦 +
1)))↑2))) |
245 | 109, 111,
244 | 3eqtrd 2798 |
. . 3
⊢ ((𝑦 ∈ ℕ ∧ (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2
· 𝑦))↑2)))
→ (seq1( · , (𝑘
∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = (((2↑(4 ·
(𝑦 + 1))) ·
((!‘(𝑦 + 1))↑4))
/ ((!‘(2 · (𝑦
+ 1)))↑2))) |
246 | 245 | ex 417 |
. 2
⊢ (𝑦 ∈ ℕ → ((seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2
· 𝑦))↑2))
→ (seq1( · , (𝑘
∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = (((2↑(4 ·
(𝑦 + 1))) ·
((!‘(𝑦 + 1))↑4))
/ ((!‘(2 · (𝑦
+ 1)))↑2)))) |
247 | 11, 22, 33, 44, 104, 246 | nnind 11677 |
1
⊢ (𝑁 ∈ ℕ → (seq1(
· , (𝑘 ∈
ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁) = (((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)) / ((!‘(2
· 𝑁))↑2))) |