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 42708
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 7143 . . . . . . 7 (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
21fveq2d 6649 . . . . . 6 (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1)))
31fvoveq1d 7157 . . . . . 6 (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) + 1)))
42, 3oveq12d 7153 . . . . 5 (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))))
5 fveq2 6645 . . . . . . 7 (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
65oveq2d 7151 . . . . . 6 (𝑥 = 1 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘1)))
76oveq2d 7151 . . . . 5 (𝑥 = 1 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))))
84, 7eqeq12d 2814 . . . 4 (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))))
9 oveq2 7143 . . . . . . 7 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
109fveq2d 6649 . . . . . 6 (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦)))
119fvoveq1d 7157 . . . . . 6 (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1)))
1210, 11oveq12d 7153 . . . . 5 (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
13 fveq2 6645 . . . . . . 7 (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦))
1413oveq2d 7151 . . . . . 6 (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦)))
1514oveq2d 7151 . . . . 5 (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))
1612, 15eqeq12d 2814 . . . 4 (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
17 oveq2 7143 . . . . . . 7 (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
1817fveq2d 6649 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1))))
1917fvoveq1d 7157 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1)))
2018, 19oveq12d 7153 . . . . 5 (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))))
21 fveq2 6645 . . . . . . 7 (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1)))
2221oveq2d 7151 . . . . . 6 (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))
2322oveq2d 7151 . . . . 5 (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
2420, 23eqeq12d 2814 . . . 4 (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
25 oveq2 7143 . . . . . . 7 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
2625fveq2d 6649 . . . . . 6 (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛)))
2725fvoveq1d 7157 . . . . . 6 (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1)))
2826, 27oveq12d 7153 . . . . 5 (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
29 fveq2 6645 . . . . . . 7 (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛))
3029oveq2d 7151 . . . . . 6 (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛)))
3130oveq2d 7151 . . . . 5 (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
3228, 31eqeq12d 2814 . . . 4 (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
33 2t1e2 11788 . . . . . . 7 (2 · 1) = 2
3433fveq2i 6648 . . . . . 6 (𝐼‘(2 · 1)) = (𝐼‘2)
3533oveq1i 7145 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
36 2p1e3 11767 . . . . . . . 8 (2 + 1) = 3
3735, 36eqtri 2821 . . . . . . 7 ((2 · 1) + 1) = 3
3837fveq2i 6648 . . . . . 6 (𝐼‘((2 · 1) + 1)) = (𝐼‘3)
3934, 38oveq12i 7147 . . . . 5 ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((𝐼‘2) / (𝐼‘3))
40 2z 12002 . . . . . . . . 9 2 ∈ ℤ
41 uzid 12246 . . . . . . . . 9 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
4240, 41ax-mp 5 . . . . . . . 8 2 ∈ (ℤ‘2)
43 wallispilem4.2 . . . . . . . . . 10 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
4443wallispilem2 42706 . . . . . . . . 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 11751 . . . . . . . . 9 (2 − 1) = 1
4847oveq1i 7145 . . . . . . . 8 ((2 − 1) / 2) = (1 / 2)
49 2cn 11700 . . . . . . . . . . 11 2 ∈ ℂ
5049subidi 10946 . . . . . . . . . 10 (2 − 2) = 0
5150fveq2i 6648 . . . . . . . . 9 (𝐼‘(2 − 2)) = (𝐼‘0)
5244simp1i 1136 . . . . . . . . 9 (𝐼‘0) = π
5351, 52eqtri 2821 . . . . . . . 8 (𝐼‘(2 − 2)) = π
5448, 53oveq12i 7147 . . . . . . 7 (((2 − 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) · π)
55 ax-1cn 10584 . . . . . . . . 9 1 ∈ ℂ
56 2cnne0 11835 . . . . . . . . 9 (2 ∈ ℂ ∧ 2 ≠ 0)
57 picn 25052 . . . . . . . . 9 π ∈ ℂ
58 div32 11307 . . . . . . . . 9 ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈ ℂ) → ((1 / 2) · π) = (1 · (π / 2)))
5955, 56, 57, 58mp3an 1458 . . . . . . . 8 ((1 / 2) · π) = (1 · (π / 2))
60 2ne0 11729 . . . . . . . . . 10 2 ≠ 0
6157, 49, 60divcli 11371 . . . . . . . . 9 (π / 2) ∈ ℂ
6261mulid2i 10635 . . . . . . . 8 (1 · (π / 2)) = (π / 2)
6359, 62eqtri 2821 . . . . . . 7 ((1 / 2) · π) = (π / 2)
6446, 54, 633eqtri 2825 . . . . . 6 (𝐼‘2) = (π / 2)
65 3z 12003 . . . . . . . . 9 3 ∈ ℤ
66 2re 11699 . . . . . . . . . 10 2 ∈ ℝ
67 3re 11705 . . . . . . . . . 10 3 ∈ ℝ
68 2lt3 11797 . . . . . . . . . 10 2 < 3
6966, 67, 68ltleii 10752 . . . . . . . . 9 2 ≤ 3
70 eluz2 12237 . . . . . . . . 9 (3 ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3))
7140, 65, 69, 70mpbir3an 1338 . . . . . . . 8 3 ∈ (ℤ‘2)
7243wallispilem2 42706 . . . . . . . . 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 11753 . . . . . . . . . 10 (3 − 1) = 2
7675eqcomi 2807 . . . . . . . . 9 2 = (3 − 1)
7776oveq1i 7145 . . . . . . . 8 (2 / 3) = ((3 − 1) / 3)
78 3cn 11706 . . . . . . . . . . 11 3 ∈ ℂ
7978, 49, 55, 36subaddrii 10964 . . . . . . . . . 10 (3 − 2) = 1
8079fveq2i 6648 . . . . . . . . 9 (𝐼‘(3 − 2)) = (𝐼‘1)
8144simp2i 1137 . . . . . . . . 9 (𝐼‘1) = 2
8280, 81eqtr2i 2822 . . . . . . . 8 2 = (𝐼‘(3 − 2))
8377, 82oveq12i 7147 . . . . . . 7 ((2 / 3) · 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
84 3ne0 11731 . . . . . . . . 9 3 ≠ 0
8549, 78, 84divcli 11371 . . . . . . . 8 (2 / 3) ∈ ℂ
8685, 49mulcomi 10638 . . . . . . 7 ((2 / 3) · 2) = (2 · (2 / 3))
8774, 83, 863eqtr2i 2827 . . . . . 6 (𝐼‘3) = (2 · (2 / 3))
8864, 87oveq12i 7147 . . . . 5 ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 / 3)))
89 1z 12000 . . . . . . . . 9 1 ∈ ℤ
90 seq1 13377 . . . . . . . . 9 (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
9189, 90ax-mp 5 . . . . . . . 8 (seq1( · , 𝐹)‘1) = (𝐹‘1)
92 1nn 11636 . . . . . . . . 9 1 ∈ ℕ
93 oveq2 7143 . . . . . . . . . . . . . 14 (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
9493, 33eqtrdi 2849 . . . . . . . . . . . . 13 (𝑘 = 1 → (2 · 𝑘) = 2)
9593oveq1d 7150 . . . . . . . . . . . . . 14 (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
9633oveq1i 7145 . . . . . . . . . . . . . . 15 ((2 · 1) − 1) = (2 − 1)
9796, 47eqtri 2821 . . . . . . . . . . . . . 14 ((2 · 1) − 1) = 1
9895, 97eqtrdi 2849 . . . . . . . . . . . . 13 (𝑘 = 1 → ((2 · 𝑘) − 1) = 1)
9994, 98oveq12d 7153 . . . . . . . . . . . 12 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 / 1))
10049div1i 11357 . . . . . . . . . . . 12 (2 / 1) = 2
10199, 100eqtrdi 2849 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = 2)
10294oveq1d 7150 . . . . . . . . . . . . 13 (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 + 1))
103102, 36eqtrdi 2849 . . . . . . . . . . . 12 (𝑘 = 1 → ((2 · 𝑘) + 1) = 3)
10494, 103oveq12d 7153 . . . . . . . . . . 11 (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 / 3))
105101, 104oveq12d 7153 . . . . . . . . . 10 (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (2 · (2 / 3)))
106 wallispilem4.1 . . . . . . . . . 10 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
107 ovex 7168 . . . . . . . . . 10 (2 · (2 / 3)) ∈ V
108105, 106, 107fvmpt 6745 . . . . . . . . 9 (1 ∈ ℕ → (𝐹‘1) = (2 · (2 / 3)))
10992, 108ax-mp 5 . . . . . . . 8 (𝐹‘1) = (2 · (2 / 3))
11091, 109eqtr2i 2822 . . . . . . 7 (2 · (2 / 3)) = (seq1( · , 𝐹)‘1)
111110oveq2i 7146 . . . . . 6 ((π / 2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1))
11249, 85mulcli 10637 . . . . . . . . 9 (2 · (2 / 3)) ∈ ℂ
113109, 112eqeltri 2886 . . . . . . . 8 (𝐹‘1) ∈ ℂ
11491, 113eqeltri 2886 . . . . . . 7 (seq1( · , 𝐹)‘1) ∈ ℂ
11549, 78, 60, 84divne0i 11377 . . . . . . . . 9 (2 / 3) ≠ 0
11649, 85, 60, 115mulne0i 11272 . . . . . . . 8 (2 · (2 / 3)) ≠ 0
117110, 116eqnetrri 3058 . . . . . . 7 (seq1( · , 𝐹)‘1) ≠ 0
11861, 114, 117divreci 11374 . . . . . 6 ((π / 2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
119111, 118eqtri 2821 . . . . 5 ((π / 2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
12039, 88, 1193eqtri 2825 . . . 4 ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
121 oveq2 7143 . . . . . . 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 485 . . . . . 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 11703 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 2 ∈ ℂ)
124 nncn 11633 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
12555a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 1 ∈ ℂ)
126123, 124, 125adddid 10654 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
127123mulid1d 10647 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · 1) = 2)
128127oveq2d 7151 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
129126, 128eqtrd 2833 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
130129oveq1d 7150 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
131123, 124mulcld 10650 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
132131, 123, 125addsubassd 11006 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
13347a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 − 1) = 1)
134133oveq2d 7151 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
135130, 132, 1343eqtrd 2837 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
136135oveq1d 7150 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) = (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))))
137136oveq1d 7150 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
13875a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (3 − 1) = 2)
139138oveq2d 7151 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 1)) = ((2 · 𝑦) + 2))
14078a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 3 ∈ ℂ)
141131, 140, 125addsubassd 11006 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = ((2 · 𝑦) + (3 − 1)))
142139, 141, 1293eqtr4d 2843 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = (2 · (𝑦 + 1)))
143142oveq1d 7150 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
144143oveq1d 7150 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
145137, 144oveq12d 7153 . . . . . . . . 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 11992 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
148147peano2zd 12078 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
149146, 148zmulcld 12081 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℤ)
15066a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ∈ ℝ)
151 nnre 11632 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
152 1red 10631 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ∈ ℝ)
153151, 152readdcld 10659 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
154 0le2 11727 . . . . . . . . . . . . . . 15 0 ≤ 2
155154a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ 2)
156 nnnn0 11892 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
157156nn0ge0d 11946 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 ≤ 𝑦)
158152, 151addge02d 11218 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ 𝑦 ↔ 1 ≤ (𝑦 + 1)))
159157, 158mpbid 235 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 ≤ (𝑦 + 1))
160150, 153, 155, 159lemulge11d 11566 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ≤ (2 · (𝑦 + 1)))
16140eluz1i 12239 . . . . . . . . . . . . 13 ((2 · (𝑦 + 1)) ∈ (ℤ‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2 · (𝑦 + 1))))
162149, 160, 161sylanbrc 586 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ (ℤ‘2))
16343, 162itgsinexp 42595 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))))
164129oveq1d 7150 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (((2 · 𝑦) + 2) − 2))
165131, 123pncand 10987 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 2) = (2 · 𝑦))
166164, 165eqtrd 2833 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (2 · 𝑦))
167166fveq2d 6649 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦)))
168167oveq2d 7151 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
169163, 168eqtrd 2833 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
170129oveq1d 7150 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = (((2 · 𝑦) + 2) + 1))
171131, 123, 125addassd 10652 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) + 1) = ((2 · 𝑦) + (2 + 1)))
17236a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 + 1) = 3)
173172oveq2d 7151 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 + 1)) = ((2 · 𝑦) + 3))
174170, 171, 1733eqtrd 2837 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = ((2 · 𝑦) + 3))
175174fveq2d 6649 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3)))
176146, 147zmulcld 12081 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
17765a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 3 ∈ ℤ)
178176, 177zaddcld 12079 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℤ)
179150, 151remulcld 10660 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
18067a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 3 ∈ ℝ)
181179, 180readdcld 10659 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ)
182 nnge1 11653 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 1 ≤ 𝑦)
183150, 151, 155, 182lemulge11d 11566 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
184 0re 10632 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
185 3pos 11730 . . . . . . . . . . . . . . . 16 0 < 3
186184, 67, 185ltleii 10752 . . . . . . . . . . . . . . 15 0 ≤ 3
187179, 180addge01d 11217 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ 3 ↔ (2 · 𝑦) ≤ ((2 · 𝑦) + 3)))
188186, 187mpbii 236 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) ≤ ((2 · 𝑦) + 3))
189150, 179, 181, 183, 188letrd 10786 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 2 ≤ ((2 · 𝑦) + 3))
19040eluz1i 12239 . . . . . . . . . . . . 13 (((2 · 𝑦) + 3) ∈ (ℤ‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2 · 𝑦) + 3)))
191178, 189, 190sylanbrc 586 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ (ℤ‘2))
19243, 191itgsinexp 42595 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
193175, 192eqtrd 2833 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
194169, 193oveq12d 7153 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
195131, 125addcld 10649 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
196124, 125addcld 10649 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
197123, 196mulcld 10650 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
19860a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ≠ 0)
199 peano2nn 11637 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
200199nnne0d 11675 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
201123, 196, 198, 200mulne0d 11281 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
202195, 197, 201divcld 11405 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ)
203 2nn0 11902 . . . . . . . . . . . . 13 2 ∈ ℕ0
204203a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ∈ ℕ0)
205204, 156nn0mulcld 11948 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ0)
20643wallispilem3 42707 . . . . . . . . . . . 12 ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℝ+)
207206rpcnd 12421 . . . . . . . . . . 11 ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℂ)
208205, 207syl 17 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
209131, 140addcld 10649 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℂ)
210 0red 10633 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ∈ ℝ)
211 2pos 11728 . . . . . . . . . . . . . . . 16 0 < 2
212211a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 < 2)
213 nngt0 11656 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 0 < 𝑦)
214150, 151, 212, 213mulgt0d 10784 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 < (2 · 𝑦))
215180, 185jctir 524 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (3 ∈ ℝ ∧ 0 < 3))
216 elrp 12379 . . . . . . . . . . . . . . . 16 (3 ∈ ℝ+ ↔ (3 ∈ ℝ ∧ 0 < 3))
217215, 216sylibr 237 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 3 ∈ ℝ+)
218179, 217ltaddrpd 12452 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (2 · 𝑦) < ((2 · 𝑦) + 3))
219210, 179, 181, 214, 218lttrd 10790 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 0 < ((2 · 𝑦) + 3))
220219gt0ne0d 11193 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ≠ 0)
221197, 209, 220divcld 11405 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ)
222197, 209, 201, 220divne0d 11421 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0)
223178, 146zsubcld 12080 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℤ)
224181, 150subge0d 11219 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (0 ≤ (((2 · 𝑦) + 3) − 2) ↔ 2 ≤ ((2 · 𝑦) + 3)))
225189, 224mpbird 260 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 0 ≤ (((2 · 𝑦) + 3) − 2))
226 elnn0z 11982 . . . . . . . . . . . . . 14 ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤ (((2 · 𝑦) + 3) − 2)))
227223, 225, 226sylanbrc 586 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℕ0)
22843wallispilem3 42707 . . . . . . . . . . . . 13 ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
229227, 228syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
230229rpcnne0d 12428 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0))
231221, 222, 230jca31 518 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0)))
232 divmuldiv 11329 . . . . . . . . . 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 2843 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))))
235131, 140, 123addsubassd 11006 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + (3 − 2)))
23679a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (3 − 2) = 1)
237236oveq2d 7151 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 2)) = ((2 · 𝑦) + 1))
238235, 237eqtrd 2833 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + 1))
239238fveq2d 6649 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1)))
240239oveq2d 7151 . . . . . . . . 9 (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
241240oveq2d 7151 . . . . . . . 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 2833 . . . . . . 7 (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
243242adantr 484 . . . . . 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 12270 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ‘1))
245244biimpi 219 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ‘1))
246 seqp1 13379 . . . . . . . . . . . 12 (𝑦 ∈ (ℤ‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
247245, 246syl 17 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
248 oveq2 7143 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
249248oveq1d 7150 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
250248, 249oveq12d 7153 . . . . . . . . . . . . . 14 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
251248oveq1d 7150 . . . . . . . . . . . . . . 15 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
252248, 251oveq12d 7153 . . . . . . . . . . . . . 14 (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
253250, 252oveq12d 7153 . . . . . . . . . . . . 13 (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
254150, 153remulcld 10660 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
255254, 152resubcld 11057 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
256 1lt2 11796 . . . . . . . . . . . . . . . . . . 19 1 < 2
257256a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 1 < 2)
258 nnrp 12388 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
259152, 258ltaddrp2d 12453 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
260150, 153, 257, 259mulgt1d 11565 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
261152, 260gtned 10764 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
262197, 125, 261subne0d 10995 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
263254, 255, 262redivcld 11457 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ)
264174, 181eqeltrd 2890 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ)
265174, 220eqnetrd 3054 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
266254, 264, 265redivcld 11457 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ)
267263, 266remulcld 10660 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ)
268106, 253, 199, 267fvmptd3 6768 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
269268oveq2d 7151 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
270247, 269eqtrd 2833 . . . . . . . . . 10 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
271270oveq2d 7151 . . . . . . . . 9 (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))))
272271oveq2d 7151 . . . . . . . 8 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))))
273135oveq2d 7151 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)))
274174oveq2d 7151 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
275273, 274oveq12d 7153 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
276275oveq2d 7151 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
277276oveq2d 7151 . . . . . . . . . 10 (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
278277oveq2d 7151 . . . . . . . . 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 12931 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ)
280279adantl 485 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ)
281 oveq2 7143 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤))
282281oveq1d 7150 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1))
283281, 282oveq12d 7153 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1)))
284281oveq1d 7150 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1))
285281, 284oveq12d 7153 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1)))
286283, 285oveq12d 7153 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
287 id 22 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℕ → 𝑤 ∈ ℕ)
288 2rp 12382 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℝ+
289288a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 2 ∈ ℝ+)
290 nnrp 12388 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 𝑤 ∈ ℝ+)
291289, 290rpmulcld 12435 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ+)
29266a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 2 ∈ ℝ)
293 nnre 11632 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 𝑤 ∈ ℝ)
294292, 293remulcld 10660 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ)
295 1red 10631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 1 ∈ ℝ)
296294, 295resubcld 11057 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ)
297 nnge1 11653 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 1 ≤ 𝑤)
298 nncn 11633 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
299298mulid2d 10648 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℕ → (1 · 𝑤) = 𝑤)
300295, 292, 290ltmul1d 12460 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ ℕ → (1 < 2 ↔ (1 · 𝑤) < (2 · 𝑤)))
301256, 300mpbii 236 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℕ → (1 · 𝑤) < (2 · 𝑤))
302299, 301eqbrtrrd 5054 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤))
303295, 293, 294, 297, 302lelttrd 10787 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 1 < (2 · 𝑤))
304295, 294posdifd 11216 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → (1 < (2 · 𝑤) ↔ 0 < ((2 · 𝑤) − 1)))
305303, 304mpbid 235 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 0 < ((2 · 𝑤) − 1))
306296, 305elrpd 12416 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ+)
307291, 306rpdivcld 12436 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) − 1)) ∈ ℝ+)
308154a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 0 ≤ 2)
309290rpge0d 12423 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℕ → 0 ≤ 𝑤)
310292, 293, 308, 309mulge0d 11206 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℕ → 0 ≤ (2 · 𝑤))
311294, 310ge0p1rpd 12449 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℕ → ((2 · 𝑤) + 1) ∈ ℝ+)
312291, 311rpdivcld 12436 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) + 1)) ∈ ℝ+)
313307, 312rpmulcld 12435 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℕ → (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))) ∈ ℝ+)
314106, 286, 287, 313fvmptd3 6768 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℕ → (𝐹𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
315314, 313eqeltrd 2890 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℕ → (𝐹𝑤) ∈ ℝ+)
316280, 315syl 17 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹𝑤) ∈ ℝ+)
317 rpmulcl 12400 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ℝ+𝑧 ∈ ℝ+) → (𝑤 · 𝑧) ∈ ℝ+)
318317adantl 485 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ+𝑧 ∈ ℝ+)) → (𝑤 · 𝑧) ∈ ℝ+)
319245, 316, 318seqcl 13386 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℝ+)
320319rpcnne0d 12428 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0))
321288a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 2 ∈ ℝ+)
322151, 157ge0p1rpd 12449 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ+)
323321, 322rpmulcld 12435 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ+)
324150, 151, 155, 157mulge0d 11206 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → 0 ≤ (2 · 𝑦))
325179, 324ge0p1rpd 12449 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ+)
326323, 325rpdivcld 12436 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) ∈ ℝ+)
327321, 258rpmulcld 12435 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ+)
328327, 217rpaddcld 12434 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ+)
329323, 328rpdivcld 12436 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℝ+)
330326, 329rpmulcld 12435 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℝ+)
331330rpcnne0d 12428 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0))
332 divdiv1 11340 . . . . . . . . . . . . 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 2804 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
335334oveq2d 7151 . . . . . . . . . 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 12421 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℂ)
338319rpne0d 12424 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ≠ 0)
339337, 338reccld 11398 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑦)) ∈ ℂ)
340330rpcnd 12421 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
341330rpne0d 12424 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)
342336, 339, 340, 341divassd 11440 . . . . . . . . . 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 3055 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
344197, 195, 197, 209, 343, 220divmuldivd 11446 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))))
345344oveq2d 7151 . . . . . . . . . . 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 10650 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
347197, 197mulcld 10650 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
348195, 209mulcld 10650 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ∈ ℂ)
349197, 197, 201, 201mulne0d 11281 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ≠ 0)
350195, 209, 343, 220mulne0d 11281 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ≠ 0)
351346, 347, 348, 349, 350divdiv2d 11437 . . . . . . . . . . . 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 11440 . . . . . . . . . . . 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 2833 . . . . . . . . . . 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 11452 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
355354eqcomd 2804 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
356355oveq2d 7151 . . . . . . . . . . 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 2837 . . . . . . . . . 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 2839 . . . . . . . . 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 11870 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
361360, 339mulcld 10650 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
362202, 221, 222divcld 11405 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
363361, 362mulcomd 10651 . . . . . . . . 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 2837 . . . . . . . 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 2833 . . . . . . 7 (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
366365adantr 484 . . . . . 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 2843 . . . . 5 ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
368367ex 416 . . . 4 (𝑦 ∈ ℕ → (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
3698, 16, 24, 32, 120, 368nnind 11643 . . 3 (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
370369mpteq2ia 5121 . 2 (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
371 wallispilem4.3 . 2 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
372 wallispilem4.4 . 2 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
373370, 371, 3723eqtr4i 2831 1 𝐺 = 𝐻
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2111  wne 2987   class class class wbr 5030  cmpt 5110  cfv 6324  (class class class)co 7135  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531   < clt 10664  cle 10665  cmin 10859   / cdiv 11286  cn 11625  2c2 11680  3c3 11681  0cn0 11885  cz 11969  cuz 12231  +crp 12377  (,)cioo 12726  ...cfz 12885  seqcseq 13364  cexp 13425  sincsin 15409  πcpi 15412  citg 24222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-cc 9846  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-symdif 4169  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-disj 4996  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-ofr 7390  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-omul 8090  df-er 8272  df-map 8391  df-pm 8392  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-fi 8859  df-sup 8890  df-inf 8891  df-oi 8958  df-dju 9314  df-card 9352  df-acn 9355  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426  df-fac 13630  df-bc 13659  df-hash 13687  df-shft 14418  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-limsup 14820  df-clim 14837  df-rlim 14838  df-sum 15035  df-ef 15413  df-sin 15415  df-cos 15416  df-pi 15418  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-mulg 18217  df-cntz 18439  df-cmn 18900  df-psmet 20083  df-xmet 20084  df-met 20085  df-bl 20086  df-mopn 20087  df-fbas 20088  df-fg 20089  df-cnfld 20092  df-top 21499  df-topon 21516  df-topsp 21538  df-bases 21551  df-cld 21624  df-ntr 21625  df-cls 21626  df-nei 21703  df-lp 21741  df-perf 21742  df-cn 21832  df-cnp 21833  df-haus 21920  df-cmp 21992  df-tx 22167  df-hmeo 22360  df-fil 22451  df-fm 22543  df-flim 22544  df-flf 22545  df-xms 22927  df-ms 22928  df-tms 22929  df-cncf 23483  df-ovol 24068  df-vol 24069  df-mbf 24223  df-itg1 24224  df-itg2 24225  df-ibl 24226  df-itg 24227  df-0p 24274  df-limc 24469  df-dv 24470
This theorem is referenced by:  wallispilem5  42709
  Copyright terms: Public domain W3C validator