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 43934
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 7337 . . . . . . 7 (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
21fveq2d 6823 . . . . . 6 (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1)))
31fvoveq1d 7351 . . . . . 6 (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) + 1)))
42, 3oveq12d 7347 . . . . 5 (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))))
5 fveq2 6819 . . . . . . 7 (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
65oveq2d 7345 . . . . . 6 (𝑥 = 1 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘1)))
76oveq2d 7345 . . . . 5 (𝑥 = 1 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))))
84, 7eqeq12d 2752 . . . 4 (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))))
9 oveq2 7337 . . . . . . 7 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
109fveq2d 6823 . . . . . 6 (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦)))
119fvoveq1d 7351 . . . . . 6 (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1)))
1210, 11oveq12d 7347 . . . . 5 (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
13 fveq2 6819 . . . . . . 7 (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦))
1413oveq2d 7345 . . . . . 6 (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦)))
1514oveq2d 7345 . . . . 5 (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))
1612, 15eqeq12d 2752 . . . 4 (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
17 oveq2 7337 . . . . . . 7 (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
1817fveq2d 6823 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1))))
1917fvoveq1d 7351 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1)))
2018, 19oveq12d 7347 . . . . 5 (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))))
21 fveq2 6819 . . . . . . 7 (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1)))
2221oveq2d 7345 . . . . . 6 (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))
2322oveq2d 7345 . . . . 5 (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
2420, 23eqeq12d 2752 . . . 4 (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
25 oveq2 7337 . . . . . . 7 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
2625fveq2d 6823 . . . . . 6 (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛)))
2725fvoveq1d 7351 . . . . . 6 (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1)))
2826, 27oveq12d 7347 . . . . 5 (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
29 fveq2 6819 . . . . . . 7 (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛))
3029oveq2d 7345 . . . . . 6 (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛)))
3130oveq2d 7345 . . . . 5 (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
3228, 31eqeq12d 2752 . . . 4 (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
33 2t1e2 12229 . . . . . . 7 (2 · 1) = 2
3433fveq2i 6822 . . . . . 6 (𝐼‘(2 · 1)) = (𝐼‘2)
3533oveq1i 7339 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
36 2p1e3 12208 . . . . . . . 8 (2 + 1) = 3
3735, 36eqtri 2764 . . . . . . 7 ((2 · 1) + 1) = 3
3837fveq2i 6822 . . . . . 6 (𝐼‘((2 · 1) + 1)) = (𝐼‘3)
3934, 38oveq12i 7341 . . . . 5 ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((𝐼‘2) / (𝐼‘3))
40 2z 12445 . . . . . . . . 9 2 ∈ ℤ
41 uzid 12690 . . . . . . . . 9 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
4240, 41ax-mp 5 . . . . . . . 8 2 ∈ (ℤ‘2)
43 wallispilem4.2 . . . . . . . . . 10 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
4443wallispilem2 43932 . . . . . . . . 9 ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (2 ∈ (ℤ‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))))
4544simp3i 1140 . . . . . . . 8 (2 ∈ (ℤ‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2))))
4642, 45ax-mp 5 . . . . . . 7 (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))
47 2m1e1 12192 . . . . . . . . 9 (2 − 1) = 1
4847oveq1i 7339 . . . . . . . 8 ((2 − 1) / 2) = (1 / 2)
49 2cn 12141 . . . . . . . . . . 11 2 ∈ ℂ
5049subidi 11385 . . . . . . . . . 10 (2 − 2) = 0
5150fveq2i 6822 . . . . . . . . 9 (𝐼‘(2 − 2)) = (𝐼‘0)
5244simp1i 1138 . . . . . . . . 9 (𝐼‘0) = π
5351, 52eqtri 2764 . . . . . . . 8 (𝐼‘(2 − 2)) = π
5448, 53oveq12i 7341 . . . . . . 7 (((2 − 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) · π)
55 ax-1cn 11022 . . . . . . . . 9 1 ∈ ℂ
56 2cnne0 12276 . . . . . . . . 9 (2 ∈ ℂ ∧ 2 ≠ 0)
57 picn 25714 . . . . . . . . 9 π ∈ ℂ
58 div32 11746 . . . . . . . . 9 ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈ ℂ) → ((1 / 2) · π) = (1 · (π / 2)))
5955, 56, 57, 58mp3an 1460 . . . . . . . 8 ((1 / 2) · π) = (1 · (π / 2))
60 2ne0 12170 . . . . . . . . . 10 2 ≠ 0
6157, 49, 60divcli 11810 . . . . . . . . 9 (π / 2) ∈ ℂ
6261mulid2i 11073 . . . . . . . 8 (1 · (π / 2)) = (π / 2)
6359, 62eqtri 2764 . . . . . . 7 ((1 / 2) · π) = (π / 2)
6446, 54, 633eqtri 2768 . . . . . 6 (𝐼‘2) = (π / 2)
65 3z 12446 . . . . . . . . 9 3 ∈ ℤ
66 2re 12140 . . . . . . . . . 10 2 ∈ ℝ
67 3re 12146 . . . . . . . . . 10 3 ∈ ℝ
68 2lt3 12238 . . . . . . . . . 10 2 < 3
6966, 67, 68ltleii 11191 . . . . . . . . 9 2 ≤ 3
70 eluz2 12681 . . . . . . . . 9 (3 ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3))
7140, 65, 69, 70mpbir3an 1340 . . . . . . . 8 3 ∈ (ℤ‘2)
7243wallispilem2 43932 . . . . . . . . 9 ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (3 ∈ (ℤ‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))))
7372simp3i 1140 . . . . . . . 8 (3 ∈ (ℤ‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2))))
7471, 73ax-mp 5 . . . . . . 7 (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
75 3m1e2 12194 . . . . . . . . . 10 (3 − 1) = 2
7675eqcomi 2745 . . . . . . . . 9 2 = (3 − 1)
7776oveq1i 7339 . . . . . . . 8 (2 / 3) = ((3 − 1) / 3)
78 3cn 12147 . . . . . . . . . . 11 3 ∈ ℂ
7978, 49, 55, 36subaddrii 11403 . . . . . . . . . 10 (3 − 2) = 1
8079fveq2i 6822 . . . . . . . . 9 (𝐼‘(3 − 2)) = (𝐼‘1)
8144simp2i 1139 . . . . . . . . 9 (𝐼‘1) = 2
8280, 81eqtr2i 2765 . . . . . . . 8 2 = (𝐼‘(3 − 2))
8377, 82oveq12i 7341 . . . . . . 7 ((2 / 3) · 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
84 3ne0 12172 . . . . . . . . 9 3 ≠ 0
8549, 78, 84divcli 11810 . . . . . . . 8 (2 / 3) ∈ ℂ
8685, 49mulcomi 11076 . . . . . . 7 ((2 / 3) · 2) = (2 · (2 / 3))
8774, 83, 863eqtr2i 2770 . . . . . 6 (𝐼‘3) = (2 · (2 / 3))
8864, 87oveq12i 7341 . . . . 5 ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 / 3)))
89 1z 12443 . . . . . . . . 9 1 ∈ ℤ
90 seq1 13827 . . . . . . . . 9 (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
9189, 90ax-mp 5 . . . . . . . 8 (seq1( · , 𝐹)‘1) = (𝐹‘1)
92 1nn 12077 . . . . . . . . 9 1 ∈ ℕ
93 oveq2 7337 . . . . . . . . . . . . . 14 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
9493, 33eqtrdi 2792 . . . . . . . . . . . . 13 (𝑘 = 1 → (2 · 𝑘) = 2)
9593oveq1d 7344 . . . . . . . . . . . . . 14 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
9633oveq1i 7339 . . . . . . . . . . . . . . 15 ((2 · 1) − 1) = (2 − 1)
9796, 47eqtri 2764 . . . . . . . . . . . . . 14 ((2 · 1) − 1) = 1
9895, 97eqtrdi 2792 . . . . . . . . . . . . 13 (𝑘 = 1 → ((2 · 𝑘) − 1) = 1)
9994, 98oveq12d 7347 . . . . . . . . . . . 12 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 / 1))
10049div1i 11796 . . . . . . . . . . . 12 (2 / 1) = 2
10199, 100eqtrdi 2792 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = 2)
10294oveq1d 7344 . . . . . . . . . . . . 13 (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 + 1))
103102, 36eqtrdi 2792 . . . . . . . . . . . 12 (𝑘 = 1 → ((2 · 𝑘) + 1) = 3)
10494, 103oveq12d 7347 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 / 3))
105101, 104oveq12d 7347 . . . . . . . . . 10 (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (2 · (2 / 3)))
106 wallispilem4.1 . . . . . . . . . 10 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
107 ovex 7362 . . . . . . . . . 10 (2 · (2 / 3)) ∈ V
108105, 106, 107fvmpt 6925 . . . . . . . . 9 (1 ∈ ℕ → (𝐹‘1) = (2 · (2 / 3)))
10992, 108ax-mp 5 . . . . . . . 8 (𝐹‘1) = (2 · (2 / 3))
11091, 109eqtr2i 2765 . . . . . . 7 (2 · (2 / 3)) = (seq1( · , 𝐹)‘1)
111110oveq2i 7340 . . . . . 6 ((π / 2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1))
11249, 85mulcli 11075 . . . . . . . . 9 (2 · (2 / 3)) ∈ ℂ
113109, 112eqeltri 2833 . . . . . . . 8 (𝐹‘1) ∈ ℂ
11491, 113eqeltri 2833 . . . . . . 7 (seq1( · , 𝐹)‘1) ∈ ℂ
11549, 78, 60, 84divne0i 11816 . . . . . . . . 9 (2 / 3) ≠ 0
11649, 85, 60, 115mulne0i 11711 . . . . . . . 8 (2 · (2 / 3)) ≠ 0
117110, 116eqnetrri 3012 . . . . . . 7 (seq1( · , 𝐹)‘1) ≠ 0
11861, 114, 117divreci 11813 . . . . . 6 ((π / 2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
119111, 118eqtri 2764 . . . . 5 ((π / 2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
12039, 88, 1193eqtri 2768 . . . 4 ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
121 oveq2 7337 . . . . . . 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 482 . . . . . 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 12144 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ∈ ℂ)
124 nncn 12074 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
12555a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 1 ∈ ℂ)
126123, 124, 125adddid 11092 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
127123mulid1d 11085 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · 1) = 2)
128127oveq2d 7345 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
129126, 128eqtrd 2776 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
130129oveq1d 7344 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
131123, 124mulcld 11088 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
132131, 123, 125addsubassd 11445 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
13347a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 − 1) = 1)
134133oveq2d 7345 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
135130, 132, 1343eqtrd 2780 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
136135oveq1d 7344 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) = (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))))
137136oveq1d 7344 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
13875a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (3 − 1) = 2)
139138oveq2d 7345 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 1)) = ((2 · 𝑦) + 2))
14078a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 3 ∈ ℂ)
141131, 140, 125addsubassd 11445 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = ((2 · 𝑦) + (3 − 1)))
142139, 141, 1293eqtr4d 2786 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = (2 · (𝑦 + 1)))
143142oveq1d 7344 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
144143oveq1d 7344 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
145137, 144oveq12d 7347 . . . . . . . . 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 12435 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
148147peano2zd 12522 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
149146, 148zmulcld 12525 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℤ)
15066a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℝ)
151 nnre 12073 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
152 1red 11069 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ∈ ℝ)
153151, 152readdcld 11097 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
154 0le2 12168 . . . . . . . . . . . . . . 15 0 ≤ 2
155154a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ 2)
156 nnnn0 12333 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
157156nn0ge0d 12389 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 ≤ 𝑦)
158152, 151addge02d 11657 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ 𝑦 ↔ 1 ≤ (𝑦 + 1)))
159157, 158mpbid 231 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 ≤ (𝑦 + 1))
160150, 153, 155, 159lemulge11d 12005 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ≤ (2 · (𝑦 + 1)))
16140eluz1i 12683 . . . . . . . . . . . . 13 ((2 · (𝑦 + 1)) ∈ (ℤ‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2 · (𝑦 + 1))))
162149, 160, 161sylanbrc 583 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ (ℤ‘2))
16343, 162itgsinexp 43821 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))))
164129oveq1d 7344 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (((2 · 𝑦) + 2) − 2))
165131, 123pncand 11426 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 2) = (2 · 𝑦))
166164, 165eqtrd 2776 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (2 · 𝑦))
167166fveq2d 6823 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦)))
168167oveq2d 7345 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
169163, 168eqtrd 2776 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
170129oveq1d 7344 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = (((2 · 𝑦) + 2) + 1))
171131, 123, 125addassd 11090 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) + 1) = ((2 · 𝑦) + (2 + 1)))
17236a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 + 1) = 3)
173172oveq2d 7345 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 + 1)) = ((2 · 𝑦) + 3))
174170, 171, 1733eqtrd 2780 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = ((2 · 𝑦) + 3))
175174fveq2d 6823 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3)))
176146, 147zmulcld 12525 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
17765a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 3 ∈ ℤ)
178176, 177zaddcld 12523 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℤ)
179150, 151remulcld 11098 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
18067a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 3 ∈ ℝ)
181179, 180readdcld 11097 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ)
182 nnge1 12094 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ≤ 𝑦)
183150, 151, 155, 182lemulge11d 12005 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
184 0re 11070 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
185 3pos 12171 . . . . . . . . . . . . . . . 16 0 < 3
186184, 67, 185ltleii 11191 . . . . . . . . . . . . . . 15 0 ≤ 3
187179, 180addge01d 11656 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ 3 ↔ (2 · 𝑦) ≤ ((2 · 𝑦) + 3)))
188186, 187mpbii 232 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ≤ ((2 · 𝑦) + 3))
189150, 179, 181, 183, 188letrd 11225 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ≤ ((2 · 𝑦) + 3))
19040eluz1i 12683 . . . . . . . . . . . . 13 (((2 · 𝑦) + 3) ∈ (ℤ‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2 · 𝑦) + 3)))
191178, 189, 190sylanbrc 583 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ (ℤ‘2))
19243, 191itgsinexp 43821 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
193175, 192eqtrd 2776 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
194169, 193oveq12d 7347 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
195131, 125addcld 11087 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
196124, 125addcld 11087 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
197123, 196mulcld 11088 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
19860a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ≠ 0)
199 peano2nn 12078 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
200199nnne0d 12116 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
201123, 196, 198, 200mulne0d 11720 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
202195, 197, 201divcld 11844 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ)
203 2nn0 12343 . . . . . . . . . . . . 13 2 ∈ ℕ0
204203a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ∈ ℕ0)
205204, 156nn0mulcld 12391 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ0)
20643wallispilem3 43933 . . . . . . . . . . . 12 ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℝ+)
207206rpcnd 12867 . . . . . . . . . . 11 ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℂ)
208205, 207syl 17 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
209131, 140addcld 11087 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℂ)
210 0red 11071 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ∈ ℝ)
211 2pos 12169 . . . . . . . . . . . . . . . 16 0 < 2
212211a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 < 2)
213 nngt0 12097 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 < 𝑦)
214150, 151, 212, 213mulgt0d 11223 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 < (2 · 𝑦))
215180, 185jctir 521 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (3 ∈ ℝ ∧ 0 < 3))
216 elrp 12825 . . . . . . . . . . . . . . . 16 (3 ∈ ℝ+ ↔ (3 ∈ ℝ ∧ 0 < 3))
217215, 216sylibr 233 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 3 ∈ ℝ+)
218179, 217ltaddrpd 12898 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) < ((2 · 𝑦) + 3))
219210, 179, 181, 214, 218lttrd 11229 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 < ((2 · 𝑦) + 3))
220219gt0ne0d 11632 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ≠ 0)
221197, 209, 220divcld 11844 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ)
222197, 209, 201, 220divne0d 11860 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0)
223178, 146zsubcld 12524 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℤ)
224181, 150subge0d 11658 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ (((2 · 𝑦) + 3) − 2) ↔ 2 ≤ ((2 · 𝑦) + 3)))
225189, 224mpbird 256 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ (((2 · 𝑦) + 3) − 2))
226 elnn0z 12425 . . . . . . . . . . . . . 14 ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤ (((2 · 𝑦) + 3) − 2)))
227223, 225, 226sylanbrc 583 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℕ0)
22843wallispilem3 43933 . . . . . . . . . . . . 13 ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
229227, 228syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
230229rpcnne0d 12874 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0))
231221, 222, 230jca31 515 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0)))
232 divmuldiv 11768 . . . . . . . . . 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 835 . . . . . . . . 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 2786 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))))
235131, 140, 123addsubassd 11445 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + (3 − 2)))
23679a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (3 − 2) = 1)
237236oveq2d 7345 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 2)) = ((2 · 𝑦) + 1))
238235, 237eqtrd 2776 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + 1))
239238fveq2d 6823 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1)))
240239oveq2d 7345 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
241240oveq2d 7345 . . . . . . . 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 2776 . . . . . . 7 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
243242adantr 481 . . . . . 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 12715 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ‘1))
245244biimpi 215 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘1))
246 seqp1 13829 . . . . . . . . . . . 12 (𝑦 ∈ (ℤ‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
247245, 246syl 17 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
248 oveq2 7337 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
249248oveq1d 7344 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
250248, 249oveq12d 7347 . . . . . . . . . . . . . 14 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
251248oveq1d 7344 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
252248, 251oveq12d 7347 . . . . . . . . . . . . . 14 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
253250, 252oveq12d 7347 . . . . . . . . . . . . 13 (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
254150, 153remulcld 11098 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
255254, 152resubcld 11496 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
256 1lt2 12237 . . . . . . . . . . . . . . . . . . 19 1 < 2
257256a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 1 < 2)
258 nnrp 12834 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
259152, 258ltaddrp2d 12899 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
260150, 153, 257, 259mulgt1d 12004 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
261152, 260gtned 11203 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
262197, 125, 261subne0d 11434 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
263254, 255, 262redivcld 11896 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ)
264174, 181eqeltrd 2837 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ)
265174, 220eqnetrd 3008 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
266254, 264, 265redivcld 11896 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ)
267263, 266remulcld 11098 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ)
268106, 253, 199, 267fvmptd3 6948 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
269268oveq2d 7345 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
270247, 269eqtrd 2776 . . . . . . . . . 10 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
271270oveq2d 7345 . . . . . . . . 9 (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))))
272271oveq2d 7345 . . . . . . . 8 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))))
273135oveq2d 7345 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)))
274174oveq2d 7345 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
275273, 274oveq12d 7347 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
276275oveq2d 7345 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
277276oveq2d 7345 . . . . . . . . . 10 (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
278277oveq2d 7345 . . . . . . . . 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)))))))
279 elfznn 13378 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ)
280279adantl 482 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ)
281 oveq2 7337 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤))
282281oveq1d 7344 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1))
283281, 282oveq12d 7347 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1)))
284281oveq1d 7344 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1))
285281, 284oveq12d 7347 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1)))
286283, 285oveq12d 7347 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
287 id 22 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℕ → 𝑤 ∈ ℕ)
288 2rp 12828 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℝ+
289288a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 2 ∈ ℝ+)
290 nnrp 12834 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 𝑤 ∈ ℝ+)
291289, 290rpmulcld 12881 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ+)
29266a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 2 ∈ ℝ)
293 nnre 12073 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 𝑤 ∈ ℝ)
294292, 293remulcld 11098 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ)
295 1red 11069 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 1 ∈ ℝ)
296294, 295resubcld 11496 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ)
297 nnge1 12094 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 1 ≤ 𝑤)
298 nncn 12074 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
299298mulid2d 11086 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℕ → (1 · 𝑤) = 𝑤)
300295, 292, 290ltmul1d 12906 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ ℕ → (1 < 2 ↔ (1 · 𝑤) < (2 · 𝑤)))
301256, 300mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℕ → (1 · 𝑤) < (2 · 𝑤))
302299, 301eqbrtrrd 5113 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤))
303295, 293, 294, 297, 302lelttrd 11226 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 1 < (2 · 𝑤))
304295, 294posdifd 11655 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → (1 < (2 · 𝑤) ↔ 0 < ((2 · 𝑤) − 1)))
305303, 304mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 0 < ((2 · 𝑤) − 1))
306296, 305elrpd 12862 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ+)
307291, 306rpdivcld 12882 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) − 1)) ∈ ℝ+)
308154a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 0 ≤ 2)
309290rpge0d 12869 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 0 ≤ 𝑤)
310292, 293, 308, 309mulge0d 11645 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 0 ≤ (2 · 𝑤))
311294, 310ge0p1rpd 12895 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → ((2 · 𝑤) + 1) ∈ ℝ+)
312291, 311rpdivcld 12882 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) + 1)) ∈ ℝ+)
313307, 312rpmulcld 12881 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℕ → (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))) ∈ ℝ+)
314106, 286, 287, 313fvmptd3 6948 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℕ → (𝐹𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
315314, 313eqeltrd 2837 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℕ → (𝐹𝑤) ∈ ℝ+)
316280, 315syl 17 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹𝑤) ∈ ℝ+)
317 rpmulcl 12846 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ℝ+𝑧 ∈ ℝ+) → (𝑤 · 𝑧) ∈ ℝ+)
318317adantl 482 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ+𝑧 ∈ ℝ+)) → (𝑤 · 𝑧) ∈ ℝ+)
319245, 316, 318seqcl 13836 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℝ+)
320319rpcnne0d 12874 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0))
321288a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 2 ∈ ℝ+)
322151, 157ge0p1rpd 12895 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ+)
323321, 322rpmulcld 12881 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ+)
324150, 151, 155, 157mulge0d 11645 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 0 ≤ (2 · 𝑦))
325179, 324ge0p1rpd 12895 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ+)
326323, 325rpdivcld 12882 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) ∈ ℝ+)
327321, 258rpmulcld 12881 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ+)
328327, 217rpaddcld 12880 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ+)
329323, 328rpdivcld 12882 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℝ+)
330326, 329rpmulcld 12881 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℝ+)
331330rpcnne0d 12874 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0))
332 divdiv1 11779 . . . . . . . . . . . . 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))))))
333125, 320, 331, 332syl3anc 1370 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
334333eqcomd 2742 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
335334oveq2d 7345 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) = ((π / 2) · ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
33661a1i 11 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
337319rpcnd 12867 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℂ)
338319rpne0d 12870 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ≠ 0)
339337, 338reccld 11837 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑦)) ∈ ℂ)
340330rpcnd 12867 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
341330rpne0d 12870 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)
342336, 339, 340, 341divassd 11879 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = ((π / 2) · ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
343135, 262eqnetrrd 3009 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
344197, 195, 197, 209, 343, 220divmuldivd 11885 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))))
345344oveq2d 7345 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)))))
346336, 339mulcld 11088 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
347197, 197mulcld 11088 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
348195, 209mulcld 11088 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ∈ ℂ)
349197, 197, 201, 201mulne0d 11720 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ≠ 0)
350195, 209, 343, 220mulne0d 11720 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ≠ 0)
351346, 347, 348, 349, 350divdiv2d 11876 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)))) = ((((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
352346, 348, 347, 349divassd 11879 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))))
353351, 352eqtrd 2776 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))))
354195, 197, 197, 209, 201, 220, 201divdivdivd 11891 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
355354eqcomd 2742 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
356355oveq2d 7345 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
357345, 353, 3563eqtrd 2780 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
358335, 342, 3573eqtr2d 2782 . . . . . . . . 9 (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
35957a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → π ∈ ℂ)
360359halfcld 12311 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
361360, 339mulcld 11088 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
362202, 221, 222divcld 11844 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
363361, 362mulcomd 11089 . . . . . . . . 9 (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
364278, 358, 3633eqtrd 2780 . . . . . . . 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( · , 𝐹)‘𝑦)))))
365272, 364eqtrd 2776 . . . . . . 7 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
366365adantr 481 . . . . . 6 ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
367122, 243, 3663eqtr4d 2786 . . . . 5 ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
368367ex 413 . . . 4 (𝑦 ∈ ℕ → (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
3698, 16, 24, 32, 120, 368nnind 12084 . . 3 (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
370369mpteq2ia 5192 . 2 (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
371 wallispilem4.3 . 2 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
372 wallispilem4.4 . 2 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
373370, 371, 3723eqtr4i 2774 1 𝐺 = 𝐻
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  wne 2940   class class class wbr 5089  cmpt 5172  cfv 6473  (class class class)co 7329  cc 10962  cr 10963  0cc0 10964  1c1 10965   + caddc 10967   · cmul 10969   < clt 11102  cle 11103  cmin 11298   / cdiv 11725  cn 12066  2c2 12121  3c3 12122  0cn0 12326  cz 12412  cuz 12675  +crp 12823  (,)cioo 13172  ...cfz 13332  seqcseq 13814  cexp 13875  sincsin 15864  πcpi 15867  citg 24880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-inf2 9490  ax-cc 10284  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041  ax-pre-sup 11042  ax-addf 11043  ax-mulf 11044
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-symdif 4188  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-tp 4577  df-op 4579  df-uni 4852  df-int 4894  df-iun 4940  df-iin 4941  df-disj 5055  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-se 5570  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-isom 6482  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-of 7587  df-ofr 7588  df-om 7773  df-1st 7891  df-2nd 7892  df-supp 8040  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-1o 8359  df-2o 8360  df-oadd 8363  df-omul 8364  df-er 8561  df-map 8680  df-pm 8681  df-ixp 8749  df-en 8797  df-dom 8798  df-sdom 8799  df-fin 8800  df-fsupp 9219  df-fi 9260  df-sup 9291  df-inf 9292  df-oi 9359  df-dju 9750  df-card 9788  df-acn 9791  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-div 11726  df-nn 12067  df-2 12129  df-3 12130  df-4 12131  df-5 12132  df-6 12133  df-7 12134  df-8 12135  df-9 12136  df-n0 12327  df-z 12413  df-dec 12531  df-uz 12676  df-q 12782  df-rp 12824  df-xneg 12941  df-xadd 12942  df-xmul 12943  df-ioo 13176  df-ioc 13177  df-ico 13178  df-icc 13179  df-fz 13333  df-fzo 13476  df-fl 13605  df-mod 13683  df-seq 13815  df-exp 13876  df-fac 14081  df-bc 14110  df-hash 14138  df-shft 14869  df-cj 14901  df-re 14902  df-im 14903  df-sqrt 15037  df-abs 15038  df-limsup 15271  df-clim 15288  df-rlim 15289  df-sum 15489  df-ef 15868  df-sin 15870  df-cos 15871  df-pi 15873  df-struct 16937  df-sets 16954  df-slot 16972  df-ndx 16984  df-base 17002  df-ress 17031  df-plusg 17064  df-mulr 17065  df-starv 17066  df-sca 17067  df-vsca 17068  df-ip 17069  df-tset 17070  df-ple 17071  df-ds 17073  df-unif 17074  df-hom 17075  df-cco 17076  df-rest 17222  df-topn 17223  df-0g 17241  df-gsum 17242  df-topgen 17243  df-pt 17244  df-prds 17247  df-xrs 17302  df-qtop 17307  df-imas 17308  df-xps 17310  df-mre 17384  df-mrc 17385  df-acs 17387  df-mgm 18415  df-sgrp 18464  df-mnd 18475  df-submnd 18520  df-mulg 18789  df-cntz 19011  df-cmn 19475  df-psmet 20687  df-xmet 20688  df-met 20689  df-bl 20690  df-mopn 20691  df-fbas 20692  df-fg 20693  df-cnfld 20696  df-top 22141  df-topon 22158  df-topsp 22180  df-bases 22194  df-cld 22268  df-ntr 22269  df-cls 22270  df-nei 22347  df-lp 22385  df-perf 22386  df-cn 22476  df-cnp 22477  df-haus 22564  df-cmp 22636  df-tx 22811  df-hmeo 23004  df-fil 23095  df-fm 23187  df-flim 23188  df-flf 23189  df-xms 23571  df-ms 23572  df-tms 23573  df-cncf 24139  df-ovol 24726  df-vol 24727  df-mbf 24881  df-itg1 24882  df-itg2 24883  df-ibl 24884  df-itg 24885  df-0p 24932  df-limc 25128  df-dv 25129
This theorem is referenced by:  wallispilem5  43935
  Copyright terms: Public domain W3C validator