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 40768
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 6411 . . 3 (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1))
2 oveq2 6885 . . . . . 6 (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
32oveq1d 6892 . . . . 5 (𝑥 = 1 → ((2 · 𝑥) + 1) = ((2 · 1) + 1))
43oveq2d 6893 . . . 4 (𝑥 = 1 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 1) + 1)))
5 fveq2 6411 . . . 4 (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
64, 5oveq12d 6895 . . 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 2828 . 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 6411 . . 3 (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦))
9 oveq2 6885 . . . . . 6 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
109oveq1d 6892 . . . . 5 (𝑥 = 𝑦 → ((2 · 𝑥) + 1) = ((2 · 𝑦) + 1))
1110oveq2d 6893 . . . 4 (𝑥 = 𝑦 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑦) + 1)))
12 fveq2 6411 . . . 4 (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))
1311, 12oveq12d 6895 . . 3 (𝑥 = 𝑦 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)))
148, 13eqeq12d 2828 . 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 6411 . . 3 (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)))
16 oveq2 6885 . . . . . 6 (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
1716oveq1d 6892 . . . . 5 (𝑥 = (𝑦 + 1) → ((2 · 𝑥) + 1) = ((2 · (𝑦 + 1)) + 1))
1817oveq2d 6893 . . . 4 (𝑥 = (𝑦 + 1) → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · (𝑦 + 1)) + 1)))
19 fveq2 6411 . . . 4 (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
2018, 19oveq12d 6895 . . 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 2828 . 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 6411 . . 3 (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁))
23 oveq2 6885 . . . . . 6 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
2423oveq1d 6892 . . . . 5 (𝑥 = 𝑁 → ((2 · 𝑥) + 1) = ((2 · 𝑁) + 1))
2524oveq2d 6893 . . . 4 (𝑥 = 𝑁 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑁) + 1)))
26 fveq2 6411 . . . 4 (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁))
2725, 26oveq12d 6895 . . 3 (𝑥 = 𝑁 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)))
2822, 27eqeq12d 2828 . 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 11676 . . . 4 1 ∈ ℤ
30 seq1 13040 . . . 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 11319 . . . 4 1 ∈ ℕ
33 oveq2 6885 . . . . . . 7 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
3433oveq1d 6892 . . . . . . 7 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
3533, 34oveq12d 6895 . . . . . 6 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 1) / ((2 · 1) − 1)))
3633oveq1d 6892 . . . . . . 7 (𝑘 = 1 → ((2 · 𝑘) + 1) = ((2 · 1) + 1))
3733, 36oveq12d 6895 . . . . . 6 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 1) / ((2 · 1) + 1)))
3835, 37oveq12d 6895 . . . . 5 (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))))
39 eqid 2813 . . . . 5 (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
40 ovex 6909 . . . . 5 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) ∈ V
4138, 39, 40fvmpt 6506 . . . 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 11457 . . . . . . 7 (2 · 1) = 2
4443oveq1i 6887 . . . . . . . 8 ((2 · 1) − 1) = (2 − 1)
45 2m1e1 11421 . . . . . . . 8 (2 − 1) = 1
4644, 45eqtri 2835 . . . . . . 7 ((2 · 1) − 1) = 1
4743, 46oveq12i 6889 . . . . . 6 ((2 · 1) / ((2 · 1) − 1)) = (2 / 1)
4843oveq1i 6887 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
49 2p1e3 11437 . . . . . . . 8 (2 + 1) = 3
5048, 49eqtri 2835 . . . . . . 7 ((2 · 1) + 1) = 3
5143, 50oveq12i 6889 . . . . . 6 ((2 · 1) / ((2 · 1) + 1)) = (2 / 3)
5247, 51oveq12i 6889 . . . . 5 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = ((2 / 1) · (2 / 3))
53 2cn 11378 . . . . . 6 2 ∈ ℂ
54 ax-1cn 10282 . . . . . 6 1 ∈ ℂ
55 3cn 11382 . . . . . 6 3 ∈ ℂ
56 ax-1ne0 10293 . . . . . 6 1 ≠ 0
57 3ne0 11401 . . . . . 6 3 ≠ 0
5853, 54, 53, 55, 56, 57divmuldivi 11073 . . . . 5 ((2 / 1) · (2 / 3)) = ((2 · 2) / (1 · 3))
59 2t2e4 11458 . . . . . 6 (2 · 2) = 4
6055mulid2i 10333 . . . . . 6 (1 · 3) = 3
6159, 60oveq12i 6889 . . . . 5 ((2 · 2) / (1 · 3)) = (4 / 3)
6252, 58, 613eqtri 2839 . . . 4 (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = (4 / 3)
63 4cn 11385 . . . . 5 4 ∈ ℂ
64 divrec2 10990 . . . . 5 ((4 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (4 / 3) = ((1 / 3) · 4))
6563, 55, 57, 64mp3an 1578 . . . 4 (4 / 3) = ((1 / 3) · 4)
6650eqcomi 2822 . . . . . 6 3 = ((2 · 1) + 1)
6766oveq2i 6888 . . . . 5 (1 / 3) = (1 / ((2 · 1) + 1))
68 seq1 13040 . . . . . . . 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 6892 . . . . . . . . . 10 (𝑘 = 1 → ((2 · 𝑘)↑4) = ((2 · 1)↑4))
7133, 34oveq12d 6895 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 1) · ((2 · 1) − 1)))
7271oveq1d 6892 . . . . . . . . . 10 (𝑘 = 1 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 1) · ((2 · 1) − 1))↑2))
7370, 72oveq12d 6895 . . . . . . . . 9 (𝑘 = 1 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
74 eqid 2813 . . . . . . . . 9 (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))
75 ovex 6909 . . . . . . . . 9 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) ∈ V
7673, 74, 75fvmpt 6506 . . . . . . . 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 6887 . . . . . . . . 9 ((2 · 1)↑4) = (2↑4)
7943, 46oveq12i 6889 . . . . . . . . . . 11 ((2 · 1) · ((2 · 1) − 1)) = (2 · 1)
8079, 43eqtri 2835 . . . . . . . . . 10 ((2 · 1) · ((2 · 1) − 1)) = 2
8180oveq1i 6887 . . . . . . . . 9 (((2 · 1) · ((2 · 1) − 1))↑2) = (2↑2)
8278, 81oveq12i 6889 . . . . . . . 8 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = ((2↑4) / (2↑2))
83 2exp4 16009 . . . . . . . . . 10 (2↑4) = 16
84 sq2 13186 . . . . . . . . . 10 (2↑2) = 4
8583, 84oveq12i 6889 . . . . . . . . 9 ((2↑4) / (2↑2)) = (16 / 4)
86 4t4e16 11861 . . . . . . . . . . 11 (4 · 4) = 16
8786eqcomi 2822 . . . . . . . . . 10 16 = (4 · 4)
8887oveq1i 6887 . . . . . . . . 9 (16 / 4) = ((4 · 4) / 4)
89 4ne0 11403 . . . . . . . . . 10 4 ≠ 0
9063, 63, 89divcan3i 11059 . . . . . . . . 9 ((4 · 4) / 4) = 4
9185, 88, 903eqtri 2839 . . . . . . . 8 ((2↑4) / (2↑2)) = 4
9282, 91eqtri 2835 . . . . . . 7 (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = 4
9369, 77, 923eqtri 2839 . . . . . 6 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = 4
9493eqcomi 2822 . . . . 5 4 = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1)
9567, 94oveq12i 6889 . . . 4 ((1 / 3) · 4) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
9662, 65, 953eqtri 2839 . . 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 2839 . 2 (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
98 elnnuz 11945 . . . . . . 7 (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ‘1))
9998biimpi 207 . . . . . 6 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘1))
10099adantr 468 . . . . 5 ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → 𝑦 ∈ (ℤ‘1))
101 seqp1 13042 . . . . 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 473 . . . . 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 6892 . . . 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 2814 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))
106 oveq2 6885 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
107106oveq1d 6892 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
108106, 107oveq12d 6895 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
109106oveq1d 6892 . . . . . . . . . . . 12 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
110106, 109oveq12d 6895 . . . . . . . . . . 11 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
111108, 110oveq12d 6895 . . . . . . . . . 10 (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
112111adantl 469 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
113 peano2nn 11320 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
114 2rp 12054 . . . . . . . . . . . . 13 2 ∈ ℝ+
115114a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ∈ ℝ+)
116 nnre 11315 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
117 nnnn0 11569 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
118117nn0ge0d 11623 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ 𝑦)
119116, 118ge0p1rpd 12119 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ+)
120115, 119rpmulcld 12105 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ+)
121 2re 11377 . . . . . . . . . . . . . . 15 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℝ)
123 1red 10329 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ∈ ℝ)
124116, 123readdcld 10357 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
125122, 124remulcld 10358 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
126125, 123resubcld 10746 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
127 1lt2 11473 . . . . . . . . . . . . . . 15 1 < 2
128127a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 < 2)
129 nnrp 12059 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
130123, 129ltaddrp2d 12123 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
131122, 124, 128, 130mulgt1d 11248 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
132123, 125posdifd 10902 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 < (2 · (𝑦 + 1)) ↔ 0 < ((2 · (𝑦 + 1)) − 1)))
133131, 132mpbid 223 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 0 < ((2 · (𝑦 + 1)) − 1))
134126, 133elrpd 12086 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ+)
135120, 134rpdivcld 12106 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ+)
136115rpge0d 12093 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ 2)
137 0le1 10839 . . . . . . . . . . . . . . 15 0 ≤ 1
138137a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ 1)
139116, 123, 118, 138addge0d 10891 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 ≤ (𝑦 + 1))
140122, 124, 136, 139mulge0d 10892 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 0 ≤ (2 · (𝑦 + 1)))
141125, 140ge0p1rpd 12119 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ+)
142120, 141rpdivcld 12106 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ+)
143135, 142rpmulcld 12105 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ+)
144105, 112, 113, 143fvmptd 6512 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
145144oveq2d 6893 . . . . . . 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 10356 . . . . . . . . . 10 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
147126recnd 10356 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℂ)
148141rpcnd 12091 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℂ)
149133gt0ne0d 10880 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
150141rpne0d 12094 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
151146, 147, 146, 148, 149, 150divmuldivd 11130 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
152146, 146mulcld 10348 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
153152, 147, 148, 149, 150divdiv1d 11120 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
154146sqvald 13231 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))
155154eqcomd 2819 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) = ((2 · (𝑦 + 1))↑2))
156155oveq1d 6892 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) = (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))
157156oveq1d 6892 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
158151, 153, 1573eqtr2d 2853 . . . . . . . 8 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
159158oveq2d 6893 . . . . . . 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 13232 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ∈ ℂ)
161160, 147, 149divcld 11089 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
162161, 148, 150divrec2d 11093 . . . . . . . . 9 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))))
163162oveq2d 6893 . . . . . . . 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 11380 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ∈ ℂ)
165 nncn 11316 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
166164, 165mulcld 10348 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
167 1cnd 10323 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 1 ∈ ℂ)
168166, 167addcld 10347 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
169 2nn 11465 . . . . . . . . . . . . . . 15 2 ∈ ℕ
170169a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℕ)
171 id 22 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ)
172170, 171nnmulcld 11357 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ)
173172peano2nnd 11325 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℕ)
174173nnne0d 11354 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
175168, 174reccld 11082 . . . . . . . . . 10 (𝑦 ∈ ℕ → (1 / ((2 · 𝑦) + 1)) ∈ ℂ)
176 eqidd 2814 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
177 oveq2 6885 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
178177oveq1d 6892 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → ((2 · 𝑘)↑4) = ((2 · 𝑥)↑4))
179177oveq1d 6892 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → ((2 · 𝑘) − 1) = ((2 · 𝑥) − 1))
180177, 179oveq12d 6895 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 𝑥) · ((2 · 𝑥) − 1)))
181180oveq1d 6892 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2))
182178, 181oveq12d 6895 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
183182adantl 469 . . . . . . . . . . . . 13 (((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) ∧ 𝑘 = 𝑥) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
184 elfznn 12596 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...𝑦) → 𝑥 ∈ ℕ)
185184adantl 469 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → 𝑥 ∈ ℕ)
186169a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ∈ ℕ)
187 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
188186, 187nnmulcld 11357 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℕ)
189 4nn0 11581 . . . . . . . . . . . . . . . . . . 19 4 ∈ ℕ0
190189a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → 4 ∈ ℕ0)
191188, 190nnexpcld 13256 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℕ)
192191nncnd 11324 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℂ)
193 2cnd 11380 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ∈ ℂ)
194 nncn 11316 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ∈ ℂ)
195193, 194mulcld 10348 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℂ)
196 1cnd 10323 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 1 ∈ ℂ)
197195, 196subcld 10680 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ∈ ℂ)
198195, 197mulcld 10348 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ∈ ℂ)
199198sqcld 13232 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ∈ ℂ)
200186nnne0d 11354 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 2 ≠ 0)
201 nnne0 11342 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → 𝑥 ≠ 0)
202193, 194, 200, 201mulne0d 10967 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 0)
203 1red 10329 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℕ → 1 ∈ ℝ)
204121a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 2 ∈ ℝ)
205204, 203remulcld 10358 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 1) ∈ ℝ)
206 nnre 11315 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
207204, 206remulcld 10358 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℝ)
20843a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → (2 · 1) = 2)
209127, 208syl5breqr 4889 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → 1 < (2 · 1))
210 0le2 11397 . . . . . . . . . . . . . . . . . . . . . . 23 0 ≤ 2
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 0 ≤ 2)
212 nnge1 11335 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 1 ≤ 𝑥)
213203, 206, 204, 211, 212lemul2ad 11252 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℕ → (2 · 1) ≤ (2 · 𝑥))
214203, 205, 207, 209, 213ltletrd 10485 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℕ → 1 < (2 · 𝑥))
215203, 214gtned 10460 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 1)
216195, 196, 215subne0d 10689 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ≠ 0)
217195, 197, 202, 216mulne0d 10967 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ≠ 0)
218 2z 11678 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
219218a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → 2 ∈ ℤ)
220198, 217, 219expne0d 13240 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ≠ 0)
221192, 199, 220divcld 11089 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
222184, 221syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...𝑦) → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
223222adantl 469 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
224176, 183, 185, 223fvmptd 6512 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
225224, 223eqeltrd 2892 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) ∈ ℂ)
226 mulcl 10308 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑥 · 𝑤) ∈ ℂ)
227226adantl 469 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑥 · 𝑤) ∈ ℂ)
22899, 225, 227seqcl 13047 . . . . . . . . . 10 (𝑦 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) ∈ ℂ)
229175, 228mulcld 10348 . . . . . . . . 9 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) ∈ ℂ)
230148, 150reccld 11082 . . . . . . . . 9 (𝑦 ∈ ℕ → (1 / ((2 · (𝑦 + 1)) + 1)) ∈ ℂ)
231229, 230, 161mul12d 10533 . . . . . . . 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 10349 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (1 / ((2 · 𝑦) + 1))))
233232oveq1d 6892 . . . . . . . . . 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 10351 . . . . . . . . . 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 11130 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))))
236160mulid2d 10346 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 · ((2 · (𝑦 + 1))↑2)) = ((2 · (𝑦 + 1))↑2))
237164, 165, 167adddid 10352 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
23843a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → (2 · 1) = 2)
239238oveq2d 6893 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
240237, 239eqtrd 2847 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
241240oveq1d 6892 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
242166, 164, 167addsubassd 10700 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
24345a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 − 1) = 1)
244243oveq2d 6893 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
245241, 242, 2443eqtrd 2851 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
246245oveq2d 6893 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
247168sqvald 13231 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
248246, 247eqtr4d 2850 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1)↑2))
249236, 248oveq12d 6895 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)))
250 2p2e4 11430 . . . . . . . . . . . . . . . . . 18 (2 + 2) = 4
25153, 53, 250mvlladdi 10587 . . . . . . . . . . . . . . . . 17 2 = (4 − 2)
252251a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 = (4 − 2))
253252oveq2d 6893 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1))↑(4 − 2)))
254120rpne0d 12094 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
255218a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ∈ ℤ)
256 4z 11680 . . . . . . . . . . . . . . . . 17 4 ∈ ℤ
257256a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 4 ∈ ℤ)
258146, 254, 255, 257expsubd 13245 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑(4 − 2)) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
259253, 258eqtrd 2847 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
260245eqcomd 2819 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) = ((2 · (𝑦 + 1)) − 1))
261260oveq1d 6892 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · (𝑦 + 1)) − 1)↑2))
262259, 261oveq12d 6895 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)))
263146, 254, 257expclzd 13239 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑4) ∈ ℂ)
264147sqcld 13232 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ∈ ℂ)
265165, 167addcld 10347 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
266170nnne0d 11354 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ≠ 0)
267113nnne0d 11354 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
268164, 265, 266, 267mulne0d 10967 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
269146, 268, 255expne0d 13240 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ≠ 0)
270147, 149, 255expne0d 13240 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ≠ 0)
271263, 160, 264, 269, 270divdiv1d 11120 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))))
272146, 147sqmuld 13246 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) = (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)))
273272eqcomd 2819 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
274273oveq2d 6893 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
275262, 271, 2743eqtrd 2851 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
276235, 249, 2753eqtrd 2851 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
277276oveq2d 6893 . . . . . . . . . 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 2851 . . . . . . . . 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 6893 . . . . . . . 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 2851 . . . . . . 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 2851 . . . . . 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 2814 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
283 simpr 473 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → 𝑘 = (𝑦 + 1))
284283oveq2d 6893 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (2 · 𝑘) = (2 · (𝑦 + 1)))
285284oveq1d 6892 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘)↑4) = ((2 · (𝑦 + 1))↑4))
286284oveq1d 6892 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
287284, 286oveq12d 6895 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))
288287oveq1d 6892 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
289285, 288oveq12d 6895 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
290146, 147mulcld 10348 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
291290sqcld 13232 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ∈ ℂ)
292146, 147, 254, 149mulne0d 10967 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ≠ 0)
293290, 292, 255expne0d 13240 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ≠ 0)
294263, 291, 293divcld 11089 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) ∈ ℂ)
295282, 289, 113, 294fvmptd 6512 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
296295eqcomd 2819 . . . . . . . 8 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))
297296oveq2d 6893 . . . . . . 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 6893 . . . . . 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 13042 . . . . . . . . 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 2819 . . . . . . 7 (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
302301oveq2d 6893 . . . . . 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 2851 . . . . 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 468 . . . 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 2851 . . 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 399 . 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 11326 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 1637  wcel 2157  wne 2985   class class class wbr 4851  cmpt 4930  cfv 6104  (class class class)co 6877  cc 10222  cr 10223  0cc0 10224  1c1 10225   + caddc 10227   · cmul 10229   < clt 10362  cle 10363  cmin 10554   / cdiv 10972  cn 11308  2c2 11359  3c3 11360  4c4 11361  6c6 11363  0cn0 11562  cz 11646  cdc 11762  cuz 11907  +crp 12049  ...cfz 12552  seqcseq 13027  cexp 13086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-3 11368  df-4 11369  df-5 11370  df-6 11371  df-7 11372  df-8 11373  df-9 11374  df-n0 11563  df-z 11647  df-dec 11763  df-uz 11908  df-rp 12050  df-fz 12553  df-seq 13028  df-exp 13087
This theorem is referenced by:  wallispi2  40770
  Copyright terms: Public domain W3C validator