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

Theorem wallispilem4 40765
Description: 𝐹 maps to explicit expression for the ratio of two consecutive values of 𝐼. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
Hypotheses
Ref Expression
wallispilem4.1 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
wallispilem4.2 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
wallispilem4.3 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
wallispilem4.4 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
Assertion
Ref Expression
wallispilem4 𝐺 = 𝐻
Distinct variable groups:   𝑧,𝑛   𝑧,𝐹
Allowed substitution hints:   𝐹(𝑘,𝑛)   𝐺(𝑧,𝑘,𝑛)   𝐻(𝑧,𝑘,𝑛)   𝐼(𝑧,𝑘,𝑛)

Proof of Theorem wallispilem4
Dummy variables 𝑤 𝑦 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6885 . . . . . . 7 (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
21fveq2d 6415 . . . . . 6 (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1)))
31fvoveq1d 6899 . . . . . 6 (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) + 1)))
42, 3oveq12d 6895 . . . . 5 (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))))
5 fveq2 6411 . . . . . . 7 (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
65oveq2d 6893 . . . . . 6 (𝑥 = 1 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘1)))
76oveq2d 6893 . . . . 5 (𝑥 = 1 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))))
84, 7eqeq12d 2828 . . . 4 (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))))
9 oveq2 6885 . . . . . . 7 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
109fveq2d 6415 . . . . . 6 (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦)))
119fvoveq1d 6899 . . . . . 6 (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1)))
1210, 11oveq12d 6895 . . . . 5 (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
13 fveq2 6411 . . . . . . 7 (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦))
1413oveq2d 6893 . . . . . 6 (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦)))
1514oveq2d 6893 . . . . 5 (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))
1612, 15eqeq12d 2828 . . . 4 (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
17 oveq2 6885 . . . . . . 7 (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
1817fveq2d 6415 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1))))
1917fvoveq1d 6899 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1)))
2018, 19oveq12d 6895 . . . . 5 (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))))
21 fveq2 6411 . . . . . . 7 (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1)))
2221oveq2d 6893 . . . . . 6 (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))
2322oveq2d 6893 . . . . 5 (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
2420, 23eqeq12d 2828 . . . 4 (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
25 oveq2 6885 . . . . . . 7 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
2625fveq2d 6415 . . . . . 6 (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛)))
2725fvoveq1d 6899 . . . . . 6 (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1)))
2826, 27oveq12d 6895 . . . . 5 (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
29 fveq2 6411 . . . . . . 7 (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛))
3029oveq2d 6893 . . . . . 6 (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛)))
3130oveq2d 6893 . . . . 5 (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
3228, 31eqeq12d 2828 . . . 4 (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
33 2t1e2 11457 . . . . . . 7 (2 · 1) = 2
3433fveq2i 6414 . . . . . 6 (𝐼‘(2 · 1)) = (𝐼‘2)
3533oveq1i 6887 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
36 2p1e3 11437 . . . . . . . 8 (2 + 1) = 3
3735, 36eqtri 2835 . . . . . . 7 ((2 · 1) + 1) = 3
3837fveq2i 6414 . . . . . 6 (𝐼‘((2 · 1) + 1)) = (𝐼‘3)
3934, 38oveq12i 6889 . . . . 5 ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((𝐼‘2) / (𝐼‘3))
40 2z 11678 . . . . . . . . 9 2 ∈ ℤ
41 uzid 11922 . . . . . . . . 9 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
4240, 41ax-mp 5 . . . . . . . 8 2 ∈ (ℤ‘2)
43 wallispilem4.2 . . . . . . . . . 10 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
4443wallispilem2 40763 . . . . . . . . 9 ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (2 ∈ (ℤ‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))))
4544simp3i 1164 . . . . . . . 8 (2 ∈ (ℤ‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2))))
4642, 45ax-mp 5 . . . . . . 7 (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))
47 2m1e1 11421 . . . . . . . . 9 (2 − 1) = 1
4847oveq1i 6887 . . . . . . . 8 ((2 − 1) / 2) = (1 / 2)
49 2cn 11378 . . . . . . . . . . 11 2 ∈ ℂ
5049subidi 10640 . . . . . . . . . 10 (2 − 2) = 0
5150fveq2i 6414 . . . . . . . . 9 (𝐼‘(2 − 2)) = (𝐼‘0)
5244simp1i 1162 . . . . . . . . 9 (𝐼‘0) = π
5351, 52eqtri 2835 . . . . . . . 8 (𝐼‘(2 − 2)) = π
5448, 53oveq12i 6889 . . . . . . 7 (((2 − 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) · π)
55 ax-1cn 10282 . . . . . . . . 9 1 ∈ ℂ
56 2cnne0 11512 . . . . . . . . 9 (2 ∈ ℂ ∧ 2 ≠ 0)
57 picn 24432 . . . . . . . . 9 π ∈ ℂ
58 div32 10993 . . . . . . . . 9 ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈ ℂ) → ((1 / 2) · π) = (1 · (π / 2)))
5955, 56, 57, 58mp3an 1578 . . . . . . . 8 ((1 / 2) · π) = (1 · (π / 2))
60 2ne0 11399 . . . . . . . . . 10 2 ≠ 0
6157, 49, 60divcli 11055 . . . . . . . . 9 (π / 2) ∈ ℂ
6261mulid2i 10333 . . . . . . . 8 (1 · (π / 2)) = (π / 2)
6359, 62eqtri 2835 . . . . . . 7 ((1 / 2) · π) = (π / 2)
6446, 54, 633eqtri 2839 . . . . . 6 (𝐼‘2) = (π / 2)
65 3z 11679 . . . . . . . . 9 3 ∈ ℤ
66 2re 11377 . . . . . . . . . 10 2 ∈ ℝ
67 3re 11381 . . . . . . . . . 10 3 ∈ ℝ
68 2lt3 11474 . . . . . . . . . 10 2 < 3
6966, 67, 68ltleii 10448 . . . . . . . . 9 2 ≤ 3
70 eluz2 11913 . . . . . . . . 9 (3 ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3))
7140, 65, 69, 70mpbir3an 1434 . . . . . . . 8 3 ∈ (ℤ‘2)
7243wallispilem2 40763 . . . . . . . . 9 ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (3 ∈ (ℤ‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))))
7372simp3i 1164 . . . . . . . 8 (3 ∈ (ℤ‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2))))
7471, 73ax-mp 5 . . . . . . 7 (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
75 3m1e2 11423 . . . . . . . . . 10 (3 − 1) = 2
7675eqcomi 2822 . . . . . . . . 9 2 = (3 − 1)
7776oveq1i 6887 . . . . . . . 8 (2 / 3) = ((3 − 1) / 3)
78 3cn 11382 . . . . . . . . . . 11 3 ∈ ℂ
7978, 49, 55, 36subaddrii 10658 . . . . . . . . . 10 (3 − 2) = 1
8079fveq2i 6414 . . . . . . . . 9 (𝐼‘(3 − 2)) = (𝐼‘1)
8144simp2i 1163 . . . . . . . . 9 (𝐼‘1) = 2
8280, 81eqtr2i 2836 . . . . . . . 8 2 = (𝐼‘(3 − 2))
8377, 82oveq12i 6889 . . . . . . 7 ((2 / 3) · 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
84 3ne0 11401 . . . . . . . . 9 3 ≠ 0
8549, 78, 84divcli 11055 . . . . . . . 8 (2 / 3) ∈ ℂ
8685, 49mulcomi 10336 . . . . . . 7 ((2 / 3) · 2) = (2 · (2 / 3))
8774, 83, 863eqtr2i 2841 . . . . . 6 (𝐼‘3) = (2 · (2 / 3))
8864, 87oveq12i 6889 . . . . 5 ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 / 3)))
89 1z 11676 . . . . . . . . 9 1 ∈ ℤ
90 seq1 13040 . . . . . . . . 9 (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
9189, 90ax-mp 5 . . . . . . . 8 (seq1( · , 𝐹)‘1) = (𝐹‘1)
92 1nn 11319 . . . . . . . . 9 1 ∈ ℕ
93 oveq2 6885 . . . . . . . . . . . . . 14 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
9493, 33syl6eq 2863 . . . . . . . . . . . . 13 (𝑘 = 1 → (2 · 𝑘) = 2)
9593oveq1d 6892 . . . . . . . . . . . . . 14 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
9633oveq1i 6887 . . . . . . . . . . . . . . 15 ((2 · 1) − 1) = (2 − 1)
9796, 47eqtri 2835 . . . . . . . . . . . . . 14 ((2 · 1) − 1) = 1
9895, 97syl6eq 2863 . . . . . . . . . . . . 13 (𝑘 = 1 → ((2 · 𝑘) − 1) = 1)
9994, 98oveq12d 6895 . . . . . . . . . . . 12 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 / 1))
10049div1i 11041 . . . . . . . . . . . 12 (2 / 1) = 2
10199, 100syl6eq 2863 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = 2)
10294oveq1d 6892 . . . . . . . . . . . . 13 (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 + 1))
103102, 36syl6eq 2863 . . . . . . . . . . . 12 (𝑘 = 1 → ((2 · 𝑘) + 1) = 3)
10494, 103oveq12d 6895 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 / 3))
105101, 104oveq12d 6895 . . . . . . . . . 10 (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (2 · (2 / 3)))
106 wallispilem4.1 . . . . . . . . . 10 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
107 ovex 6909 . . . . . . . . . 10 (2 · (2 / 3)) ∈ V
108105, 106, 107fvmpt 6506 . . . . . . . . 9 (1 ∈ ℕ → (𝐹‘1) = (2 · (2 / 3)))
10992, 108ax-mp 5 . . . . . . . 8 (𝐹‘1) = (2 · (2 / 3))
11091, 109eqtr2i 2836 . . . . . . 7 (2 · (2 / 3)) = (seq1( · , 𝐹)‘1)
111110oveq2i 6888 . . . . . 6 ((π / 2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1))
11249, 85mulcli 10335 . . . . . . . . 9 (2 · (2 / 3)) ∈ ℂ
113109, 112eqeltri 2888 . . . . . . . 8 (𝐹‘1) ∈ ℂ
11491, 113eqeltri 2888 . . . . . . 7 (seq1( · , 𝐹)‘1) ∈ ℂ
11549, 78, 60, 84divne0i 11061 . . . . . . . . 9 (2 / 3) ≠ 0
11649, 85, 60, 115mulne0i 10958 . . . . . . . 8 (2 · (2 / 3)) ≠ 0
117110, 116eqnetrri 3056 . . . . . . 7 (seq1( · , 𝐹)‘1) ≠ 0
11861, 114, 117divreci 11058 . . . . . 6 ((π / 2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
119111, 118eqtri 2835 . . . . 5 ((π / 2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
12039, 88, 1193eqtri 2839 . . . 4 ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
121 oveq2 6885 . . . . . . 7 (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
122121adantl 469 . . . . . 6 ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
123 2cnd 11380 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ∈ ℂ)
124 nncn 11316 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
12555a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 1 ∈ ℂ)
126123, 124, 125adddid 10352 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
127123mulid1d 10345 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · 1) = 2)
128127oveq2d 6893 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
129126, 128eqtrd 2847 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
130129oveq1d 6892 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
131123, 124mulcld 10348 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
132131, 123, 125addsubassd 10700 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
13347a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 − 1) = 1)
134133oveq2d 6893 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
135130, 132, 1343eqtrd 2851 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
136135oveq1d 6892 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) = (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))))
137136oveq1d 6892 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
13875a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (3 − 1) = 2)
139138oveq2d 6893 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 1)) = ((2 · 𝑦) + 2))
14078a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 3 ∈ ℂ)
141131, 140, 125addsubassd 10700 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = ((2 · 𝑦) + (3 − 1)))
142139, 141, 1293eqtr4d 2857 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = (2 · (𝑦 + 1)))
143142oveq1d 6892 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
144143oveq1d 6892 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
145137, 144oveq12d 6895 . . . . . . . . 9 (𝑦 ∈ ℕ → (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
14640a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℤ)
147 nnz 11668 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
148147peano2zd 11754 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
149146, 148zmulcld 11757 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℤ)
15066a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℝ)
151 nnre 11315 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
152 1red 10329 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ∈ ℝ)
153151, 152readdcld 10357 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
154 0le2 11397 . . . . . . . . . . . . . . 15 0 ≤ 2
155154a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ 2)
156 nnnn0 11569 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
157156nn0ge0d 11623 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 ≤ 𝑦)
158152, 151addge02d 10904 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ 𝑦 ↔ 1 ≤ (𝑦 + 1)))
159157, 158mpbid 223 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 ≤ (𝑦 + 1))
160150, 153, 155, 159lemulge11d 11249 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ≤ (2 · (𝑦 + 1)))
16140eluz1i 11915 . . . . . . . . . . . . 13 ((2 · (𝑦 + 1)) ∈ (ℤ‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2 · (𝑦 + 1))))
162149, 160, 161sylanbrc 574 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ (ℤ‘2))
16343, 162itgsinexp 40651 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))))
164129oveq1d 6892 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (((2 · 𝑦) + 2) − 2))
165131, 123pncand 10681 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 2) = (2 · 𝑦))
166164, 165eqtrd 2847 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (2 · 𝑦))
167166fveq2d 6415 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦)))
168167oveq2d 6893 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
169163, 168eqtrd 2847 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
170129oveq1d 6892 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = (((2 · 𝑦) + 2) + 1))
171131, 123, 125addassd 10350 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) + 1) = ((2 · 𝑦) + (2 + 1)))
17236a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 + 1) = 3)
173172oveq2d 6893 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 + 1)) = ((2 · 𝑦) + 3))
174170, 171, 1733eqtrd 2851 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = ((2 · 𝑦) + 3))
175174fveq2d 6415 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3)))
176146, 147zmulcld 11757 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
17765a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 3 ∈ ℤ)
178176, 177zaddcld 11755 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℤ)
179150, 151remulcld 10358 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
18067a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 3 ∈ ℝ)
181179, 180readdcld 10357 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ)
182 nnge1 11335 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ≤ 𝑦)
183150, 151, 155, 182lemulge11d 11249 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
184 0re 10330 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
185 3pos 11400 . . . . . . . . . . . . . . . 16 0 < 3
186184, 67, 185ltleii 10448 . . . . . . . . . . . . . . 15 0 ≤ 3
187179, 180addge01d 10903 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ 3 ↔ (2 · 𝑦) ≤ ((2 · 𝑦) + 3)))
188186, 187mpbii 224 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ≤ ((2 · 𝑦) + 3))
189150, 179, 181, 183, 188letrd 10482 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ≤ ((2 · 𝑦) + 3))
19040eluz1i 11915 . . . . . . . . . . . . 13 (((2 · 𝑦) + 3) ∈ (ℤ‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2 · 𝑦) + 3)))
191178, 189, 190sylanbrc 574 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ (ℤ‘2))
19243, 191itgsinexp 40651 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
193175, 192eqtrd 2847 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
194169, 193oveq12d 6895 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
195131, 125addcld 10347 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
196124, 125addcld 10347 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
197123, 196mulcld 10348 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
19860a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ≠ 0)
199 peano2nn 11320 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
200199nnne0d 11354 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
201123, 196, 198, 200mulne0d 10967 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
202195, 197, 201divcld 11089 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ)
203 2nn0 11579 . . . . . . . . . . . . 13 2 ∈ ℕ0
204203a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ∈ ℕ0)
205204, 156nn0mulcld 11625 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ0)
20643wallispilem3 40764 . . . . . . . . . . . 12 ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℝ+)
207206rpcnd 12091 . . . . . . . . . . 11 ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℂ)
208205, 207syl 17 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
209131, 140addcld 10347 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℂ)
210 0red 10331 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ∈ ℝ)
211 2pos 11398 . . . . . . . . . . . . . . . 16 0 < 2
212211a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 < 2)
213 nngt0 11338 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 < 𝑦)
214150, 151, 212, 213mulgt0d 10480 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 < (2 · 𝑦))
215180, 185jctir 512 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (3 ∈ ℝ ∧ 0 < 3))
216 elrp 12051 . . . . . . . . . . . . . . . 16 (3 ∈ ℝ+ ↔ (3 ∈ ℝ ∧ 0 < 3))
217215, 216sylibr 225 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 3 ∈ ℝ+)
218179, 217ltaddrpd 12122 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) < ((2 · 𝑦) + 3))
219210, 179, 181, 214, 218lttrd 10486 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 < ((2 · 𝑦) + 3))
220219gt0ne0d 10880 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ≠ 0)
221197, 209, 220divcld 11089 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ)
222197, 209, 201, 220divne0d 11105 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0)
223178, 146zsubcld 11756 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℤ)
224181, 150subge0d 10905 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ (((2 · 𝑦) + 3) − 2) ↔ 2 ≤ ((2 · 𝑦) + 3)))
225189, 224mpbird 248 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ (((2 · 𝑦) + 3) − 2))
226 elnn0z 11659 . . . . . . . . . . . . . 14 ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤ (((2 · 𝑦) + 3) − 2)))
227223, 225, 226sylanbrc 574 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℕ0)
22843wallispilem3 40764 . . . . . . . . . . . . 13 ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
229227, 228syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
230229rpcnne0d 12098 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0))
231221, 222, 230jca31 506 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0)))
232 divmuldiv 11013 . . . . . . . . . 10 ((((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ ∧ (𝐼‘(2 · 𝑦)) ∈ ℂ) ∧ ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0))) → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
233202, 208, 231, 232syl21anc 857 . . . . . . . . 9 (𝑦 ∈ ℕ → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
234145, 194, 2333eqtr4d 2857 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))))
235131, 140, 123addsubassd 10700 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + (3 − 2)))
23679a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (3 − 2) = 1)
237236oveq2d 6893 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 2)) = ((2 · 𝑦) + 1))
238235, 237eqtrd 2847 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + 1))
239238fveq2d 6415 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1)))
240239oveq2d 6893 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
241240oveq2d 6893 . . . . . . . 8 (𝑦 ∈ ℕ → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
242234, 241eqtrd 2847 . . . . . . 7 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
243242adantr 468 . . . . . 6 ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
244 elnnuz 11945 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ‘1))
245244biimpi 207 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘1))
246 seqp1 13042 . . . . . . . . . . . 12 (𝑦 ∈ (ℤ‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
247245, 246syl 17 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
248106a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))
249 oveq2 6885 . . . . . . . . . . . . . . . 16 (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
250249oveq1d 6892 . . . . . . . . . . . . . . . 16 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
251249, 250oveq12d 6895 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
252249oveq1d 6892 . . . . . . . . . . . . . . . 16 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
253249, 252oveq12d 6895 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
254251, 253oveq12d 6895 . . . . . . . . . . . . . 14 (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
255254adantl 469 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
256150, 153remulcld 10358 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
257256, 152resubcld 10746 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
258 1lt2 11473 . . . . . . . . . . . . . . . . . . 19 1 < 2
259258a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 1 < 2)
260 nnrp 12059 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
261152, 260ltaddrp2d 12123 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
262150, 153, 259, 261mulgt1d 11248 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
263152, 262gtned 10460 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
264197, 125, 263subne0d 10689 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
265256, 257, 264redivcld 11141 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ)
266174, 181eqeltrd 2892 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ)
267174, 220eqnetrd 3052 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
268256, 266, 267redivcld 11141 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ)
269265, 268remulcld 10358 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ)
270248, 255, 199, 269fvmptd 6512 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
271270oveq2d 6893 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
272247, 271eqtrd 2847 . . . . . . . . . 10 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
273272oveq2d 6893 . . . . . . . . 9 (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))))
274273oveq2d 6893 . . . . . . . 8 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))))
275135oveq2d 6893 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)))
276174oveq2d 6893 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
277275, 276oveq12d 6895 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
278277oveq2d 6893 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
279278oveq2d 6893 . . . . . . . . . 10 (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
280279oveq2d 6893 . . . . . . . . 9 (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))))
281 elfznn 12596 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ)
282281adantl 469 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ)
283106a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℕ → 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))
284 oveq2 6885 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤))
285284oveq1d 6892 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1))
286284, 285oveq12d 6895 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1)))
287284oveq1d 6892 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1))
288284, 287oveq12d 6895 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1)))
289286, 288oveq12d 6895 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
290289adantl 469 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℕ ∧ 𝑘 = 𝑤) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
291 id 22 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℕ → 𝑤 ∈ ℕ)
292 2rp 12054 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℝ+
293292a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 2 ∈ ℝ+)
294 nnrp 12059 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 𝑤 ∈ ℝ+)
295293, 294rpmulcld 12105 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ+)
29666a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 2 ∈ ℝ)
297 nnre 11315 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 𝑤 ∈ ℝ)
298296, 297remulcld 10358 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ)
299 1red 10329 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 1 ∈ ℝ)
300298, 299resubcld 10746 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ)
301 nnge1 11335 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 1 ≤ 𝑤)
302 nncn 11316 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
303302mulid2d 10346 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℕ → (1 · 𝑤) = 𝑤)
304299, 296, 294ltmul1d 12130 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ ℕ → (1 < 2 ↔ (1 · 𝑤) < (2 · 𝑤)))
305258, 304mpbii 224 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℕ → (1 · 𝑤) < (2 · 𝑤))
306303, 305eqbrtrrd 4875 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤))
307299, 297, 298, 301, 306lelttrd 10483 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 1 < (2 · 𝑤))
308299, 298posdifd 10902 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → (1 < (2 · 𝑤) ↔ 0 < ((2 · 𝑤) − 1)))
309307, 308mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 0 < ((2 · 𝑤) − 1))
310300, 309elrpd 12086 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ+)
311295, 310rpdivcld 12106 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) − 1)) ∈ ℝ+)
312154a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 0 ≤ 2)
313294rpge0d 12093 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 0 ≤ 𝑤)
314296, 297, 312, 313mulge0d 10892 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 0 ≤ (2 · 𝑤))
315298, 314ge0p1rpd 12119 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → ((2 · 𝑤) + 1) ∈ ℝ+)
316295, 315rpdivcld 12106 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) + 1)) ∈ ℝ+)
317311, 316rpmulcld 12105 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℕ → (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))) ∈ ℝ+)
318283, 290, 291, 317fvmptd 6512 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℕ → (𝐹𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
319318, 317eqeltrd 2892 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℕ → (𝐹𝑤) ∈ ℝ+)
320282, 319syl 17 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹𝑤) ∈ ℝ+)
321 rpmulcl 12072 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ℝ+𝑧 ∈ ℝ+) → (𝑤 · 𝑧) ∈ ℝ+)
322321adantl 469 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ+𝑧 ∈ ℝ+)) → (𝑤 · 𝑧) ∈ ℝ+)
323245, 320, 322seqcl 13047 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℝ+)
324323rpcnne0d 12098 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0))
325292a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 2 ∈ ℝ+)
326151, 157ge0p1rpd 12119 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ+)
327325, 326rpmulcld 12105 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ+)
328150, 151, 155, 157mulge0d 10892 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 0 ≤ (2 · 𝑦))
329179, 328ge0p1rpd 12119 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ+)
330327, 329rpdivcld 12106 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) ∈ ℝ+)
331325, 260rpmulcld 12105 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ+)
332331, 217rpaddcld 12104 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ+)
333327, 332rpdivcld 12106 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℝ+)
334330, 333rpmulcld 12105 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℝ+)
335334rpcnne0d 12098 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0))
336 divdiv1 11024 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0) ∧ ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)) → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
337125, 324, 335, 336syl3anc 1483 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
338337eqcomd 2819 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
339338oveq2d 6893 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) = ((π / 2) · ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
34061a1i 11 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
341323rpcnd 12091 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℂ)
342323rpne0d 12094 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ≠ 0)
343341, 342reccld 11082 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑦)) ∈ ℂ)
344334rpcnd 12091 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
345334rpne0d 12094 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)
346340, 343, 344, 345divassd 11124 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = ((π / 2) · ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
347135, 264eqnetrrd 3053 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
348197, 195, 197, 209, 347, 220divmuldivd 11130 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))))
349348oveq2d 6893 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)))))
350340, 343mulcld 10348 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
351197, 197mulcld 10348 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
352195, 209mulcld 10348 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ∈ ℂ)
353197, 197, 201, 201mulne0d 10967 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ≠ 0)
354195, 209, 347, 220mulne0d 10967 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ≠ 0)
355350, 351, 352, 353, 354divdiv2d 11121 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)))) = ((((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
356350, 352, 351, 353divassd 11124 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))))
357355, 356eqtrd 2847 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))))
358195, 197, 197, 209, 201, 220, 201divdivdivd 11136 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
359358eqcomd 2819 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
360359oveq2d 6893 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
361349, 357, 3603eqtrd 2851 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
362339, 346, 3613eqtr2d 2853 . . . . . . . . 9 (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
36357a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → π ∈ ℂ)
364363halfcld 11547 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
365364, 343mulcld 10348 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
366202, 221, 222divcld 11089 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
367365, 366mulcomd 10349 . . . . . . . . 9 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
368280, 362, 3673eqtrd 2851 . . . . . . . 8 (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
369274, 368eqtrd 2847 . . . . . . 7 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
370369adantr 468 . . . . . 6 ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
371122, 243, 3703eqtr4d 2857 . . . . 5 ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
372371ex 399 . . . 4 (𝑦 ∈ ℕ → (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
3738, 16, 24, 32, 120, 372nnind 11326 . . 3 (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
374373mpteq2ia 4941 . 2 (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
375 wallispilem4.3 . 2 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
376 wallispilem4.4 . 2 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
377374, 375, 3763eqtr4i 2845 1 𝐺 = 𝐻
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  0cn0 11562  cz 11646  cuz 11907  +crp 12049  (,)cioo 12396  ...cfz 12552  seqcseq 13027  cexp 13086  sincsin 15017  πcpi 15020  citg 23605
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-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cc 9545  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  ax-pre-sup 10302  ax-addf 10303  ax-mulf 10304
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  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-symdif 4049  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-int 4677  df-iun 4721  df-iin 4722  df-disj 4820  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-se 5278  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-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-of 7130  df-ofr 7131  df-om 7299  df-1st 7401  df-2nd 7402  df-supp 7533  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-2o 7800  df-oadd 7803  df-omul 7804  df-er 7982  df-map 8097  df-pm 8098  df-ixp 8149  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-fsupp 8518  df-fi 8559  df-sup 8590  df-inf 8591  df-oi 8657  df-card 9051  df-acn 9054  df-cda 9278  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-q 12011  df-rp 12050  df-xneg 12165  df-xadd 12166  df-xmul 12167  df-ioo 12400  df-ioc 12401  df-ico 12402  df-icc 12403  df-fz 12553  df-fzo 12693  df-fl 12820  df-mod 12896  df-seq 13028  df-exp 13087  df-fac 13284  df-bc 13313  df-hash 13341  df-shft 14033  df-cj 14065  df-re 14066  df-im 14067  df-sqrt 14201  df-abs 14202  df-limsup 14428  df-clim 14445  df-rlim 14446  df-sum 14643  df-ef 15021  df-sin 15023  df-cos 15024  df-pi 15026  df-struct 16073  df-ndx 16074  df-slot 16075  df-base 16077  df-sets 16078  df-ress 16079  df-plusg 16169  df-mulr 16170  df-starv 16171  df-sca 16172  df-vsca 16173  df-ip 16174  df-tset 16175  df-ple 16176  df-ds 16178  df-unif 16179  df-hom 16180  df-cco 16181  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17954  df-cmn 18399  df-psmet 19949  df-xmet 19950  df-met 19951  df-bl 19952  df-mopn 19953  df-fbas 19954  df-fg 19955  df-cnfld 19958  df-top 20916  df-topon 20933  df-topsp 20955  df-bases 20968  df-cld 21041  df-ntr 21042  df-cls 21043  df-nei 21120  df-lp 21158  df-perf 21159  df-cn 21249  df-cnp 21250  df-haus 21337  df-cmp 21408  df-tx 21583  df-hmeo 21776  df-fil 21867  df-fm 21959  df-flim 21960  df-flf 21961  df-xms 22342  df-ms 22343  df-tms 22344  df-cncf 22898  df-ovol 23451  df-vol 23452  df-mbf 23606  df-itg1 23607  df-itg2 23608  df-ibl 23609  df-itg 23610  df-0p 23657  df-limc 23850  df-dv 23851
This theorem is referenced by:  wallispilem5  40766
  Copyright terms: Public domain W3C validator