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 45722
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 7421 . . . . . . 7 (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
21fveq2d 6894 . . . . . 6 (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1)))
31fvoveq1d 7435 . . . . . 6 (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) + 1)))
42, 3oveq12d 7431 . . . . 5 (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))))
5 fveq2 6890 . . . . . . 7 (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
65oveq2d 7429 . . . . . 6 (𝑥 = 1 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘1)))
76oveq2d 7429 . . . . 5 (𝑥 = 1 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))))
84, 7eqeq12d 2742 . . . 4 (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))))
9 oveq2 7421 . . . . . . 7 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
109fveq2d 6894 . . . . . 6 (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦)))
119fvoveq1d 7435 . . . . . 6 (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1)))
1210, 11oveq12d 7431 . . . . 5 (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
13 fveq2 6890 . . . . . . 7 (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦))
1413oveq2d 7429 . . . . . 6 (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦)))
1514oveq2d 7429 . . . . 5 (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))
1612, 15eqeq12d 2742 . . . 4 (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
17 oveq2 7421 . . . . . . 7 (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
1817fveq2d 6894 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1))))
1917fvoveq1d 7435 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1)))
2018, 19oveq12d 7431 . . . . 5 (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))))
21 fveq2 6890 . . . . . . 7 (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1)))
2221oveq2d 7429 . . . . . 6 (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))
2322oveq2d 7429 . . . . 5 (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
2420, 23eqeq12d 2742 . . . 4 (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
25 oveq2 7421 . . . . . . 7 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
2625fveq2d 6894 . . . . . 6 (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛)))
2725fvoveq1d 7435 . . . . . 6 (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1)))
2826, 27oveq12d 7431 . . . . 5 (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
29 fveq2 6890 . . . . . . 7 (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛))
3029oveq2d 7429 . . . . . 6 (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛)))
3130oveq2d 7429 . . . . 5 (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
3228, 31eqeq12d 2742 . . . 4 (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
33 2t1e2 12418 . . . . . . 7 (2 · 1) = 2
3433fveq2i 6893 . . . . . 6 (𝐼‘(2 · 1)) = (𝐼‘2)
3533oveq1i 7423 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
36 2p1e3 12397 . . . . . . . 8 (2 + 1) = 3
3735, 36eqtri 2754 . . . . . . 7 ((2 · 1) + 1) = 3
3837fveq2i 6893 . . . . . 6 (𝐼‘((2 · 1) + 1)) = (𝐼‘3)
3934, 38oveq12i 7425 . . . . 5 ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((𝐼‘2) / (𝐼‘3))
40 2z 12637 . . . . . . . . 9 2 ∈ ℤ
41 uzid 12880 . . . . . . . . 9 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
4240, 41ax-mp 5 . . . . . . . 8 2 ∈ (ℤ‘2)
43 wallispilem4.2 . . . . . . . . . 10 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
4443wallispilem2 45720 . . . . . . . . 9 ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (2 ∈ (ℤ‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))))
4544simp3i 1138 . . . . . . . 8 (2 ∈ (ℤ‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2))))
4642, 45ax-mp 5 . . . . . . 7 (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))
47 2m1e1 12381 . . . . . . . . 9 (2 − 1) = 1
4847oveq1i 7423 . . . . . . . 8 ((2 − 1) / 2) = (1 / 2)
49 2cn 12330 . . . . . . . . . . 11 2 ∈ ℂ
5049subidi 11569 . . . . . . . . . 10 (2 − 2) = 0
5150fveq2i 6893 . . . . . . . . 9 (𝐼‘(2 − 2)) = (𝐼‘0)
5244simp1i 1136 . . . . . . . . 9 (𝐼‘0) = π
5351, 52eqtri 2754 . . . . . . . 8 (𝐼‘(2 − 2)) = π
5448, 53oveq12i 7425 . . . . . . 7 (((2 − 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) · π)
55 ax-1cn 11204 . . . . . . . . 9 1 ∈ ℂ
56 2cnne0 12465 . . . . . . . . 9 (2 ∈ ℂ ∧ 2 ≠ 0)
57 picn 26481 . . . . . . . . 9 π ∈ ℂ
58 div32 11931 . . . . . . . . 9 ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈ ℂ) → ((1 / 2) · π) = (1 · (π / 2)))
5955, 56, 57, 58mp3an 1458 . . . . . . . 8 ((1 / 2) · π) = (1 · (π / 2))
60 2ne0 12359 . . . . . . . . . 10 2 ≠ 0
6157, 49, 60divcli 11998 . . . . . . . . 9 (π / 2) ∈ ℂ
6261mullidi 11257 . . . . . . . 8 (1 · (π / 2)) = (π / 2)
6359, 62eqtri 2754 . . . . . . 7 ((1 / 2) · π) = (π / 2)
6446, 54, 633eqtri 2758 . . . . . 6 (𝐼‘2) = (π / 2)
65 3z 12638 . . . . . . . . 9 3 ∈ ℤ
66 2re 12329 . . . . . . . . . 10 2 ∈ ℝ
67 3re 12335 . . . . . . . . . 10 3 ∈ ℝ
68 2lt3 12427 . . . . . . . . . 10 2 < 3
6966, 67, 68ltleii 11375 . . . . . . . . 9 2 ≤ 3
70 eluz2 12871 . . . . . . . . 9 (3 ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3))
7140, 65, 69, 70mpbir3an 1338 . . . . . . . 8 3 ∈ (ℤ‘2)
7243wallispilem2 45720 . . . . . . . . 9 ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (3 ∈ (ℤ‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))))
7372simp3i 1138 . . . . . . . 8 (3 ∈ (ℤ‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2))))
7471, 73ax-mp 5 . . . . . . 7 (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
75 3m1e2 12383 . . . . . . . . . 10 (3 − 1) = 2
7675eqcomi 2735 . . . . . . . . 9 2 = (3 − 1)
7776oveq1i 7423 . . . . . . . 8 (2 / 3) = ((3 − 1) / 3)
78 3cn 12336 . . . . . . . . . . 11 3 ∈ ℂ
7978, 49, 55, 36subaddrii 11587 . . . . . . . . . 10 (3 − 2) = 1
8079fveq2i 6893 . . . . . . . . 9 (𝐼‘(3 − 2)) = (𝐼‘1)
8144simp2i 1137 . . . . . . . . 9 (𝐼‘1) = 2
8280, 81eqtr2i 2755 . . . . . . . 8 2 = (𝐼‘(3 − 2))
8377, 82oveq12i 7425 . . . . . . 7 ((2 / 3) · 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
84 3ne0 12361 . . . . . . . . 9 3 ≠ 0
8549, 78, 84divcli 11998 . . . . . . . 8 (2 / 3) ∈ ℂ
8685, 49mulcomi 11260 . . . . . . 7 ((2 / 3) · 2) = (2 · (2 / 3))
8774, 83, 863eqtr2i 2760 . . . . . 6 (𝐼‘3) = (2 · (2 / 3))
8864, 87oveq12i 7425 . . . . 5 ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 / 3)))
89 1z 12635 . . . . . . . . 9 1 ∈ ℤ
90 seq1 14025 . . . . . . . . 9 (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
9189, 90ax-mp 5 . . . . . . . 8 (seq1( · , 𝐹)‘1) = (𝐹‘1)
92 1nn 12266 . . . . . . . . 9 1 ∈ ℕ
93 oveq2 7421 . . . . . . . . . . . . . 14 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
9493, 33eqtrdi 2782 . . . . . . . . . . . . 13 (𝑘 = 1 → (2 · 𝑘) = 2)
9593oveq1d 7428 . . . . . . . . . . . . . 14 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
9633oveq1i 7423 . . . . . . . . . . . . . . 15 ((2 · 1) − 1) = (2 − 1)
9796, 47eqtri 2754 . . . . . . . . . . . . . 14 ((2 · 1) − 1) = 1
9895, 97eqtrdi 2782 . . . . . . . . . . . . 13 (𝑘 = 1 → ((2 · 𝑘) − 1) = 1)
9994, 98oveq12d 7431 . . . . . . . . . . . 12 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 / 1))
10049div1i 11984 . . . . . . . . . . . 12 (2 / 1) = 2
10199, 100eqtrdi 2782 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = 2)
10294oveq1d 7428 . . . . . . . . . . . . 13 (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 + 1))
103102, 36eqtrdi 2782 . . . . . . . . . . . 12 (𝑘 = 1 → ((2 · 𝑘) + 1) = 3)
10494, 103oveq12d 7431 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 / 3))
105101, 104oveq12d 7431 . . . . . . . . . 10 (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (2 · (2 / 3)))
106 wallispilem4.1 . . . . . . . . . 10 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
107 ovex 7446 . . . . . . . . . 10 (2 · (2 / 3)) ∈ V
108105, 106, 107fvmpt 6998 . . . . . . . . 9 (1 ∈ ℕ → (𝐹‘1) = (2 · (2 / 3)))
10992, 108ax-mp 5 . . . . . . . 8 (𝐹‘1) = (2 · (2 / 3))
11091, 109eqtr2i 2755 . . . . . . 7 (2 · (2 / 3)) = (seq1( · , 𝐹)‘1)
111110oveq2i 7424 . . . . . 6 ((π / 2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1))
11249, 85mulcli 11259 . . . . . . . . 9 (2 · (2 / 3)) ∈ ℂ
113109, 112eqeltri 2822 . . . . . . . 8 (𝐹‘1) ∈ ℂ
11491, 113eqeltri 2822 . . . . . . 7 (seq1( · , 𝐹)‘1) ∈ ℂ
11549, 78, 60, 84divne0i 12004 . . . . . . . . 9 (2 / 3) ≠ 0
11649, 85, 60, 115mulne0i 11895 . . . . . . . 8 (2 · (2 / 3)) ≠ 0
117110, 116eqnetrri 3002 . . . . . . 7 (seq1( · , 𝐹)‘1) ≠ 0
11861, 114, 117divreci 12001 . . . . . 6 ((π / 2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
119111, 118eqtri 2754 . . . . 5 ((π / 2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
12039, 88, 1193eqtri 2758 . . . 4 ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
121 oveq2 7421 . . . . . . 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 480 . . . . . 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 12333 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ∈ ℂ)
124 nncn 12263 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
12555a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 1 ∈ ℂ)
126123, 124, 125adddid 11276 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
127123mulridd 11269 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · 1) = 2)
128127oveq2d 7429 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
129126, 128eqtrd 2766 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
130129oveq1d 7428 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
131123, 124mulcld 11272 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
132131, 123, 125addsubassd 11629 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
13347a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 − 1) = 1)
134133oveq2d 7429 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
135130, 132, 1343eqtrd 2770 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
136135oveq1d 7428 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) = (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))))
137136oveq1d 7428 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
13875a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (3 − 1) = 2)
139138oveq2d 7429 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 1)) = ((2 · 𝑦) + 2))
14078a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 3 ∈ ℂ)
141131, 140, 125addsubassd 11629 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = ((2 · 𝑦) + (3 − 1)))
142139, 141, 1293eqtr4d 2776 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = (2 · (𝑦 + 1)))
143142oveq1d 7428 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
144143oveq1d 7428 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
145137, 144oveq12d 7431 . . . . . . . . 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 12622 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
148147peano2zd 12712 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
149146, 148zmulcld 12715 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℤ)
15066a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℝ)
151 nnre 12262 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
152 1red 11253 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ∈ ℝ)
153151, 152readdcld 11281 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
154 0le2 12357 . . . . . . . . . . . . . . 15 0 ≤ 2
155154a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ 2)
156 nnnn0 12522 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
157156nn0ge0d 12578 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 ≤ 𝑦)
158152, 151addge02d 11841 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ 𝑦 ↔ 1 ≤ (𝑦 + 1)))
159157, 158mpbid 231 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 ≤ (𝑦 + 1))
160150, 153, 155, 159lemulge11d 12194 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ≤ (2 · (𝑦 + 1)))
16140eluz1i 12873 . . . . . . . . . . . . 13 ((2 · (𝑦 + 1)) ∈ (ℤ‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2 · (𝑦 + 1))))
162149, 160, 161sylanbrc 581 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ (ℤ‘2))
16343, 162itgsinexp 45609 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))))
164129oveq1d 7428 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (((2 · 𝑦) + 2) − 2))
165131, 123pncand 11610 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 2) = (2 · 𝑦))
166164, 165eqtrd 2766 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (2 · 𝑦))
167166fveq2d 6894 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦)))
168167oveq2d 7429 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
169163, 168eqtrd 2766 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
170129oveq1d 7428 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = (((2 · 𝑦) + 2) + 1))
171131, 123, 125addassd 11274 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) + 1) = ((2 · 𝑦) + (2 + 1)))
17236a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 + 1) = 3)
173172oveq2d 7429 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 + 1)) = ((2 · 𝑦) + 3))
174170, 171, 1733eqtrd 2770 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = ((2 · 𝑦) + 3))
175174fveq2d 6894 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3)))
176146, 147zmulcld 12715 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
17765a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 3 ∈ ℤ)
178176, 177zaddcld 12713 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℤ)
179150, 151remulcld 11282 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
18067a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 3 ∈ ℝ)
181179, 180readdcld 11281 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ)
182 nnge1 12283 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ≤ 𝑦)
183150, 151, 155, 182lemulge11d 12194 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
184 0re 11254 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
185 3pos 12360 . . . . . . . . . . . . . . . 16 0 < 3
186184, 67, 185ltleii 11375 . . . . . . . . . . . . . . 15 0 ≤ 3
187179, 180addge01d 11840 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ 3 ↔ (2 · 𝑦) ≤ ((2 · 𝑦) + 3)))
188186, 187mpbii 232 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ≤ ((2 · 𝑦) + 3))
189150, 179, 181, 183, 188letrd 11409 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ≤ ((2 · 𝑦) + 3))
19040eluz1i 12873 . . . . . . . . . . . . 13 (((2 · 𝑦) + 3) ∈ (ℤ‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2 · 𝑦) + 3)))
191178, 189, 190sylanbrc 581 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ (ℤ‘2))
19243, 191itgsinexp 45609 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
193175, 192eqtrd 2766 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
194169, 193oveq12d 7431 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
195131, 125addcld 11271 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
196124, 125addcld 11271 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
197123, 196mulcld 11272 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
19860a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ≠ 0)
199 peano2nn 12267 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
200199nnne0d 12305 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
201123, 196, 198, 200mulne0d 11904 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
202195, 197, 201divcld 12032 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ)
203 2nn0 12532 . . . . . . . . . . . . 13 2 ∈ ℕ0
204203a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ∈ ℕ0)
205204, 156nn0mulcld 12580 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ0)
20643wallispilem3 45721 . . . . . . . . . . . 12 ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℝ+)
207206rpcnd 13063 . . . . . . . . . . 11 ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℂ)
208205, 207syl 17 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
209131, 140addcld 11271 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℂ)
210 0red 11255 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ∈ ℝ)
211 2pos 12358 . . . . . . . . . . . . . . . 16 0 < 2
212211a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 < 2)
213 nngt0 12286 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 < 𝑦)
214150, 151, 212, 213mulgt0d 11407 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 < (2 · 𝑦))
215180, 185jctir 519 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (3 ∈ ℝ ∧ 0 < 3))
216 elrp 13021 . . . . . . . . . . . . . . . 16 (3 ∈ ℝ+ ↔ (3 ∈ ℝ ∧ 0 < 3))
217215, 216sylibr 233 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 3 ∈ ℝ+)
218179, 217ltaddrpd 13094 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) < ((2 · 𝑦) + 3))
219210, 179, 181, 214, 218lttrd 11413 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 < ((2 · 𝑦) + 3))
220219gt0ne0d 11816 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ≠ 0)
221197, 209, 220divcld 12032 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ)
222197, 209, 201, 220divne0d 12048 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0)
223178, 146zsubcld 12714 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℤ)
224181, 150subge0d 11842 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ (((2 · 𝑦) + 3) − 2) ↔ 2 ≤ ((2 · 𝑦) + 3)))
225189, 224mpbird 256 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ (((2 · 𝑦) + 3) − 2))
226 elnn0z 12614 . . . . . . . . . . . . . 14 ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤ (((2 · 𝑦) + 3) − 2)))
227223, 225, 226sylanbrc 581 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℕ0)
22843wallispilem3 45721 . . . . . . . . . . . . 13 ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
229227, 228syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
230229rpcnne0d 13070 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0))
231221, 222, 230jca31 513 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0)))
232 divmuldiv 11956 . . . . . . . . . 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 836 . . . . . . . . 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 2776 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))))
235131, 140, 123addsubassd 11629 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + (3 − 2)))
23679a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (3 − 2) = 1)
237236oveq2d 7429 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 2)) = ((2 · 𝑦) + 1))
238235, 237eqtrd 2766 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + 1))
239238fveq2d 6894 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1)))
240239oveq2d 7429 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
241240oveq2d 7429 . . . . . . . 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 2766 . . . . . . 7 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
243242adantr 479 . . . . . 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 12909 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ‘1))
245244biimpi 215 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘1))
246 seqp1 14027 . . . . . . . . . . . 12 (𝑦 ∈ (ℤ‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
247245, 246syl 17 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
248 oveq2 7421 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
249248oveq1d 7428 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
250248, 249oveq12d 7431 . . . . . . . . . . . . . 14 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
251248oveq1d 7428 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
252248, 251oveq12d 7431 . . . . . . . . . . . . . 14 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
253250, 252oveq12d 7431 . . . . . . . . . . . . 13 (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
254150, 153remulcld 11282 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
255254, 152resubcld 11680 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
256 1lt2 12426 . . . . . . . . . . . . . . . . . . 19 1 < 2
257256a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 1 < 2)
258 nnrp 13030 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
259152, 258ltaddrp2d 13095 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
260150, 153, 257, 259mulgt1d 12193 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
261152, 260gtned 11387 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
262197, 125, 261subne0d 11618 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
263254, 255, 262redivcld 12084 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ)
264174, 181eqeltrd 2826 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ)
265174, 220eqnetrd 2998 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
266254, 264, 265redivcld 12084 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ)
267263, 266remulcld 11282 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ)
268106, 253, 199, 267fvmptd3 7021 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
269268oveq2d 7429 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
270247, 269eqtrd 2766 . . . . . . . . . 10 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
271270oveq2d 7429 . . . . . . . . 9 (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))))
272271oveq2d 7429 . . . . . . . 8 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))))
273135oveq2d 7429 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)))
274174oveq2d 7429 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
275273, 274oveq12d 7431 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
276275oveq2d 7429 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
277276oveq2d 7429 . . . . . . . . . 10 (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
278277oveq2d 7429 . . . . . . . . 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 13575 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ)
280279adantl 480 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ)
281 oveq2 7421 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤))
282281oveq1d 7428 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1))
283281, 282oveq12d 7431 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1)))
284281oveq1d 7428 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1))
285281, 284oveq12d 7431 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1)))
286283, 285oveq12d 7431 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
287 id 22 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℕ → 𝑤 ∈ ℕ)
288 2rp 13024 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℝ+
289288a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 2 ∈ ℝ+)
290 nnrp 13030 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 𝑤 ∈ ℝ+)
291289, 290rpmulcld 13077 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ+)
29266a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 2 ∈ ℝ)
293 nnre 12262 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 𝑤 ∈ ℝ)
294292, 293remulcld 11282 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ)
295 1red 11253 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 1 ∈ ℝ)
296294, 295resubcld 11680 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ)
297 nnge1 12283 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 1 ≤ 𝑤)
298 nncn 12263 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
299298mullidd 11270 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℕ → (1 · 𝑤) = 𝑤)
300295, 292, 290ltmul1d 13102 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ ℕ → (1 < 2 ↔ (1 · 𝑤) < (2 · 𝑤)))
301256, 300mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℕ → (1 · 𝑤) < (2 · 𝑤))
302299, 301eqbrtrrd 5167 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤))
303295, 293, 294, 297, 302lelttrd 11410 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 1 < (2 · 𝑤))
304295, 294posdifd 11839 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → (1 < (2 · 𝑤) ↔ 0 < ((2 · 𝑤) − 1)))
305303, 304mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 0 < ((2 · 𝑤) − 1))
306296, 305elrpd 13058 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ+)
307291, 306rpdivcld 13078 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) − 1)) ∈ ℝ+)
308154a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 0 ≤ 2)
309290rpge0d 13065 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 0 ≤ 𝑤)
310292, 293, 308, 309mulge0d 11829 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 0 ≤ (2 · 𝑤))
311294, 310ge0p1rpd 13091 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → ((2 · 𝑤) + 1) ∈ ℝ+)
312291, 311rpdivcld 13078 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) + 1)) ∈ ℝ+)
313307, 312rpmulcld 13077 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℕ → (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))) ∈ ℝ+)
314106, 286, 287, 313fvmptd3 7021 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℕ → (𝐹𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
315314, 313eqeltrd 2826 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℕ → (𝐹𝑤) ∈ ℝ+)
316280, 315syl 17 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹𝑤) ∈ ℝ+)
317 rpmulcl 13042 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ℝ+𝑧 ∈ ℝ+) → (𝑤 · 𝑧) ∈ ℝ+)
318317adantl 480 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ+𝑧 ∈ ℝ+)) → (𝑤 · 𝑧) ∈ ℝ+)
319245, 316, 318seqcl 14033 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℝ+)
320319rpcnne0d 13070 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0))
321288a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 2 ∈ ℝ+)
322151, 157ge0p1rpd 13091 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ+)
323321, 322rpmulcld 13077 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ+)
324150, 151, 155, 157mulge0d 11829 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 0 ≤ (2 · 𝑦))
325179, 324ge0p1rpd 13091 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ+)
326323, 325rpdivcld 13078 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) ∈ ℝ+)
327321, 258rpmulcld 13077 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ+)
328327, 217rpaddcld 13076 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ+)
329323, 328rpdivcld 13078 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℝ+)
330326, 329rpmulcld 13077 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℝ+)
331330rpcnne0d 13070 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0))
332 divdiv1 11967 . . . . . . . . . . . . 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 1368 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
334333eqcomd 2732 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
335334oveq2d 7429 . . . . . . . . . 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 13063 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℂ)
338319rpne0d 13066 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ≠ 0)
339337, 338reccld 12025 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑦)) ∈ ℂ)
340330rpcnd 13063 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
341330rpne0d 13066 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)
342336, 339, 340, 341divassd 12067 . . . . . . . . . 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 2999 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
344197, 195, 197, 209, 343, 220divmuldivd 12073 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))))
345344oveq2d 7429 . . . . . . . . . . 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 11272 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
347197, 197mulcld 11272 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
348195, 209mulcld 11272 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ∈ ℂ)
349197, 197, 201, 201mulne0d 11904 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ≠ 0)
350195, 209, 343, 220mulne0d 11904 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ≠ 0)
351346, 347, 348, 349, 350divdiv2d 12064 . . . . . . . . . . . 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 12067 . . . . . . . . . . . 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 2766 . . . . . . . . . . 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 12079 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
355354eqcomd 2732 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
356355oveq2d 7429 . . . . . . . . . . 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 2770 . . . . . . . . . 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 2772 . . . . . . . . 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 12500 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
361360, 339mulcld 11272 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
362202, 221, 222divcld 12032 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
363361, 362mulcomd 11273 . . . . . . . . 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 2770 . . . . . . . 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 2766 . . . . . . 7 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
366365adantr 479 . . . . . 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 2776 . . . . 5 ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
368367ex 411 . . . 4 (𝑦 ∈ ℕ → (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
3698, 16, 24, 32, 120, 368nnind 12273 . . 3 (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
370369mpteq2ia 5246 . 2 (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
371 wallispilem4.3 . 2 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
372 wallispilem4.4 . 2 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
373370, 371, 3723eqtr4i 2764 1 𝐺 = 𝐻
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  wcel 2099  wne 2930   class class class wbr 5143  cmpt 5226  cfv 6543  (class class class)co 7413  cc 11144  cr 11145  0cc0 11146  1c1 11147   + caddc 11149   · cmul 11151   < clt 11286  cle 11287  cmin 11482   / cdiv 11909  cn 12255  2c2 12310  3c3 12311  0cn0 12515  cz 12601  cuz 12865  +crp 13019  (,)cioo 13369  ...cfz 13529  seqcseq 14012  cexp 14072  sincsin 16057  πcpi 16060  citg 25632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7735  ax-inf2 9674  ax-cc 10466  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224  ax-addf 11225
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-symdif 4241  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6302  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-ofr 7680  df-om 7866  df-1st 7992  df-2nd 7993  df-supp 8164  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-oadd 8489  df-omul 8490  df-er 8723  df-map 8846  df-pm 8847  df-ixp 8916  df-en 8964  df-dom 8965  df-sdom 8966  df-fin 8967  df-fsupp 9396  df-fi 9444  df-sup 9475  df-inf 9476  df-oi 9543  df-dju 9934  df-card 9972  df-acn 9975  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12256  df-2 12318  df-3 12319  df-4 12320  df-5 12321  df-6 12322  df-7 12323  df-8 12324  df-9 12325  df-n0 12516  df-z 12602  df-dec 12721  df-uz 12866  df-q 12976  df-rp 13020  df-xneg 13137  df-xadd 13138  df-xmul 13139  df-ioo 13373  df-ioc 13374  df-ico 13375  df-icc 13376  df-fz 13530  df-fzo 13673  df-fl 13803  df-mod 13881  df-seq 14013  df-exp 14073  df-fac 14283  df-bc 14312  df-hash 14340  df-shft 15064  df-cj 15096  df-re 15097  df-im 15098  df-sqrt 15232  df-abs 15233  df-limsup 15465  df-clim 15482  df-rlim 15483  df-sum 15683  df-ef 16061  df-sin 16063  df-cos 16064  df-pi 16066  df-struct 17141  df-sets 17158  df-slot 17176  df-ndx 17188  df-base 17206  df-ress 17235  df-plusg 17271  df-mulr 17272  df-starv 17273  df-sca 17274  df-vsca 17275  df-ip 17276  df-tset 17277  df-ple 17278  df-ds 17280  df-unif 17281  df-hom 17282  df-cco 17283  df-rest 17429  df-topn 17430  df-0g 17448  df-gsum 17449  df-topgen 17450  df-pt 17451  df-prds 17454  df-xrs 17509  df-qtop 17514  df-imas 17515  df-xps 17517  df-mre 17591  df-mrc 17592  df-acs 17594  df-mgm 18625  df-sgrp 18704  df-mnd 18720  df-submnd 18766  df-mulg 19055  df-cntz 19304  df-cmn 19773  df-psmet 21328  df-xmet 21329  df-met 21330  df-bl 21331  df-mopn 21332  df-fbas 21333  df-fg 21334  df-cnfld 21337  df-top 22881  df-topon 22898  df-topsp 22920  df-bases 22934  df-cld 23008  df-ntr 23009  df-cls 23010  df-nei 23087  df-lp 23125  df-perf 23126  df-cn 23216  df-cnp 23217  df-haus 23304  df-cmp 23376  df-tx 23551  df-hmeo 23744  df-fil 23835  df-fm 23927  df-flim 23928  df-flf 23929  df-xms 24311  df-ms 24312  df-tms 24313  df-cncf 24883  df-ovol 25478  df-vol 25479  df-mbf 25633  df-itg1 25634  df-itg2 25635  df-ibl 25636  df-itg 25637  df-0p 25684  df-limc 25880  df-dv 25881
This theorem is referenced by:  wallispilem5  45723
  Copyright terms: Public domain W3C validator