Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wallispi2lem1 Structured version   Visualization version   GIF version

Theorem wallispi2lem1 42233
Description: An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
Assertion
Ref Expression
wallispi2lem1 (𝑁 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)))

Proof of Theorem wallispi2lem1
Dummy variables 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6663 . . 3 (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1))
2 oveq2 7153 . . . . . 6 (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
32oveq1d 7160 . . . . 5 (𝑥 = 1 → ((2 · 𝑥) + 1) = ((2 · 1) + 1))
43oveq2d 7161 . . . 4 (𝑥 = 1 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 1) + 1)))
5 fveq2 6663 . . . 4 (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
64, 5oveq12d 7163 . . 3 (𝑥 = 1 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1)))
71, 6eqeq12d 2834 . 2 (𝑥 = 1 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))))
8 fveq2 6663 . . 3 (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦))
9 oveq2 7153 . . . . . 6 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
109oveq1d 7160 . . . . 5 (𝑥 = 𝑦 → ((2 · 𝑥) + 1) = ((2 · 𝑦) + 1))
1110oveq2d 7161 . . . 4 (𝑥 = 𝑦 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑦) + 1)))
12 fveq2 6663 . . . 4 (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))
1311, 12oveq12d 7163 . . 3 (𝑥 = 𝑦 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)))
148, 13eqeq12d 2834 . 2 (𝑥 = 𝑦 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))))
15 fveq2 6663 . . 3 (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)))
16 oveq2 7153 . . . . . 6 (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
1716oveq1d 7160 . . . . 5 (𝑥 = (𝑦 + 1) → ((2 · 𝑥) + 1) = ((2 · (𝑦 + 1)) + 1))
1817oveq2d 7161 . . . 4 (𝑥 = (𝑦 + 1) → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · (𝑦 + 1)) + 1)))
19 fveq2 6663 . . . 4 (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
2018, 19oveq12d 7163 . . 3 (𝑥 = (𝑦 + 1) → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
2115, 20eqeq12d 2834 . 2 (𝑥 = (𝑦 + 1) → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))))
22 fveq2 6663 . . 3 (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁))
23 oveq2 7153 . . . . . 6 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
2423oveq1d 7160 . . . . 5 (𝑥 = 𝑁 → ((2 · 𝑥) + 1) = ((2 · 𝑁) + 1))
2524oveq2d 7161 . . . 4 (𝑥 = 𝑁 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑁) + 1)))
26 fveq2 6663 . . . 4 (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁))
2725, 26oveq12d 7163 . . 3 (𝑥 = 𝑁 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)))
2822, 27eqeq12d 2834 . 2 (𝑥 = 𝑁 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁))))
29 1z 12000 . . . 4 1 ∈ ℤ
30 seq1 13370 . . . 4 (1 ∈ ℤ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘1))
3129, 30ax-mp 5 . . 3 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘1)
32 1nn 11637 . . . 4 1 ∈ ℕ
33 oveq2 7153 . . . . . . 7 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
3433oveq1d 7160 . . . . . . 7 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
3533, 34oveq12d 7163 . . . . . 6 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 1) / ((2 · 1) − 1)))
3633oveq1d 7160 . . . . . . 7 (𝑘 = 1 → ((2 · 𝑘) + 1) = ((2 · 1) + 1))
3733, 36oveq12d 7163 . . . . . 6 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 1) / ((2 · 1) + 1)))
3835, 37oveq12d 7163 . . . . 5 (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))))
39 eqid 2818 . . . . 5 (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
40 ovex 7178 . . . . 5 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) ∈ V
4138, 39, 40fvmpt 6761 . . . 4 (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘1) = (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))))
4232, 41ax-mp 5 . . 3 ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘1) = (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1)))
43 2t1e2 11788 . . . . . . 7 (2 · 1) = 2
4443oveq1i 7155 . . . . . . . 8 ((2 · 1) − 1) = (2 − 1)
45 2m1e1 11751 . . . . . . . 8 (2 − 1) = 1
4644, 45eqtri 2841 . . . . . . 7 ((2 · 1) − 1) = 1
4743, 46oveq12i 7157 . . . . . 6 ((2 · 1) / ((2 · 1) − 1)) = (2 / 1)
4843oveq1i 7155 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
49 2p1e3 11767 . . . . . . . 8 (2 + 1) = 3
5048, 49eqtri 2841 . . . . . . 7 ((2 · 1) + 1) = 3
5143, 50oveq12i 7157 . . . . . 6 ((2 · 1) / ((2 · 1) + 1)) = (2 / 3)
5247, 51oveq12i 7157 . . . . 5 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = ((2 / 1) · (2 / 3))
53 2cn 11700 . . . . . 6 2 ∈ ℂ
54 ax-1cn 10583 . . . . . 6 1 ∈ ℂ
55 3cn 11706 . . . . . 6 3 ∈ ℂ
56 ax-1ne0 10594 . . . . . 6 1 ≠ 0
57 3ne0 11731 . . . . . 6 3 ≠ 0
5853, 54, 53, 55, 56, 57divmuldivi 11388 . . . . 5 ((2 / 1) · (2 / 3)) = ((2 · 2) / (1 · 3))
59 2t2e4 11789 . . . . . 6 (2 · 2) = 4
6055mulid2i 10634 . . . . . 6 (1 · 3) = 3
6159, 60oveq12i 7157 . . . . 5 ((2 · 2) / (1 · 3)) = (4 / 3)
6252, 58, 613eqtri 2845 . . . 4 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = (4 / 3)
63 4cn 11710 . . . . 5 4 ∈ ℂ
64 divrec2 11303 . . . . 5 ((4 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (4 / 3) = ((1 / 3) · 4))
6563, 55, 57, 64mp3an 1452 . . . 4 (4 / 3) = ((1 / 3) · 4)
6650eqcomi 2827 . . . . . 6 3 = ((2 · 1) + 1)
6766oveq2i 7156 . . . . 5 (1 / 3) = (1 / ((2 · 1) + 1))
68 seq1 13370 . . . . . . . 8 (1 ∈ ℤ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1))
6929, 68ax-mp 5 . . . . . . 7 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1)
7033oveq1d 7160 . . . . . . . . . 10 (𝑘 = 1 → ((2 · 𝑘)↑4) = ((2 · 1)↑4))
7133, 34oveq12d 7163 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 1) · ((2 · 1) − 1)))
7271oveq1d 7160 . . . . . . . . . 10 (𝑘 = 1 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 1) · ((2 · 1) − 1))↑2))
7370, 72oveq12d 7163 . . . . . . . . 9 (𝑘 = 1 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
74 eqid 2818 . . . . . . . . 9 (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))
75 ovex 7178 . . . . . . . . 9 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) ∈ V
7673, 74, 75fvmpt 6761 . . . . . . . 8 (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
7732, 76ax-mp 5 . . . . . . 7 ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2))
7843oveq1i 7155 . . . . . . . . 9 ((2 · 1)↑4) = (2↑4)
7943, 46oveq12i 7157 . . . . . . . . . . 11 ((2 · 1) · ((2 · 1) − 1)) = (2 · 1)
8079, 43eqtri 2841 . . . . . . . . . 10 ((2 · 1) · ((2 · 1) − 1)) = 2
8180oveq1i 7155 . . . . . . . . 9 (((2 · 1) · ((2 · 1) − 1))↑2) = (2↑2)
8278, 81oveq12i 7157 . . . . . . . 8 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = ((2↑4) / (2↑2))
83 2exp4 16409 . . . . . . . . . 10 (2↑4) = 16
84 sq2 13548 . . . . . . . . . 10 (2↑2) = 4
8583, 84oveq12i 7157 . . . . . . . . 9 ((2↑4) / (2↑2)) = (16 / 4)
86 4t4e16 12185 . . . . . . . . . . 11 (4 · 4) = 16
8786eqcomi 2827 . . . . . . . . . 10 16 = (4 · 4)
8887oveq1i 7155 . . . . . . . . 9 (16 / 4) = ((4 · 4) / 4)
89 4ne0 11733 . . . . . . . . . 10 4 ≠ 0
9063, 63, 89divcan3i 11374 . . . . . . . . 9 ((4 · 4) / 4) = 4
9185, 88, 903eqtri 2845 . . . . . . . 8 ((2↑4) / (2↑2)) = 4
9282, 91eqtri 2841 . . . . . . 7 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = 4
9369, 77, 923eqtri 2845 . . . . . 6 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = 4
9493eqcomi 2827 . . . . 5 4 = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1)
9567, 94oveq12i 7157 . . . 4 ((1 / 3) · 4) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
9662, 65, 953eqtri 2845 . . 3 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
9731, 42, 963eqtri 2845 . 2 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
98 elnnuz 12270 . . . . . . 7 (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ‘1))
9998biimpi 217 . . . . . 6 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘1))
10099adantr 481 . . . . 5 ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → 𝑦 ∈ (ℤ‘1))
101 seqp1 13372 . . . . 5 (𝑦 ∈ (ℤ‘1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))))
102100, 101syl 17 . . . 4 ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))))
103 simpr 485 . . . . 5 ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)))
104103oveq1d 7160 . . . 4 ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))))
105 eqidd 2819 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))
106 oveq2 7153 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
107106oveq1d 7160 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
108106, 107oveq12d 7163 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
109106oveq1d 7160 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
110106, 109oveq12d 7163 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
111108, 110oveq12d 7163 . . . . . . . . . 10 (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
112111adantl 482 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
113 peano2nn 11638 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
114 2rp 12382 . . . . . . . . . . . . 13 2 ∈ ℝ+
115114a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ∈ ℝ+)
116 nnre 11633 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
117 nnnn0 11892 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
118117nn0ge0d 11946 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ 𝑦)
119116, 118ge0p1rpd 12449 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ+)
120115, 119rpmulcld 12435 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ+)
121 2re 11699 . . . . . . . . . . . . . . 15 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℝ)
123 1red 10630 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ∈ ℝ)
124116, 123readdcld 10658 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
125122, 124remulcld 10659 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
126125, 123resubcld 11056 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
127 1lt2 11796 . . . . . . . . . . . . . . 15 1 < 2
128127a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 < 2)
129 nnrp 12388 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
130123, 129ltaddrp2d 12453 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
131122, 124, 128, 130mulgt1d 11564 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
132123, 125posdifd 11215 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 < (2 · (𝑦 + 1)) ↔ 0 < ((2 · (𝑦 + 1)) − 1)))
133131, 132mpbid 233 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 0 < ((2 · (𝑦 + 1)) − 1))
134126, 133elrpd 12416 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ+)
135120, 134rpdivcld 12436 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ+)
136115rpge0d 12423 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ 2)
137 0le1 11151 . . . . . . . . . . . . . . 15 0 ≤ 1
138137a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ 1)
139116, 123, 118, 138addge0d 11204 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ (𝑦 + 1))
140122, 124, 136, 139mulge0d 11205 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 0 ≤ (2 · (𝑦 + 1)))
141125, 140ge0p1rpd 12449 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ+)
142120, 141rpdivcld 12436 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ+)
143135, 142rpmulcld 12435 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ+)
144105, 112, 113, 143fvmptd 6767 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
145144oveq2d 7161 . . . . . . 7 (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
146125recnd 10657 . . . . . . . . . 10 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
147126recnd 10657 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℂ)
148141rpcnd 12421 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℂ)
149133gt0ne0d 11192 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
150141rpne0d 12424 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
151146, 147, 146, 148, 149, 150divmuldivd 11445 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
152146, 146mulcld 10649 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
153152, 147, 148, 149, 150divdiv1d 11435 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
154146sqvald 13495 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))
155154eqcomd 2824 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) = ((2 · (𝑦 + 1))↑2))
156155oveq1d 7160 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) = (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))
157156oveq1d 7160 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
158151, 153, 1573eqtr2d 2859 . . . . . . . 8 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
159158oveq2d 7161 . . . . . . 7 (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1))))
160146sqcld 13496 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ∈ ℂ)
161160, 147, 149divcld 11404 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
162161, 148, 150divrec2d 11408 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))))
163162oveq2d 7161 . . . . . . . 8 (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1))) = (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((1 / ((2 · (𝑦 + 1)) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))))
164 2cnd 11703 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ∈ ℂ)
165 nncn 11634 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
166164, 165mulcld 10649 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
167 1cnd 10624 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 1 ∈ ℂ)
168166, 167addcld 10648 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
169 2nn 11698 . . . . . . . . . . . . . . 15 2 ∈ ℕ
170169a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℕ)
171 id 22 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ)
172170, 171nnmulcld 11678 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ)
173172peano2nnd 11643 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℕ)
174173nnne0d 11675 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
175168, 174reccld 11397 . . . . . . . . . 10 (𝑦 ∈ ℕ → (1 / ((2 · 𝑦) + 1)) ∈ ℂ)
176 eqidd 2819 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
177 oveq2 7153 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
178177oveq1d 7160 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → ((2 · 𝑘)↑4) = ((2 · 𝑥)↑4))
179177oveq1d 7160 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → ((2 · 𝑘) − 1) = ((2 · 𝑥) − 1))
180177, 179oveq12d 7163 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 𝑥) · ((2 · 𝑥) − 1)))
181180oveq1d 7160 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2))
182178, 181oveq12d 7163 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
183182adantl 482 . . . . . . . . . . . . 13 (((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) ∧ 𝑘 = 𝑥) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
184 elfznn 12924 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...𝑦) → 𝑥 ∈ ℕ)
185184adantl 482 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → 𝑥 ∈ ℕ)
186169a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ∈ ℕ)
187 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
188186, 187nnmulcld 11678 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℕ)
189 4nn0 11904 . . . . . . . . . . . . . . . . . . 19 4 ∈ ℕ0
190189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → 4 ∈ ℕ0)
191188, 190nnexpcld 13594 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℕ)
192191nncnd 11642 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℂ)
193 2cnd 11703 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ∈ ℂ)
194 nncn 11634 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ∈ ℂ)
195193, 194mulcld 10649 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℂ)
196 1cnd 10624 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 1 ∈ ℂ)
197195, 196subcld 10985 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ∈ ℂ)
198195, 197mulcld 10649 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ∈ ℂ)
199198sqcld 13496 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ∈ ℂ)
200186nnne0d 11675 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ≠ 0)
201 nnne0 11659 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ≠ 0)
202193, 194, 200, 201mulne0d 11280 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 0)
203 1red 10630 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℕ → 1 ∈ ℝ)
204121a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 2 ∈ ℝ)
205204, 203remulcld 10659 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 1) ∈ ℝ)
206 nnre 11633 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
207204, 206remulcld 10659 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℝ)
20843a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → (2 · 1) = 2)
209127, 208breqtrrid 5095 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → 1 < (2 · 1))
210 0le2 11727 . . . . . . . . . . . . . . . . . . . . . . 23 0 ≤ 2
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 0 ≤ 2)
212 nnge1 11653 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 1 ≤ 𝑥)
213203, 206, 204, 211, 212lemul2ad 11568 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 1) ≤ (2 · 𝑥))
214203, 205, 207, 209, 213ltletrd 10788 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℕ → 1 < (2 · 𝑥))
215203, 214gtned 10763 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 1)
216195, 196, 215subne0d 10994 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ≠ 0)
217195, 197, 202, 216mulne0d 11280 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ≠ 0)
218 2z 12002 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
219218a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → 2 ∈ ℤ)
220198, 217, 219expne0d 13504 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ≠ 0)
221192, 199, 220divcld 11404 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
222184, 221syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...𝑦) → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
223222adantl 482 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
224176, 183, 185, 223fvmptd 6767 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
225224, 223eqeltrd 2910 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) ∈ ℂ)
226 mulcl 10609 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑥 · 𝑤) ∈ ℂ)
227226adantl 482 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑥 · 𝑤) ∈ ℂ)
22899, 225, 227seqcl 13378 . . . . . . . . . 10 (𝑦 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) ∈ ℂ)
229175, 228mulcld 10649 . . . . . . . . 9 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) ∈ ℂ)
230148, 150reccld 11397 . . . . . . . . 9 (𝑦 ∈ ℕ → (1 / ((2 · (𝑦 + 1)) + 1)) ∈ ℂ)
231229, 230, 161mul12d 10837 . . . . . . . 8 (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((1 / ((2 · (𝑦 + 1)) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))))
232175, 228mulcomd 10650 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (1 / ((2 · 𝑦) + 1))))
233232oveq1d 7160 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = (((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (1 / ((2 · 𝑦) + 1))) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))))
234228, 175, 161mulassd 10652 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (1 / ((2 · 𝑦) + 1))) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))))
235167, 168, 160, 147, 174, 149divmuldivd 11445 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))))
236160mulid2d 10647 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 · ((2 · (𝑦 + 1))↑2)) = ((2 · (𝑦 + 1))↑2))
237164, 165, 167adddid 10653 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
23843a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → (2 · 1) = 2)
239238oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
240237, 239eqtrd 2853 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
241240oveq1d 7160 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
242166, 164, 167addsubassd 11005 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
24345a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 − 1) = 1)
244243oveq2d 7161 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
245241, 242, 2443eqtrd 2857 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
246245oveq2d 7161 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
247168sqvald 13495 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
248246, 247eqtr4d 2856 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1)↑2))
249236, 248oveq12d 7163 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)))
250 2p2e4 11760 . . . . . . . . . . . . . . . . . 18 (2 + 2) = 4
25153, 53, 250mvlladdi 10892 . . . . . . . . . . . . . . . . 17 2 = (4 − 2)
252251a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 = (4 − 2))
253252oveq2d 7161 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1))↑(4 − 2)))
254120rpne0d 12424 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
255218a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ∈ ℤ)
256 4z 12004 . . . . . . . . . . . . . . . . 17 4 ∈ ℤ
257256a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 4 ∈ ℤ)
258146, 254, 255, 257expsubd 13509 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑(4 − 2)) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
259253, 258eqtrd 2853 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
260245eqcomd 2824 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) = ((2 · (𝑦 + 1)) − 1))
261260oveq1d 7160 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · (𝑦 + 1)) − 1)↑2))
262259, 261oveq12d 7163 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)))
263146, 254, 257expclzd 13503 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑4) ∈ ℂ)
264147sqcld 13496 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ∈ ℂ)
265165, 167addcld 10648 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
266170nnne0d 11675 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ≠ 0)
267113nnne0d 11675 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
268164, 265, 266, 267mulne0d 11280 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
269146, 268, 255expne0d 13504 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ≠ 0)
270147, 149, 255expne0d 13504 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ≠ 0)
271263, 160, 264, 269, 270divdiv1d 11435 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))))
272146, 147sqmuld 13510 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) = (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)))
273272eqcomd 2824 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
274273oveq2d 7161 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
275262, 271, 2743eqtrd 2857 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
276235, 249, 2753eqtrd 2857 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
277276oveq2d 7161 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))))
278233, 234, 2773eqtrd 2857 . . . . . . . . 9 (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))))
279278oveq2d 7161 . . . . . . . 8 (𝑦 ∈ ℕ → ((1 / ((2 · (𝑦 + 1)) + 1)) · (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))))
280163, 231, 2793eqtrd 2857 . . . . . . 7 (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))))
281145, 159, 2803eqtrd 2857 . . . . . 6 (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))))
282 eqidd 2819 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
283 simpr 485 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → 𝑘 = (𝑦 + 1))
284283oveq2d 7161 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (2 · 𝑘) = (2 · (𝑦 + 1)))
285284oveq1d 7160 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘)↑4) = ((2 · (𝑦 + 1))↑4))
286284oveq1d 7160 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
287284, 286oveq12d 7163 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))
288287oveq1d 7160 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
289285, 288oveq12d 7163 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
290146, 147mulcld 10649 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
291290sqcld 13496 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ∈ ℂ)
292146, 147, 254, 149mulne0d 11280 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ≠ 0)
293290, 292, 255expne0d 13504 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ≠ 0)
294263, 291, 293divcld 11404 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) ∈ ℂ)
295282, 289, 113, 294fvmptd 6767 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
296295eqcomd 2824 . . . . . . . 8 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))
297296oveq2d 7161 . . . . . . 7 (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
298297oveq2d 7161 . . . . . 6 (𝑦 ∈ ℕ → ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))))
299 seqp1 13372 . . . . . . . . 9 (𝑦 ∈ (ℤ‘1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
30099, 299syl 17 . . . . . . . 8 (𝑦 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
301300eqcomd 2824 . . . . . . 7 (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
302301oveq2d 7161 . . . . . 6 (𝑦 ∈ ℕ → ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
303281, 298, 3023eqtrd 2857 . . . . 5 (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
304303adantr 481 . . . 4 ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
305102, 104, 3043eqtrd 2857 . . 3 ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
306305ex 413 . 2 (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))))
3077, 14, 21, 28, 97, 306nnind 11644 1 (𝑁 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wne 3013   class class class wbr 5057  cmpt 5137  cfv 6348  (class class class)co 7145  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530   < clt 10663  cle 10664  cmin 10858   / cdiv 11285  cn 11626  2c2 11680  3c3 11681  4c4 11682  6c6 11684  0cn0 11885  cz 11969  cdc 12086  cuz 12231  +crp 12377  ...cfz 12880  seqcseq 13357  cexp 13417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-rp 12378  df-fz 12881  df-seq 13358  df-exp 13418
This theorem is referenced by:  wallispi2  42235
  Copyright terms: Public domain W3C validator