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 39582
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 6150 . . 3 (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1))
2 oveq2 6613 . . . . . 6 (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
32oveq1d 6620 . . . . 5 (𝑥 = 1 → ((2 · 𝑥) + 1) = ((2 · 1) + 1))
43oveq2d 6621 . . . 4 (𝑥 = 1 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 1) + 1)))
5 fveq2 6150 . . . 4 (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
64, 5oveq12d 6623 . . 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 2641 . 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 6150 . . 3 (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦))
9 oveq2 6613 . . . . . 6 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
109oveq1d 6620 . . . . 5 (𝑥 = 𝑦 → ((2 · 𝑥) + 1) = ((2 · 𝑦) + 1))
1110oveq2d 6621 . . . 4 (𝑥 = 𝑦 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑦) + 1)))
12 fveq2 6150 . . . 4 (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))
1311, 12oveq12d 6623 . . 3 (𝑥 = 𝑦 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)))
148, 13eqeq12d 2641 . 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 6150 . . 3 (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)))
16 oveq2 6613 . . . . . 6 (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
1716oveq1d 6620 . . . . 5 (𝑥 = (𝑦 + 1) → ((2 · 𝑥) + 1) = ((2 · (𝑦 + 1)) + 1))
1817oveq2d 6621 . . . 4 (𝑥 = (𝑦 + 1) → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · (𝑦 + 1)) + 1)))
19 fveq2 6150 . . . 4 (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
2018, 19oveq12d 6623 . . 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 2641 . 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 6150 . . 3 (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁))
23 oveq2 6613 . . . . . 6 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
2423oveq1d 6620 . . . . 5 (𝑥 = 𝑁 → ((2 · 𝑥) + 1) = ((2 · 𝑁) + 1))
2524oveq2d 6621 . . . 4 (𝑥 = 𝑁 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑁) + 1)))
26 fveq2 6150 . . . 4 (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁))
2725, 26oveq12d 6623 . . 3 (𝑥 = 𝑁 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)))
2822, 27eqeq12d 2641 . 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 11352 . . . 4 1 ∈ ℤ
30 seq1 12751 . . . 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 10976 . . . 4 1 ∈ ℕ
33 oveq2 6613 . . . . . . 7 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
3433oveq1d 6620 . . . . . . 7 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
3533, 34oveq12d 6623 . . . . . 6 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 1) / ((2 · 1) − 1)))
3633oveq1d 6620 . . . . . . 7 (𝑘 = 1 → ((2 · 𝑘) + 1) = ((2 · 1) + 1))
3733, 36oveq12d 6623 . . . . . 6 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 1) / ((2 · 1) + 1)))
3835, 37oveq12d 6623 . . . . 5 (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))))
39 eqid 2626 . . . . 5 (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
40 ovex 6633 . . . . 5 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) ∈ V
4138, 39, 40fvmpt 6240 . . . 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 11121 . . . . . . 7 (2 · 1) = 2
4443oveq1i 6615 . . . . . . . 8 ((2 · 1) − 1) = (2 − 1)
45 2m1e1 11080 . . . . . . . 8 (2 − 1) = 1
4644, 45eqtri 2648 . . . . . . 7 ((2 · 1) − 1) = 1
4743, 46oveq12i 6617 . . . . . 6 ((2 · 1) / ((2 · 1) − 1)) = (2 / 1)
4843oveq1i 6615 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
49 2p1e3 11096 . . . . . . . 8 (2 + 1) = 3
5048, 49eqtri 2648 . . . . . . 7 ((2 · 1) + 1) = 3
5143, 50oveq12i 6617 . . . . . 6 ((2 · 1) / ((2 · 1) + 1)) = (2 / 3)
5247, 51oveq12i 6617 . . . . 5 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = ((2 / 1) · (2 / 3))
53 2cn 11036 . . . . . 6 2 ∈ ℂ
54 ax-1cn 9939 . . . . . 6 1 ∈ ℂ
55 3cn 11040 . . . . . 6 3 ∈ ℂ
56 ax-1ne0 9950 . . . . . 6 1 ≠ 0
57 3ne0 11060 . . . . . 6 3 ≠ 0
5853, 54, 53, 55, 56, 57divmuldivi 10730 . . . . 5 ((2 / 1) · (2 / 3)) = ((2 · 2) / (1 · 3))
59 2t2e4 11122 . . . . . 6 (2 · 2) = 4
6055mulid2i 9988 . . . . . 6 (1 · 3) = 3
6159, 60oveq12i 6617 . . . . 5 ((2 · 2) / (1 · 3)) = (4 / 3)
6252, 58, 613eqtri 2652 . . . 4 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = (4 / 3)
63 4cn 11043 . . . . 5 4 ∈ ℂ
64 divrec2 10647 . . . . 5 ((4 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (4 / 3) = ((1 / 3) · 4))
6563, 55, 57, 64mp3an 1421 . . . 4 (4 / 3) = ((1 / 3) · 4)
6650eqcomi 2635 . . . . . 6 3 = ((2 · 1) + 1)
6766oveq2i 6616 . . . . 5 (1 / 3) = (1 / ((2 · 1) + 1))
68 seq1 12751 . . . . . . . 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 6620 . . . . . . . . . 10 (𝑘 = 1 → ((2 · 𝑘)↑4) = ((2 · 1)↑4))
7133, 34oveq12d 6623 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 1) · ((2 · 1) − 1)))
7271oveq1d 6620 . . . . . . . . . 10 (𝑘 = 1 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 1) · ((2 · 1) − 1))↑2))
7370, 72oveq12d 6623 . . . . . . . . 9 (𝑘 = 1 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
74 eqid 2626 . . . . . . . . 9 (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))
75 ovex 6633 . . . . . . . . 9 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) ∈ V
7673, 74, 75fvmpt 6240 . . . . . . . 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 6615 . . . . . . . . 9 ((2 · 1)↑4) = (2↑4)
7943, 46oveq12i 6617 . . . . . . . . . . 11 ((2 · 1) · ((2 · 1) − 1)) = (2 · 1)
8079, 43eqtri 2648 . . . . . . . . . 10 ((2 · 1) · ((2 · 1) − 1)) = 2
8180oveq1i 6615 . . . . . . . . 9 (((2 · 1) · ((2 · 1) − 1))↑2) = (2↑2)
8278, 81oveq12i 6617 . . . . . . . 8 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = ((2↑4) / (2↑2))
83 2exp4 15713 . . . . . . . . . 10 (2↑4) = 16
84 sq2 12897 . . . . . . . . . 10 (2↑2) = 4
8583, 84oveq12i 6617 . . . . . . . . 9 ((2↑4) / (2↑2)) = (16 / 4)
86 4t4e16 11577 . . . . . . . . . . 11 (4 · 4) = 16
8786eqcomi 2635 . . . . . . . . . 10 16 = (4 · 4)
8887oveq1i 6615 . . . . . . . . 9 (16 / 4) = ((4 · 4) / 4)
89 4ne0 11062 . . . . . . . . . 10 4 ≠ 0
9063, 63, 89divcan3i 10716 . . . . . . . . 9 ((4 · 4) / 4) = 4
9185, 88, 903eqtri 2652 . . . . . . . 8 ((2↑4) / (2↑2)) = 4
9282, 91eqtri 2648 . . . . . . 7 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = 4
9369, 77, 923eqtri 2652 . . . . . 6 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = 4
9493eqcomi 2635 . . . . 5 4 = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1)
9567, 94oveq12i 6617 . . . 4 ((1 / 3) · 4) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
9662, 65, 953eqtri 2652 . . 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 2652 . 2 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
98 elnnuz 11668 . . . . . . 7 (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ‘1))
9998biimpi 206 . . . . . 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 12753 . . . . 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 477 . . . . 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 6620 . . . 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 2627 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))
106 oveq2 6613 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
107106oveq1d 6620 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
108106, 107oveq12d 6623 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
109106oveq1d 6620 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
110106, 109oveq12d 6623 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
111108, 110oveq12d 6623 . . . . . . . . . 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 10977 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
114 2rp 11781 . . . . . . . . . . . . 13 2 ∈ ℝ+
115114a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ∈ ℝ+)
116 nnre 10972 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
117 nnnn0 11244 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
118117nn0ge0d 11299 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ 𝑦)
119116, 118ge0p1rpd 11846 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ+)
120115, 119rpmulcld 11832 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ+)
121 2re 11035 . . . . . . . . . . . . . . 15 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℝ)
123 1red 10000 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ∈ ℝ)
124116, 123readdcld 10014 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
125122, 124remulcld 10015 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
126125, 123resubcld 10403 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
127 1lt2 11139 . . . . . . . . . . . . . . 15 1 < 2
128127a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 < 2)
129 nnrp 11786 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
130123, 129ltaddrp2d 11850 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
131122, 124, 128, 130mulgt1d 10905 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
132123, 125posdifd 10559 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 < (2 · (𝑦 + 1)) ↔ 0 < ((2 · (𝑦 + 1)) − 1)))
133131, 132mpbid 222 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 0 < ((2 · (𝑦 + 1)) − 1))
134126, 133elrpd 11813 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ+)
135120, 134rpdivcld 11833 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ+)
136115rpge0d 11820 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ 2)
137 0le1 10496 . . . . . . . . . . . . . . 15 0 ≤ 1
138137a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ 1)
139116, 123, 118, 138addge0d 10548 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ (𝑦 + 1))
140122, 124, 136, 139mulge0d 10549 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 0 ≤ (2 · (𝑦 + 1)))
141125, 140ge0p1rpd 11846 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ+)
142120, 141rpdivcld 11833 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ+)
143135, 142rpmulcld 11832 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ+)
144105, 112, 113, 143fvmptd 6246 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
145144oveq2d 6621 . . . . . . 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 10013 . . . . . . . . . 10 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
147126recnd 10013 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℂ)
148141rpcnd 11818 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℂ)
149133gt0ne0d 10537 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
150141rpne0d 11821 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
151146, 147, 146, 148, 149, 150divmuldivd 10787 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
152146, 146mulcld 10005 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
153152, 147, 148, 149, 150divdiv1d 10777 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
154146sqvald 12942 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))
155154eqcomd 2632 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) = ((2 · (𝑦 + 1))↑2))
156155oveq1d 6620 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) = (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))
157156oveq1d 6620 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
158151, 153, 1573eqtr2d 2666 . . . . . . . 8 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
159158oveq2d 6621 . . . . . . 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 12943 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ∈ ℂ)
161160, 147, 149divcld 10746 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
162161, 148, 150divrec2d 10750 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))))
163162oveq2d 6621 . . . . . . . 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 11038 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ∈ ℂ)
165 nncn 10973 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
166164, 165mulcld 10005 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
167 1cnd 10001 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 1 ∈ ℂ)
168166, 167addcld 10004 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
169 2nn 11130 . . . . . . . . . . . . . . 15 2 ∈ ℕ
170169a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℕ)
171 id 22 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ)
172170, 171nnmulcld 11013 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ)
173172peano2nnd 10982 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℕ)
174173nnne0d 11010 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
175168, 174reccld 10739 . . . . . . . . . 10 (𝑦 ∈ ℕ → (1 / ((2 · 𝑦) + 1)) ∈ ℂ)
176 eqidd 2627 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
177 oveq2 6613 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
178177oveq1d 6620 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → ((2 · 𝑘)↑4) = ((2 · 𝑥)↑4))
179177oveq1d 6620 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → ((2 · 𝑘) − 1) = ((2 · 𝑥) − 1))
180177, 179oveq12d 6623 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 𝑥) · ((2 · 𝑥) − 1)))
181180oveq1d 6620 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2))
182178, 181oveq12d 6623 . . . . . . . . . . . . . 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 12309 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...𝑦) → 𝑥 ∈ ℕ)
185184adantl 482 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → 𝑥 ∈ ℕ)
186169a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ∈ ℕ)
187 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
188186, 187nnmulcld 11013 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℕ)
189 4nn0 11256 . . . . . . . . . . . . . . . . . . 19 4 ∈ ℕ0
190189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → 4 ∈ ℕ0)
191188, 190nnexpcld 12967 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℕ)
192191nncnd 10981 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℂ)
193 2cnd 11038 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ∈ ℂ)
194 nncn 10973 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ∈ ℂ)
195193, 194mulcld 10005 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℂ)
196 1cnd 10001 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 1 ∈ ℂ)
197195, 196subcld 10337 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ∈ ℂ)
198195, 197mulcld 10005 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ∈ ℂ)
199198sqcld 12943 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ∈ ℂ)
200186nnne0d 11010 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ≠ 0)
201 nnne0 10998 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ≠ 0)
202193, 194, 200, 201mulne0d 10624 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 0)
203 1red 10000 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℕ → 1 ∈ ℝ)
204121a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 2 ∈ ℝ)
205204, 203remulcld 10015 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 1) ∈ ℝ)
206 nnre 10972 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
207204, 206remulcld 10015 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℝ)
20843a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → (2 · 1) = 2)
209127, 208syl5breqr 4656 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → 1 < (2 · 1))
210 0le2 11056 . . . . . . . . . . . . . . . . . . . . . . 23 0 ≤ 2
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 0 ≤ 2)
212 nnge1 10991 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 1 ≤ 𝑥)
213203, 206, 204, 211, 212lemul2ad 10909 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 1) ≤ (2 · 𝑥))
214203, 205, 207, 209, 213ltletrd 10142 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℕ → 1 < (2 · 𝑥))
215203, 214gtned 10117 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 1)
216195, 196, 215subne0d 10346 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ≠ 0)
217195, 197, 202, 216mulne0d 10624 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ≠ 0)
218 2z 11354 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
219218a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → 2 ∈ ℤ)
220198, 217, 219expne0d 12951 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ≠ 0)
221192, 199, 220divcld 10746 . . . . . . . . . . . . . . 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 6246 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
225224, 223eqeltrd 2704 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) ∈ ℂ)
226 mulcl 9965 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑥 · 𝑤) ∈ ℂ)
227226adantl 482 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑥 · 𝑤) ∈ ℂ)
22899, 225, 227seqcl 12758 . . . . . . . . . 10 (𝑦 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) ∈ ℂ)
229175, 228mulcld 10005 . . . . . . . . 9 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) ∈ ℂ)
230148, 150reccld 10739 . . . . . . . . 9 (𝑦 ∈ ℕ → (1 / ((2 · (𝑦 + 1)) + 1)) ∈ ℂ)
231229, 230, 161mul12d 10190 . . . . . . . 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 10006 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (1 / ((2 · 𝑦) + 1))))
233232oveq1d 6620 . . . . . . . . . 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 10008 . . . . . . . . . 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 10787 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))))
236160mulid2d 10003 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 · ((2 · (𝑦 + 1))↑2)) = ((2 · (𝑦 + 1))↑2))
237164, 165, 167adddid 10009 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
23843a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → (2 · 1) = 2)
239238oveq2d 6621 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
240237, 239eqtrd 2660 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
241240oveq1d 6620 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
242166, 164, 167addsubassd 10357 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
24345a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 − 1) = 1)
244243oveq2d 6621 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
245241, 242, 2443eqtrd 2664 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
246245oveq2d 6621 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
247168sqvald 12942 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
248246, 247eqtr4d 2663 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1)↑2))
249236, 248oveq12d 6623 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)))
250 2p2e4 11089 . . . . . . . . . . . . . . . . . 18 (2 + 2) = 4
25153, 53, 250mvlladdi 10244 . . . . . . . . . . . . . . . . 17 2 = (4 − 2)
252251a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 = (4 − 2))
253252oveq2d 6621 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1))↑(4 − 2)))
254120rpne0d 11821 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
255218a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ∈ ℤ)
256 4z 11356 . . . . . . . . . . . . . . . . 17 4 ∈ ℤ
257256a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 4 ∈ ℤ)
258146, 254, 255, 257expsubd 12956 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑(4 − 2)) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
259253, 258eqtrd 2660 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
260245eqcomd 2632 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) = ((2 · (𝑦 + 1)) − 1))
261260oveq1d 6620 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · (𝑦 + 1)) − 1)↑2))
262259, 261oveq12d 6623 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)))
263146, 254, 257expclzd 12950 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑4) ∈ ℂ)
264147sqcld 12943 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ∈ ℂ)
265165, 167addcld 10004 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
266170nnne0d 11010 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ≠ 0)
267113nnne0d 11010 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
268164, 265, 266, 267mulne0d 10624 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
269146, 268, 255expne0d 12951 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ≠ 0)
270147, 149, 255expne0d 12951 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ≠ 0)
271263, 160, 264, 269, 270divdiv1d 10777 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))))
272146, 147sqmuld 12957 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) = (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)))
273272eqcomd 2632 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
274273oveq2d 6621 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
275262, 271, 2743eqtrd 2664 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
276235, 249, 2753eqtrd 2664 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
277276oveq2d 6621 . . . . . . . . . 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 2664 . . . . . . . . 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 6621 . . . . . . . 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 2664 . . . . . . 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 2664 . . . . . 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 2627 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
283 simpr 477 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → 𝑘 = (𝑦 + 1))
284283oveq2d 6621 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (2 · 𝑘) = (2 · (𝑦 + 1)))
285284oveq1d 6620 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘)↑4) = ((2 · (𝑦 + 1))↑4))
286284oveq1d 6620 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
287284, 286oveq12d 6623 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))
288287oveq1d 6620 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
289285, 288oveq12d 6623 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
290146, 147mulcld 10005 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
291290sqcld 12943 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ∈ ℂ)
292146, 147, 254, 149mulne0d 10624 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ≠ 0)
293290, 292, 255expne0d 12951 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ≠ 0)
294263, 291, 293divcld 10746 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) ∈ ℂ)
295282, 289, 113, 294fvmptd 6246 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
296295eqcomd 2632 . . . . . . . 8 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))
297296oveq2d 6621 . . . . . . 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 6621 . . . . . 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 12753 . . . . . . . . 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 2632 . . . . . . 7 (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
302301oveq2d 6621 . . . . . 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 2664 . . . . 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 2664 . . 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 450 . 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 10983 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 384   = wceq 1480  wcel 1992  wne 2796   class class class wbr 4618  cmpt 4678  cfv 5850  (class class class)co 6605  cc 9879  cr 9880  0cc0 9881  1c1 9882   + caddc 9884   · cmul 9886   < clt 10019  cle 10020  cmin 10211   / cdiv 10629  cn 10965  2c2 11015  3c3 11016  4c4 11017  6c6 11019  0cn0 11237  cz 11322  cdc 11437  cuz 11631  +crp 11776  ...cfz 12265  seqcseq 12738  cexp 12797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-3 11025  df-4 11026  df-5 11027  df-6 11028  df-7 11029  df-8 11030  df-9 11031  df-n0 11238  df-z 11323  df-dec 11438  df-uz 11632  df-rp 11777  df-fz 12266  df-seq 12739  df-exp 12798
This theorem is referenced by:  wallispi2  39584
  Copyright terms: Public domain W3C validator