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 40606
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 6229 . . 3 (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1))
2 oveq2 6698 . . . . . 6 (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
32oveq1d 6705 . . . . 5 (𝑥 = 1 → ((2 · 𝑥) + 1) = ((2 · 1) + 1))
43oveq2d 6706 . . . 4 (𝑥 = 1 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 1) + 1)))
5 fveq2 6229 . . . 4 (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
64, 5oveq12d 6708 . . 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 2666 . 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 6229 . . 3 (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦))
9 oveq2 6698 . . . . . 6 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
109oveq1d 6705 . . . . 5 (𝑥 = 𝑦 → ((2 · 𝑥) + 1) = ((2 · 𝑦) + 1))
1110oveq2d 6706 . . . 4 (𝑥 = 𝑦 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑦) + 1)))
12 fveq2 6229 . . . 4 (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))
1311, 12oveq12d 6708 . . 3 (𝑥 = 𝑦 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)))
148, 13eqeq12d 2666 . 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 6229 . . 3 (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)))
16 oveq2 6698 . . . . . 6 (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
1716oveq1d 6705 . . . . 5 (𝑥 = (𝑦 + 1) → ((2 · 𝑥) + 1) = ((2 · (𝑦 + 1)) + 1))
1817oveq2d 6706 . . . 4 (𝑥 = (𝑦 + 1) → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · (𝑦 + 1)) + 1)))
19 fveq2 6229 . . . 4 (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
2018, 19oveq12d 6708 . . 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 2666 . 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 6229 . . 3 (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁))
23 oveq2 6698 . . . . . 6 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
2423oveq1d 6705 . . . . 5 (𝑥 = 𝑁 → ((2 · 𝑥) + 1) = ((2 · 𝑁) + 1))
2524oveq2d 6706 . . . 4 (𝑥 = 𝑁 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑁) + 1)))
26 fveq2 6229 . . . 4 (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁))
2725, 26oveq12d 6708 . . 3 (𝑥 = 𝑁 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)))
2822, 27eqeq12d 2666 . 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 11445 . . . 4 1 ∈ ℤ
30 seq1 12854 . . . 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 11069 . . . 4 1 ∈ ℕ
33 oveq2 6698 . . . . . . 7 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
3433oveq1d 6705 . . . . . . 7 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
3533, 34oveq12d 6708 . . . . . 6 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 1) / ((2 · 1) − 1)))
3633oveq1d 6705 . . . . . . 7 (𝑘 = 1 → ((2 · 𝑘) + 1) = ((2 · 1) + 1))
3733, 36oveq12d 6708 . . . . . 6 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 1) / ((2 · 1) + 1)))
3835, 37oveq12d 6708 . . . . 5 (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))))
39 eqid 2651 . . . . 5 (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
40 ovex 6718 . . . . 5 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) ∈ V
4138, 39, 40fvmpt 6321 . . . 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 11214 . . . . . . 7 (2 · 1) = 2
4443oveq1i 6700 . . . . . . . 8 ((2 · 1) − 1) = (2 − 1)
45 2m1e1 11173 . . . . . . . 8 (2 − 1) = 1
4644, 45eqtri 2673 . . . . . . 7 ((2 · 1) − 1) = 1
4743, 46oveq12i 6702 . . . . . 6 ((2 · 1) / ((2 · 1) − 1)) = (2 / 1)
4843oveq1i 6700 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
49 2p1e3 11189 . . . . . . . 8 (2 + 1) = 3
5048, 49eqtri 2673 . . . . . . 7 ((2 · 1) + 1) = 3
5143, 50oveq12i 6702 . . . . . 6 ((2 · 1) / ((2 · 1) + 1)) = (2 / 3)
5247, 51oveq12i 6702 . . . . 5 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = ((2 / 1) · (2 / 3))
53 2cn 11129 . . . . . 6 2 ∈ ℂ
54 ax-1cn 10032 . . . . . 6 1 ∈ ℂ
55 3cn 11133 . . . . . 6 3 ∈ ℂ
56 ax-1ne0 10043 . . . . . 6 1 ≠ 0
57 3ne0 11153 . . . . . 6 3 ≠ 0
5853, 54, 53, 55, 56, 57divmuldivi 10823 . . . . 5 ((2 / 1) · (2 / 3)) = ((2 · 2) / (1 · 3))
59 2t2e4 11215 . . . . . 6 (2 · 2) = 4
6055mulid2i 10081 . . . . . 6 (1 · 3) = 3
6159, 60oveq12i 6702 . . . . 5 ((2 · 2) / (1 · 3)) = (4 / 3)
6252, 58, 613eqtri 2677 . . . 4 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = (4 / 3)
63 4cn 11136 . . . . 5 4 ∈ ℂ
64 divrec2 10740 . . . . 5 ((4 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (4 / 3) = ((1 / 3) · 4))
6563, 55, 57, 64mp3an 1464 . . . 4 (4 / 3) = ((1 / 3) · 4)
6650eqcomi 2660 . . . . . 6 3 = ((2 · 1) + 1)
6766oveq2i 6701 . . . . 5 (1 / 3) = (1 / ((2 · 1) + 1))
68 seq1 12854 . . . . . . . 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 6705 . . . . . . . . . 10 (𝑘 = 1 → ((2 · 𝑘)↑4) = ((2 · 1)↑4))
7133, 34oveq12d 6708 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 1) · ((2 · 1) − 1)))
7271oveq1d 6705 . . . . . . . . . 10 (𝑘 = 1 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 1) · ((2 · 1) − 1))↑2))
7370, 72oveq12d 6708 . . . . . . . . 9 (𝑘 = 1 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
74 eqid 2651 . . . . . . . . 9 (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))
75 ovex 6718 . . . . . . . . 9 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) ∈ V
7673, 74, 75fvmpt 6321 . . . . . . . 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 6700 . . . . . . . . 9 ((2 · 1)↑4) = (2↑4)
7943, 46oveq12i 6702 . . . . . . . . . . 11 ((2 · 1) · ((2 · 1) − 1)) = (2 · 1)
8079, 43eqtri 2673 . . . . . . . . . 10 ((2 · 1) · ((2 · 1) − 1)) = 2
8180oveq1i 6700 . . . . . . . . 9 (((2 · 1) · ((2 · 1) − 1))↑2) = (2↑2)
8278, 81oveq12i 6702 . . . . . . . 8 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = ((2↑4) / (2↑2))
83 2exp4 15841 . . . . . . . . . 10 (2↑4) = 16
84 sq2 13000 . . . . . . . . . 10 (2↑2) = 4
8583, 84oveq12i 6702 . . . . . . . . 9 ((2↑4) / (2↑2)) = (16 / 4)
86 4t4e16 11671 . . . . . . . . . . 11 (4 · 4) = 16
8786eqcomi 2660 . . . . . . . . . 10 16 = (4 · 4)
8887oveq1i 6700 . . . . . . . . 9 (16 / 4) = ((4 · 4) / 4)
89 4ne0 11155 . . . . . . . . . 10 4 ≠ 0
9063, 63, 89divcan3i 10809 . . . . . . . . 9 ((4 · 4) / 4) = 4
9185, 88, 903eqtri 2677 . . . . . . . 8 ((2↑4) / (2↑2)) = 4
9282, 91eqtri 2673 . . . . . . 7 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = 4
9369, 77, 923eqtri 2677 . . . . . 6 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = 4
9493eqcomi 2660 . . . . 5 4 = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1)
9567, 94oveq12i 6702 . . . 4 ((1 / 3) · 4) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
9662, 65, 953eqtri 2677 . . 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 2677 . 2 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
98 elnnuz 11762 . . . . . . 7 (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ‘1))
9998biimpi 206 . . . . . 6 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘1))
10099adantr 480 . . . . 5 ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → 𝑦 ∈ (ℤ‘1))
101 seqp1 12856 . . . . 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 476 . . . . 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 6705 . . . 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 2652 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))
106 oveq2 6698 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
107106oveq1d 6705 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
108106, 107oveq12d 6708 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
109106oveq1d 6705 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
110106, 109oveq12d 6708 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
111108, 110oveq12d 6708 . . . . . . . . . 10 (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
112111adantl 481 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
113 peano2nn 11070 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
114 2rp 11875 . . . . . . . . . . . . 13 2 ∈ ℝ+
115114a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ∈ ℝ+)
116 nnre 11065 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
117 nnnn0 11337 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
118117nn0ge0d 11392 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ 𝑦)
119116, 118ge0p1rpd 11940 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ+)
120115, 119rpmulcld 11926 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ+)
121 2re 11128 . . . . . . . . . . . . . . 15 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℝ)
123 1red 10093 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ∈ ℝ)
124116, 123readdcld 10107 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
125122, 124remulcld 10108 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
126125, 123resubcld 10496 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
127 1lt2 11232 . . . . . . . . . . . . . . 15 1 < 2
128127a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 < 2)
129 nnrp 11880 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
130123, 129ltaddrp2d 11944 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
131122, 124, 128, 130mulgt1d 10998 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
132123, 125posdifd 10652 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 < (2 · (𝑦 + 1)) ↔ 0 < ((2 · (𝑦 + 1)) − 1)))
133131, 132mpbid 222 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 0 < ((2 · (𝑦 + 1)) − 1))
134126, 133elrpd 11907 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ+)
135120, 134rpdivcld 11927 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ+)
136115rpge0d 11914 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ 2)
137 0le1 10589 . . . . . . . . . . . . . . 15 0 ≤ 1
138137a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ 1)
139116, 123, 118, 138addge0d 10641 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ (𝑦 + 1))
140122, 124, 136, 139mulge0d 10642 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 0 ≤ (2 · (𝑦 + 1)))
141125, 140ge0p1rpd 11940 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ+)
142120, 141rpdivcld 11927 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ+)
143135, 142rpmulcld 11926 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ+)
144105, 112, 113, 143fvmptd 6327 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
145144oveq2d 6706 . . . . . . 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 10106 . . . . . . . . . 10 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
147126recnd 10106 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℂ)
148141rpcnd 11912 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℂ)
149133gt0ne0d 10630 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
150141rpne0d 11915 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
151146, 147, 146, 148, 149, 150divmuldivd 10880 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
152146, 146mulcld 10098 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
153152, 147, 148, 149, 150divdiv1d 10870 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
154146sqvald 13045 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))
155154eqcomd 2657 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) = ((2 · (𝑦 + 1))↑2))
156155oveq1d 6705 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) = (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))
157156oveq1d 6705 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
158151, 153, 1573eqtr2d 2691 . . . . . . . 8 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
159158oveq2d 6706 . . . . . . 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 13046 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ∈ ℂ)
161160, 147, 149divcld 10839 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
162161, 148, 150divrec2d 10843 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))))
163162oveq2d 6706 . . . . . . . 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 11131 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ∈ ℂ)
165 nncn 11066 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
166164, 165mulcld 10098 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
167 1cnd 10094 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 1 ∈ ℂ)
168166, 167addcld 10097 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
169 2nn 11223 . . . . . . . . . . . . . . 15 2 ∈ ℕ
170169a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℕ)
171 id 22 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ)
172170, 171nnmulcld 11106 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ)
173172peano2nnd 11075 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℕ)
174173nnne0d 11103 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
175168, 174reccld 10832 . . . . . . . . . 10 (𝑦 ∈ ℕ → (1 / ((2 · 𝑦) + 1)) ∈ ℂ)
176 eqidd 2652 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
177 oveq2 6698 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
178177oveq1d 6705 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → ((2 · 𝑘)↑4) = ((2 · 𝑥)↑4))
179177oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → ((2 · 𝑘) − 1) = ((2 · 𝑥) − 1))
180177, 179oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 𝑥) · ((2 · 𝑥) − 1)))
181180oveq1d 6705 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2))
182178, 181oveq12d 6708 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
183182adantl 481 . . . . . . . . . . . . 13 (((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) ∧ 𝑘 = 𝑥) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
184 elfznn 12408 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...𝑦) → 𝑥 ∈ ℕ)
185184adantl 481 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → 𝑥 ∈ ℕ)
186169a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ∈ ℕ)
187 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
188186, 187nnmulcld 11106 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℕ)
189 4nn0 11349 . . . . . . . . . . . . . . . . . . 19 4 ∈ ℕ0
190189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → 4 ∈ ℕ0)
191188, 190nnexpcld 13070 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℕ)
192191nncnd 11074 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℂ)
193 2cnd 11131 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ∈ ℂ)
194 nncn 11066 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ∈ ℂ)
195193, 194mulcld 10098 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℂ)
196 1cnd 10094 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 1 ∈ ℂ)
197195, 196subcld 10430 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ∈ ℂ)
198195, 197mulcld 10098 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ∈ ℂ)
199198sqcld 13046 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ∈ ℂ)
200186nnne0d 11103 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ≠ 0)
201 nnne0 11091 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ≠ 0)
202193, 194, 200, 201mulne0d 10717 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 0)
203 1red 10093 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℕ → 1 ∈ ℝ)
204121a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 2 ∈ ℝ)
205204, 203remulcld 10108 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 1) ∈ ℝ)
206 nnre 11065 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
207204, 206remulcld 10108 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℝ)
20843a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → (2 · 1) = 2)
209127, 208syl5breqr 4723 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → 1 < (2 · 1))
210 0le2 11149 . . . . . . . . . . . . . . . . . . . . . . 23 0 ≤ 2
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 0 ≤ 2)
212 nnge1 11084 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 1 ≤ 𝑥)
213203, 206, 204, 211, 212lemul2ad 11002 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 1) ≤ (2 · 𝑥))
214203, 205, 207, 209, 213ltletrd 10235 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℕ → 1 < (2 · 𝑥))
215203, 214gtned 10210 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 1)
216195, 196, 215subne0d 10439 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ≠ 0)
217195, 197, 202, 216mulne0d 10717 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ≠ 0)
218 2z 11447 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
219218a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → 2 ∈ ℤ)
220198, 217, 219expne0d 13054 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ≠ 0)
221192, 199, 220divcld 10839 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
222184, 221syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...𝑦) → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
223222adantl 481 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
224176, 183, 185, 223fvmptd 6327 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
225224, 223eqeltrd 2730 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) ∈ ℂ)
226 mulcl 10058 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑥 · 𝑤) ∈ ℂ)
227226adantl 481 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑥 · 𝑤) ∈ ℂ)
22899, 225, 227seqcl 12861 . . . . . . . . . 10 (𝑦 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) ∈ ℂ)
229175, 228mulcld 10098 . . . . . . . . 9 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) ∈ ℂ)
230148, 150reccld 10832 . . . . . . . . 9 (𝑦 ∈ ℕ → (1 / ((2 · (𝑦 + 1)) + 1)) ∈ ℂ)
231229, 230, 161mul12d 10283 . . . . . . . 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 10099 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (1 / ((2 · 𝑦) + 1))))
233232oveq1d 6705 . . . . . . . . . 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 10101 . . . . . . . . . 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 10880 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))))
236160mulid2d 10096 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 · ((2 · (𝑦 + 1))↑2)) = ((2 · (𝑦 + 1))↑2))
237164, 165, 167adddid 10102 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
23843a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → (2 · 1) = 2)
239238oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
240237, 239eqtrd 2685 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
241240oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
242166, 164, 167addsubassd 10450 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
24345a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 − 1) = 1)
244243oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
245241, 242, 2443eqtrd 2689 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
246245oveq2d 6706 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
247168sqvald 13045 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
248246, 247eqtr4d 2688 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1)↑2))
249236, 248oveq12d 6708 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)))
250 2p2e4 11182 . . . . . . . . . . . . . . . . . 18 (2 + 2) = 4
25153, 53, 250mvlladdi 10337 . . . . . . . . . . . . . . . . 17 2 = (4 − 2)
252251a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 = (4 − 2))
253252oveq2d 6706 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1))↑(4 − 2)))
254120rpne0d 11915 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
255218a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ∈ ℤ)
256 4z 11449 . . . . . . . . . . . . . . . . 17 4 ∈ ℤ
257256a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 4 ∈ ℤ)
258146, 254, 255, 257expsubd 13059 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑(4 − 2)) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
259253, 258eqtrd 2685 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
260245eqcomd 2657 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) = ((2 · (𝑦 + 1)) − 1))
261260oveq1d 6705 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · (𝑦 + 1)) − 1)↑2))
262259, 261oveq12d 6708 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)))
263146, 254, 257expclzd 13053 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑4) ∈ ℂ)
264147sqcld 13046 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ∈ ℂ)
265165, 167addcld 10097 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
266170nnne0d 11103 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ≠ 0)
267113nnne0d 11103 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
268164, 265, 266, 267mulne0d 10717 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
269146, 268, 255expne0d 13054 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ≠ 0)
270147, 149, 255expne0d 13054 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ≠ 0)
271263, 160, 264, 269, 270divdiv1d 10870 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))))
272146, 147sqmuld 13060 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) = (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)))
273272eqcomd 2657 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
274273oveq2d 6706 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
275262, 271, 2743eqtrd 2689 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
276235, 249, 2753eqtrd 2689 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
277276oveq2d 6706 . . . . . . . . . 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 2689 . . . . . . . . 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 6706 . . . . . . . 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 2689 . . . . . . 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 2689 . . . . . 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 2652 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
283 simpr 476 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → 𝑘 = (𝑦 + 1))
284283oveq2d 6706 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (2 · 𝑘) = (2 · (𝑦 + 1)))
285284oveq1d 6705 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘)↑4) = ((2 · (𝑦 + 1))↑4))
286284oveq1d 6705 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
287284, 286oveq12d 6708 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))
288287oveq1d 6705 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
289285, 288oveq12d 6708 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
290146, 147mulcld 10098 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
291290sqcld 13046 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ∈ ℂ)
292146, 147, 254, 149mulne0d 10717 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ≠ 0)
293290, 292, 255expne0d 13054 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ≠ 0)
294263, 291, 293divcld 10839 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) ∈ ℂ)
295282, 289, 113, 294fvmptd 6327 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
296295eqcomd 2657 . . . . . . . 8 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))
297296oveq2d 6706 . . . . . . 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 6706 . . . . . 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 12856 . . . . . . . . 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 2657 . . . . . . 7 (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
302301oveq2d 6706 . . . . . 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 2689 . . . . 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 480 . . . 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 2689 . . 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 449 . 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 11076 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 383   = wceq 1523  wcel 2030  wne 2823   class class class wbr 4685  cmpt 4762  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  2c2 11108  3c3 11109  4c4 11110  6c6 11112  0cn0 11330  cz 11415  cdc 11531  cuz 11725  +crp 11870  ...cfz 12364  seqcseq 12841  cexp 12900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-rp 11871  df-fz 12365  df-seq 12842  df-exp 12901
This theorem is referenced by:  wallispi2  40608
  Copyright terms: Public domain W3C validator