Metamath Proof Explorer

Theorem wallispilem4

Description: F maps to explicit expression for the ratio of two consecutive values of I . (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Hypotheses wallispilem4.1 ⊢ 𝐹 = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
wallispilem4.2 ⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑧 ) ↑ 𝑛 ) d 𝑧 )
wallispilem4.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) )
wallispilem4.4 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) ) ) )
Assertion wallispilem4 𝐺 = 𝐻

Proof

Step Hyp Ref Expression
1 wallispilem4.1 ⊢ 𝐹 = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
2 wallispilem4.2 ⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑧 ) ↑ 𝑛 ) d 𝑧 )
3 wallispilem4.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) )
4 wallispilem4.4 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) ) ) )
5 oveq2 ⊢ ( 𝑥 = 1 → ( 2 · 𝑥 ) = ( 2 · 1 ) )
6 5 fveq2d ⊢ ( 𝑥 = 1 → ( 𝐼 ‘ ( 2 · 𝑥 ) ) = ( 𝐼 ‘ ( 2 · 1 ) ) )
7 5 fvoveq1d ⊢ ( 𝑥 = 1 → ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) = ( 𝐼 ‘ ( ( 2 · 1 ) + 1 ) ) )
8 6 7 oveq12d ⊢ ( 𝑥 = 1 → ( ( 𝐼 ‘ ( 2 · 𝑥 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) ) = ( ( 𝐼 ‘ ( 2 · 1 ) ) / ( 𝐼 ‘ ( ( 2 · 1 ) + 1 ) ) ) )
9 fveq2 ⊢ ( 𝑥 = 1 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 1 ) )
10 9 oveq2d ⊢ ( 𝑥 = 1 → ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) )
11 10 oveq2d ⊢ ( 𝑥 = 1 → ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) ) )
12 8 11 eqeq12d ⊢ ( 𝑥 = 1 → ( ( ( 𝐼 ‘ ( 2 · 𝑥 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( ( 𝐼 ‘ ( 2 · 1 ) ) / ( 𝐼 ‘ ( ( 2 · 1 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) ) ) )
13 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
14 13 fveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐼 ‘ ( 2 · 𝑥 ) ) = ( 𝐼 ‘ ( 2 · 𝑦 ) ) )
15 13 fvoveq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) = ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) )
16 14 15 oveq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐼 ‘ ( 2 · 𝑥 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) ) = ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) )
17 fveq2 ⊢ ( 𝑥 = 𝑦 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) )
18 17 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) )
19 18 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) )
20 16 19 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐼 ‘ ( 2 · 𝑥 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) )
21 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 2 · 𝑥 ) = ( 2 · ( 𝑦 + 1 ) ) )
22 21 fveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐼 ‘ ( 2 · 𝑥 ) ) = ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) )
23 21 fvoveq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) = ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) )
24 22 23 oveq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐼 ‘ ( 2 · 𝑥 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) ) = ( ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) )
25 fveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) )
26 25 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( 1 / ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) ) )
27 26 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) ) ) )
28 24 27 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝐼 ‘ ( 2 · 𝑥 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) ) ) ) )
29 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 2 · 𝑥 ) = ( 2 · 𝑛 ) )
30 29 fveq2d ⊢ ( 𝑥 = 𝑛 → ( 𝐼 ‘ ( 2 · 𝑥 ) ) = ( 𝐼 ‘ ( 2 · 𝑛 ) ) )
31 29 fvoveq1d ⊢ ( 𝑥 = 𝑛 → ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) = ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) )
32 30 31 oveq12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝐼 ‘ ( 2 · 𝑥 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) ) = ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) )
33 fveq2 ⊢ ( 𝑥 = 𝑛 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) )
34 33 oveq2d ⊢ ( 𝑥 = 𝑛 → ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) = ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) ) )
35 34 oveq2d ⊢ ( 𝑥 = 𝑛 → ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) ) ) )
36 32 35 eqeq12d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝐼 ‘ ( 2 · 𝑥 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑥 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) ) ) ) )
37 2t1e2 ⊢ ( 2 · 1 ) = 2
38 37 fveq2i ⊢ ( 𝐼 ‘ ( 2 · 1 ) ) = ( 𝐼 ‘ 2 )
39 37 oveq1i ⊢ ( ( 2 · 1 ) + 1 ) = ( 2 + 1 )
40 2p1e3 ⊢ ( 2 + 1 ) = 3
41 39 40 eqtri ⊢ ( ( 2 · 1 ) + 1 ) = 3
42 41 fveq2i ⊢ ( 𝐼 ‘ ( ( 2 · 1 ) + 1 ) ) = ( 𝐼 ‘ 3 )
43 38 42 oveq12i ⊢ ( ( 𝐼 ‘ ( 2 · 1 ) ) / ( 𝐼 ‘ ( ( 2 · 1 ) + 1 ) ) ) = ( ( 𝐼 ‘ 2 ) / ( 𝐼 ‘ 3 ) )
44 2z ⊢ 2 ∈ ℤ
45 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
46 44 45 ax-mp ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
47 2 wallispilem2 ⊢ ( ( 𝐼 ‘ 0 ) = π ∧ ( 𝐼 ‘ 1 ) = 2 ∧ ( 2 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 2 ) = ( ( ( 2 − 1 ) / 2 ) · ( 𝐼 ‘ ( 2 − 2 ) ) ) ) )
48 47 simp3i ⊢ ( 2 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 2 ) = ( ( ( 2 − 1 ) / 2 ) · ( 𝐼 ‘ ( 2 − 2 ) ) ) )
49 46 48 ax-mp ⊢ ( 𝐼 ‘ 2 ) = ( ( ( 2 − 1 ) / 2 ) · ( 𝐼 ‘ ( 2 − 2 ) ) )
50 2m1e1 ⊢ ( 2 − 1 ) = 1
51 50 oveq1i ⊢ ( ( 2 − 1 ) / 2 ) = ( 1 / 2 )
52 2cn ⊢ 2 ∈ ℂ
53 52 subidi ⊢ ( 2 − 2 ) = 0
54 53 fveq2i ⊢ ( 𝐼 ‘ ( 2 − 2 ) ) = ( 𝐼 ‘ 0 )
55 47 simp1i ⊢ ( 𝐼 ‘ 0 ) = π
56 54 55 eqtri ⊢ ( 𝐼 ‘ ( 2 − 2 ) ) = π
57 51 56 oveq12i ⊢ ( ( ( 2 − 1 ) / 2 ) · ( 𝐼 ‘ ( 2 − 2 ) ) ) = ( ( 1 / 2 ) · π )
58 ax-1cn ⊢ 1 ∈ ℂ
59 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
60 picn ⊢ π ∈ ℂ
61 div32 ⊢ ( ( 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ π ∈ ℂ ) → ( ( 1 / 2 ) · π ) = ( 1 · ( π / 2 ) ) )
62 58 59 60 61 mp3an ⊢ ( ( 1 / 2 ) · π ) = ( 1 · ( π / 2 ) )
63 2ne0 ⊢ 2 ≠ 0
64 60 52 63 divcli ⊢ ( π / 2 ) ∈ ℂ
65 64 mulid2i ⊢ ( 1 · ( π / 2 ) ) = ( π / 2 )
66 62 65 eqtri ⊢ ( ( 1 / 2 ) · π ) = ( π / 2 )
67 49 57 66 3eqtri ⊢ ( 𝐼 ‘ 2 ) = ( π / 2 )
68 3z ⊢ 3 ∈ ℤ
69 2re ⊢ 2 ∈ ℝ
70 3re ⊢ 3 ∈ ℝ
71 2lt3 ⊢ 2 < 3
72 69 70 71 ltleii ⊢ 2 ≤ 3
73 eluz2 ⊢ ( 3 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3 ) )
74 44 68 72 73 mpbir3an ⊢ 3 ∈ ( ℤ≥ ‘ 2 )
75 2 wallispilem2 ⊢ ( ( 𝐼 ‘ 0 ) = π ∧ ( 𝐼 ‘ 1 ) = 2 ∧ ( 3 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 3 ) = ( ( ( 3 − 1 ) / 3 ) · ( 𝐼 ‘ ( 3 − 2 ) ) ) ) )
76 75 simp3i ⊢ ( 3 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 3 ) = ( ( ( 3 − 1 ) / 3 ) · ( 𝐼 ‘ ( 3 − 2 ) ) ) )
77 74 76 ax-mp ⊢ ( 𝐼 ‘ 3 ) = ( ( ( 3 − 1 ) / 3 ) · ( 𝐼 ‘ ( 3 − 2 ) ) )
78 3m1e2 ⊢ ( 3 − 1 ) = 2
79 78 eqcomi ⊢ 2 = ( 3 − 1 )
80 79 oveq1i ⊢ ( 2 / 3 ) = ( ( 3 − 1 ) / 3 )
81 3cn ⊢ 3 ∈ ℂ
82 81 52 58 40 subaddrii ⊢ ( 3 − 2 ) = 1
83 82 fveq2i ⊢ ( 𝐼 ‘ ( 3 − 2 ) ) = ( 𝐼 ‘ 1 )
84 47 simp2i ⊢ ( 𝐼 ‘ 1 ) = 2
85 83 84 eqtr2i ⊢ 2 = ( 𝐼 ‘ ( 3 − 2 ) )
86 80 85 oveq12i ⊢ ( ( 2 / 3 ) · 2 ) = ( ( ( 3 − 1 ) / 3 ) · ( 𝐼 ‘ ( 3 − 2 ) ) )
87 3ne0 ⊢ 3 ≠ 0
88 52 81 87 divcli ⊢ ( 2 / 3 ) ∈ ℂ
89 88 52 mulcomi ⊢ ( ( 2 / 3 ) · 2 ) = ( 2 · ( 2 / 3 ) )
90 77 86 89 3eqtr2i ⊢ ( 𝐼 ‘ 3 ) = ( 2 · ( 2 / 3 ) )
91 67 90 oveq12i ⊢ ( ( 𝐼 ‘ 2 ) / ( 𝐼 ‘ 3 ) ) = ( ( π / 2 ) / ( 2 · ( 2 / 3 ) ) )
92 1z ⊢ 1 ∈ ℤ
93 seq1 ⊢ ( 1 ∈ ℤ → ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
94 92 93 ax-mp ⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 )
95 1nn ⊢ 1 ∈ ℕ
96 oveq2 ⊢ ( 𝑘 = 1 → ( 2 · 𝑘 ) = ( 2 · 1 ) )
97 96 37 eqtrdi ⊢ ( 𝑘 = 1 → ( 2 · 𝑘 ) = 2 )
98 96 oveq1d ⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · 1 ) − 1 ) )
99 37 oveq1i ⊢ ( ( 2 · 1 ) − 1 ) = ( 2 − 1 )
100 99 50 eqtri ⊢ ( ( 2 · 1 ) − 1 ) = 1
101 98 100 eqtrdi ⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) − 1 ) = 1 )
102 97 101 oveq12d ⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) = ( 2 / 1 ) )
103 52 div1i ⊢ ( 2 / 1 ) = 2
104 102 103 eqtrdi ⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) = 2 )
105 97 oveq1d ⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) + 1 ) = ( 2 + 1 ) )
106 105 40 eqtrdi ⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) + 1 ) = 3 )
107 97 106 oveq12d ⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) = ( 2 / 3 ) )
108 104 107 oveq12d ⊢ ( 𝑘 = 1 → ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( 2 · ( 2 / 3 ) ) )
109 ovex ⊢ ( 2 · ( 2 / 3 ) ) ∈ V
110 108 1 109 fvmpt ⊢ ( 1 ∈ ℕ → ( 𝐹 ‘ 1 ) = ( 2 · ( 2 / 3 ) ) )
111 95 110 ax-mp ⊢ ( 𝐹 ‘ 1 ) = ( 2 · ( 2 / 3 ) )
112 94 111 eqtr2i ⊢ ( 2 · ( 2 / 3 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 1 )
113 112 oveq2i ⊢ ( ( π / 2 ) / ( 2 · ( 2 / 3 ) ) ) = ( ( π / 2 ) / ( seq 1 ( · , 𝐹 ) ‘ 1 ) )
114 52 88 mulcli ⊢ ( 2 · ( 2 / 3 ) ) ∈ ℂ
115 111 114 eqeltri ⊢ ( 𝐹 ‘ 1 ) ∈ ℂ
116 94 115 eqeltri ⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) ∈ ℂ
117 52 81 63 87 divne0i ⊢ ( 2 / 3 ) ≠ 0
118 52 88 63 117 mulne0i ⊢ ( 2 · ( 2 / 3 ) ) ≠ 0
119 112 118 eqnetrri ⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≠ 0
120 64 116 119 divreci ⊢ ( ( π / 2 ) / ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) )
121 113 120 eqtri ⊢ ( ( π / 2 ) / ( 2 · ( 2 / 3 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) )
122 43 91 121 3eqtri ⊢ ( ( 𝐼 ‘ ( 2 · 1 ) ) / ( 𝐼 ‘ ( ( 2 · 1 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) )
123 oveq2 ⊢ ( ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) → ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) )
124 123 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) → ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) )
125 2cnd ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℂ )
126 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
127 58 a1i ⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℂ )
128 125 126 127 adddid ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) = ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) )
129 125 mulid1d ⊢ ( 𝑦 ∈ ℕ → ( 2 · 1 ) = 2 )
130 129 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) = ( ( 2 · 𝑦 ) + 2 ) )
131 128 130 eqtrd ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) = ( ( 2 · 𝑦 ) + 2 ) )
132 131 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) = ( ( ( 2 · 𝑦 ) + 2 ) − 1 ) )
133 125 126 mulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℂ )
134 133 125 127 addsubassd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 2 ) − 1 ) = ( ( 2 · 𝑦 ) + ( 2 − 1 ) ) )
135 50 a1i ⊢ ( 𝑦 ∈ ℕ → ( 2 − 1 ) = 1 )
136 135 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + ( 2 − 1 ) ) = ( ( 2 · 𝑦 ) + 1 ) )
137 132 134 136 3eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) = ( ( 2 · 𝑦 ) + 1 ) )
138 137 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) = ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) )
139 138 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) · ( 𝐼 ‘ ( 2 · 𝑦 ) ) ) = ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) · ( 𝐼 ‘ ( 2 · 𝑦 ) ) ) )
140 78 a1i ⊢ ( 𝑦 ∈ ℕ → ( 3 − 1 ) = 2 )
141 140 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + ( 3 − 1 ) ) = ( ( 2 · 𝑦 ) + 2 ) )
142 81 a1i ⊢ ( 𝑦 ∈ ℕ → 3 ∈ ℂ )
143 133 142 127 addsubassd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 3 ) − 1 ) = ( ( 2 · 𝑦 ) + ( 3 − 1 ) ) )
144 141 143 131 3eqtr4d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 3 ) − 1 ) = ( 2 · ( 𝑦 + 1 ) ) )
145 144 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 · 𝑦 ) + 3 ) − 1 ) / ( ( 2 · 𝑦 ) + 3 ) ) = ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) )
146 145 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( ( 2 · 𝑦 ) + 3 ) − 1 ) / ( ( 2 · 𝑦 ) + 3 ) ) · ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) · ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) )
147 139 146 oveq12d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( ( 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 ) ) ) ) )
148 44 a1i ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℤ )
149 nnz ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
150 149 peano2zd ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℤ )
151 148 150 zmulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ∈ ℤ )
152 69 a1i ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℝ )
153 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
154 1red ⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℝ )
155 153 154 readdcld ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℝ )
156 0le2 ⊢ 0 ≤ 2
157 156 a1i ⊢ ( 𝑦 ∈ ℕ → 0 ≤ 2 )
158 nnnn0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 )
159 158 nn0ge0d ⊢ ( 𝑦 ∈ ℕ → 0 ≤ 𝑦 )
160 154 153 addge02d ⊢ ( 𝑦 ∈ ℕ → ( 0 ≤ 𝑦 ↔ 1 ≤ ( 𝑦 + 1 ) ) )
161 159 160 mpbid ⊢ ( 𝑦 ∈ ℕ → 1 ≤ ( 𝑦 + 1 ) )
162 152 155 157 161 lemulge11d ⊢ ( 𝑦 ∈ ℕ → 2 ≤ ( 2 · ( 𝑦 + 1 ) ) )
163 44 eluz1i ⊢ ( ( 2 · ( 𝑦 + 1 ) ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 2 · ( 𝑦 + 1 ) ) ∈ ℤ ∧ 2 ≤ ( 2 · ( 𝑦 + 1 ) ) ) )
164 151 162 163 sylanbrc ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ∈ ( ℤ≥ ‘ 2 ) )
165 2 164 itgsinexp ⊢ ( 𝑦 ∈ ℕ → ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) = ( ( ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) · ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) − 2 ) ) ) )
166 131 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 2 ) = ( ( ( 2 · 𝑦 ) + 2 ) − 2 ) )
167 133 125 pncand ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 2 ) − 2 ) = ( 2 · 𝑦 ) )
168 166 167 eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 2 ) = ( 2 · 𝑦 ) )
169 168 fveq2d ⊢ ( 𝑦 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) − 2 ) ) = ( 𝐼 ‘ ( 2 · 𝑦 ) ) )
170 169 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) · ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) − 2 ) ) ) = ( ( ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) · ( 𝐼 ‘ ( 2 · 𝑦 ) ) ) )
171 165 170 eqtrd ⊢ ( 𝑦 ∈ ℕ → ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) = ( ( ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) · ( 𝐼 ‘ ( 2 · 𝑦 ) ) ) )
172 131 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) = ( ( ( 2 · 𝑦 ) + 2 ) + 1 ) )
173 133 125 127 addassd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 2 ) + 1 ) = ( ( 2 · 𝑦 ) + ( 2 + 1 ) ) )
174 40 a1i ⊢ ( 𝑦 ∈ ℕ → ( 2 + 1 ) = 3 )
175 174 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + ( 2 + 1 ) ) = ( ( 2 · 𝑦 ) + 3 ) )
176 172 173 175 3eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) = ( ( 2 · 𝑦 ) + 3 ) )
177 176 fveq2d ⊢ ( 𝑦 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) = ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 3 ) ) )
178 148 149 zmulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℤ )
179 68 a1i ⊢ ( 𝑦 ∈ ℕ → 3 ∈ ℤ )
180 178 179 zaddcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 3 ) ∈ ℤ )
181 152 153 remulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℝ )
182 70 a1i ⊢ ( 𝑦 ∈ ℕ → 3 ∈ ℝ )
183 181 182 readdcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 3 ) ∈ ℝ )
184 nnge1 ⊢ ( 𝑦 ∈ ℕ → 1 ≤ 𝑦 )
185 152 153 157 184 lemulge11d ⊢ ( 𝑦 ∈ ℕ → 2 ≤ ( 2 · 𝑦 ) )
186 0re ⊢ 0 ∈ ℝ
187 3pos ⊢ 0 < 3
188 186 70 187 ltleii ⊢ 0 ≤ 3
189 181 182 addge01d ⊢ ( 𝑦 ∈ ℕ → ( 0 ≤ 3 ↔ ( 2 · 𝑦 ) ≤ ( ( 2 · 𝑦 ) + 3 ) ) )
190 188 189 mpbii ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ≤ ( ( 2 · 𝑦 ) + 3 ) )
191 152 181 183 185 190 letrd ⊢ ( 𝑦 ∈ ℕ → 2 ≤ ( ( 2 · 𝑦 ) + 3 ) )
192 44 eluz1i ⊢ ( ( ( 2 · 𝑦 ) + 3 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( ( 2 · 𝑦 ) + 3 ) ∈ ℤ ∧ 2 ≤ ( ( 2 · 𝑦 ) + 3 ) ) )
193 180 191 192 sylanbrc ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 3 ) ∈ ( ℤ≥ ‘ 2 ) )
194 2 193 itgsinexp ⊢ ( 𝑦 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 3 ) ) = ( ( ( ( ( 2 · 𝑦 ) + 3 ) − 1 ) / ( ( 2 · 𝑦 ) + 3 ) ) · ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) )
195 177 194 eqtrd ⊢ ( 𝑦 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) = ( ( ( ( ( 2 · 𝑦 ) + 3 ) − 1 ) / ( ( 2 · 𝑦 ) + 3 ) ) · ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) )
196 171 195 oveq12d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) = ( ( ( ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) · ( 𝐼 ‘ ( 2 · 𝑦 ) ) ) / ( ( ( ( ( 2 · 𝑦 ) + 3 ) − 1 ) / ( ( 2 · 𝑦 ) + 3 ) ) · ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) ) )
197 133 127 addcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 1 ) ∈ ℂ )
198 126 127 addcld ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℂ )
199 125 198 mulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ∈ ℂ )
200 63 a1i ⊢ ( 𝑦 ∈ ℕ → 2 ≠ 0 )
201 peano2nn ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ )
202 201 nnne0d ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ≠ 0 )
203 125 198 200 202 mulne0d ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ≠ 0 )
204 197 199 203 divcld ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) ∈ ℂ )
205 2nn0 ⊢ 2 ∈ ℕ0
206 205 a1i ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℕ0 )
207 206 158 nn0mulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℕ0 )
208 2 wallispilem3 ⊢ ( ( 2 · 𝑦 ) ∈ ℕ0 → ( 𝐼 ‘ ( 2 · 𝑦 ) ) ∈ ℝ+ )
209 208 rpcnd ⊢ ( ( 2 · 𝑦 ) ∈ ℕ0 → ( 𝐼 ‘ ( 2 · 𝑦 ) ) ∈ ℂ )
210 207 209 syl ⊢ ( 𝑦 ∈ ℕ → ( 𝐼 ‘ ( 2 · 𝑦 ) ) ∈ ℂ )
211 133 142 addcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 3 ) ∈ ℂ )
212 0red ⊢ ( 𝑦 ∈ ℕ → 0 ∈ ℝ )
213 2pos ⊢ 0 < 2
214 213 a1i ⊢ ( 𝑦 ∈ ℕ → 0 < 2 )
215 nngt0 ⊢ ( 𝑦 ∈ ℕ → 0 < 𝑦 )
216 152 153 214 215 mulgt0d ⊢ ( 𝑦 ∈ ℕ → 0 < ( 2 · 𝑦 ) )
217 182 187 jctir ⊢ ( 𝑦 ∈ ℕ → ( 3 ∈ ℝ ∧ 0 < 3 ) )
218 elrp ⊢ ( 3 ∈ ℝ+ ↔ ( 3 ∈ ℝ ∧ 0 < 3 ) )
219 217 218 sylibr ⊢ ( 𝑦 ∈ ℕ → 3 ∈ ℝ+ )
220 181 219 ltaddrpd ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) < ( ( 2 · 𝑦 ) + 3 ) )
221 212 181 183 216 220 lttrd ⊢ ( 𝑦 ∈ ℕ → 0 < ( ( 2 · 𝑦 ) + 3 ) )
222 221 gt0ne0d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 3 ) ≠ 0 )
223 199 211 222 divcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ∈ ℂ )
224 199 211 203 222 divne0d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ≠ 0 )
225 180 148 zsubcld ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ∈ ℤ )
226 183 152 subge0d ⊢ ( 𝑦 ∈ ℕ → ( 0 ≤ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ↔ 2 ≤ ( ( 2 · 𝑦 ) + 3 ) ) )
227 191 226 mpbird ⊢ ( 𝑦 ∈ ℕ → 0 ≤ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) )
228 elnn0z ⊢ ( ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ∈ ℕ0 ↔ ( ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ∈ ℤ ∧ 0 ≤ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) )
229 225 227 228 sylanbrc ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ∈ ℕ0 )
230 2 wallispilem3 ⊢ ( ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ∈ ℕ0 → ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ∈ ℝ+ )
231 229 230 syl ⊢ ( 𝑦 ∈ ℕ → ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ∈ ℝ+ )
232 231 rpcnne0d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ∈ ℂ ∧ ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ≠ 0 ) )
233 223 224 232 jca31 ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ∈ ℂ ∧ ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ≠ 0 ) ∧ ( ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ∈ ℂ ∧ ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ≠ 0 ) ) )
234 divmuldiv ⊢ ( ( ( ( ( ( 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 ) ) ) ) )
235 204 210 233 234 syl21anc ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) · ( 𝐼 ‘ ( 2 · 𝑦 ) ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) · ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) ) )
236 147 196 235 3eqtr4d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) ) )
237 133 142 125 addsubassd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) = ( ( 2 · 𝑦 ) + ( 3 − 2 ) ) )
238 82 a1i ⊢ ( 𝑦 ∈ ℕ → ( 3 − 2 ) = 1 )
239 238 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + ( 3 − 2 ) ) = ( ( 2 · 𝑦 ) + 1 ) )
240 237 239 eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) = ( ( 2 · 𝑦 ) + 1 ) )
241 240 fveq2d ⊢ ( 𝑦 ∈ ℕ → ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) = ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) )
242 241 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) = ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) )
243 242 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( ( 2 · 𝑦 ) + 3 ) − 2 ) ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) ) )
244 236 243 eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) ) )
245 244 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) → ( ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) ) )
246 elnnuz ⊢ ( 𝑦 ∈ ℕ ↔ 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
247 246 biimpi ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
248 seqp1 ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( 𝐹 ‘ ( 𝑦 + 1 ) ) ) )
249 247 248 syl ⊢ ( 𝑦 ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( 𝐹 ‘ ( 𝑦 + 1 ) ) ) )
250 oveq2 ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( 2 · 𝑘 ) = ( 2 · ( 𝑦 + 1 ) ) )
251 250 oveq1d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) )
252 250 251 oveq12d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) = ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) )
253 250 oveq1d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) )
254 250 253 oveq12d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) )
255 252 254 oveq12d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) )
256 152 155 remulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ∈ ℝ )
257 256 154 resubcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ∈ ℝ )
258 1lt2 ⊢ 1 < 2
259 258 a1i ⊢ ( 𝑦 ∈ ℕ → 1 < 2 )
260 nnrp ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ+ )
261 154 260 ltaddrp2d ⊢ ( 𝑦 ∈ ℕ → 1 < ( 𝑦 + 1 ) )
262 152 155 259 261 mulgt1d ⊢ ( 𝑦 ∈ ℕ → 1 < ( 2 · ( 𝑦 + 1 ) ) )
263 154 262 gtned ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ≠ 1 )
264 199 127 263 subne0d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ≠ 0 )
265 256 257 264 redivcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ∈ ℝ )
266 176 183 eqeltrd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ∈ ℝ )
267 176 222 eqnetrd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ≠ 0 )
268 256 266 267 redivcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ∈ ℝ )
269 265 268 remulcld ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) ∈ ℝ )
270 1 255 201 269 fvmptd3 ⊢ ( 𝑦 ∈ ℕ → ( 𝐹 ‘ ( 𝑦 + 1 ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) )
271 270 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( 𝐹 ‘ ( 𝑦 + 1 ) ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) ) )
272 249 271 eqtrd ⊢ ( 𝑦 ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) ) )
273 272 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( 1 / ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) ) = ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) ) ) )
274 273 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) ) ) = ( ( π / 2 ) · ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) ) ) ) )
275 137 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) = ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) )
276 176 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) = ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) )
277 275 276 oveq12d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) )
278 277 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) )
279 278 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) ) ) = ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) ) )
280 279 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( π / 2 ) · ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) ) ) ) = ( ( π / 2 ) · ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) ) ) )
281 elfznn ⊢ ( 𝑤 ∈ ( 1 ... 𝑦 ) → 𝑤 ∈ ℕ )
282 281 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ( 1 ... 𝑦 ) ) → 𝑤 ∈ ℕ )
283 oveq2 ⊢ ( 𝑘 = 𝑤 → ( 2 · 𝑘 ) = ( 2 · 𝑤 ) )
284 283 oveq1d ⊢ ( 𝑘 = 𝑤 → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · 𝑤 ) − 1 ) )
285 283 284 oveq12d ⊢ ( 𝑘 = 𝑤 → ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) = ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) − 1 ) ) )
286 283 oveq1d ⊢ ( 𝑘 = 𝑤 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑤 ) + 1 ) )
287 283 286 oveq12d ⊢ ( 𝑘 = 𝑤 → ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) + 1 ) ) )
288 285 287 oveq12d ⊢ ( 𝑘 = 𝑤 → ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) − 1 ) ) · ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) + 1 ) ) ) )
289 id ⊢ ( 𝑤 ∈ ℕ → 𝑤 ∈ ℕ )
290 2rp ⊢ 2 ∈ ℝ+
291 290 a1i ⊢ ( 𝑤 ∈ ℕ → 2 ∈ ℝ+ )
292 nnrp ⊢ ( 𝑤 ∈ ℕ → 𝑤 ∈ ℝ+ )
293 291 292 rpmulcld ⊢ ( 𝑤 ∈ ℕ → ( 2 · 𝑤 ) ∈ ℝ+ )
294 69 a1i ⊢ ( 𝑤 ∈ ℕ → 2 ∈ ℝ )
295 nnre ⊢ ( 𝑤 ∈ ℕ → 𝑤 ∈ ℝ )
296 294 295 remulcld ⊢ ( 𝑤 ∈ ℕ → ( 2 · 𝑤 ) ∈ ℝ )
297 1red ⊢ ( 𝑤 ∈ ℕ → 1 ∈ ℝ )
298 296 297 resubcld ⊢ ( 𝑤 ∈ ℕ → ( ( 2 · 𝑤 ) − 1 ) ∈ ℝ )
299 nnge1 ⊢ ( 𝑤 ∈ ℕ → 1 ≤ 𝑤 )
300 nncn ⊢ ( 𝑤 ∈ ℕ → 𝑤 ∈ ℂ )
301 300 mulid2d ⊢ ( 𝑤 ∈ ℕ → ( 1 · 𝑤 ) = 𝑤 )
302 297 294 292 ltmul1d ⊢ ( 𝑤 ∈ ℕ → ( 1 < 2 ↔ ( 1 · 𝑤 ) < ( 2 · 𝑤 ) ) )
303 258 302 mpbii ⊢ ( 𝑤 ∈ ℕ → ( 1 · 𝑤 ) < ( 2 · 𝑤 ) )
304 301 303 eqbrtrrd ⊢ ( 𝑤 ∈ ℕ → 𝑤 < ( 2 · 𝑤 ) )
305 297 295 296 299 304 lelttrd ⊢ ( 𝑤 ∈ ℕ → 1 < ( 2 · 𝑤 ) )
306 297 296 posdifd ⊢ ( 𝑤 ∈ ℕ → ( 1 < ( 2 · 𝑤 ) ↔ 0 < ( ( 2 · 𝑤 ) − 1 ) ) )
307 305 306 mpbid ⊢ ( 𝑤 ∈ ℕ → 0 < ( ( 2 · 𝑤 ) − 1 ) )
308 298 307 elrpd ⊢ ( 𝑤 ∈ ℕ → ( ( 2 · 𝑤 ) − 1 ) ∈ ℝ+ )
309 293 308 rpdivcld ⊢ ( 𝑤 ∈ ℕ → ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) − 1 ) ) ∈ ℝ+ )
310 156 a1i ⊢ ( 𝑤 ∈ ℕ → 0 ≤ 2 )
311 292 rpge0d ⊢ ( 𝑤 ∈ ℕ → 0 ≤ 𝑤 )
312 294 295 310 311 mulge0d ⊢ ( 𝑤 ∈ ℕ → 0 ≤ ( 2 · 𝑤 ) )
313 296 312 ge0p1rpd ⊢ ( 𝑤 ∈ ℕ → ( ( 2 · 𝑤 ) + 1 ) ∈ ℝ+ )
314 293 313 rpdivcld ⊢ ( 𝑤 ∈ ℕ → ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) + 1 ) ) ∈ ℝ+ )
315 309 314 rpmulcld ⊢ ( 𝑤 ∈ ℕ → ( ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) − 1 ) ) · ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) + 1 ) ) ) ∈ ℝ+ )
316 1 288 289 315 fvmptd3 ⊢ ( 𝑤 ∈ ℕ → ( 𝐹 ‘ 𝑤 ) = ( ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) − 1 ) ) · ( ( 2 · 𝑤 ) / ( ( 2 · 𝑤 ) + 1 ) ) ) )
317 316 315 eqeltrd ⊢ ( 𝑤 ∈ ℕ → ( 𝐹 ‘ 𝑤 ) ∈ ℝ+ )
318 282 317 syl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ( 1 ... 𝑦 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ℝ+ )
319 rpmulcl ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) → ( 𝑤 · 𝑧 ) ∈ ℝ+ )
320 319 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑤 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( 𝑤 · 𝑧 ) ∈ ℝ+ )
321 247 318 320 seqcl ⊢ ( 𝑦 ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ∈ ℝ+ )
322 321 rpcnne0d ⊢ ( 𝑦 ∈ ℕ → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ∈ ℂ ∧ ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ≠ 0 ) )
323 290 a1i ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℝ+ )
324 153 159 ge0p1rpd ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℝ+ )
325 323 324 rpmulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ∈ ℝ+ )
326 152 153 157 159 mulge0d ⊢ ( 𝑦 ∈ ℕ → 0 ≤ ( 2 · 𝑦 ) )
327 181 326 ge0p1rpd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 1 ) ∈ ℝ+ )
328 325 327 rpdivcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) ∈ ℝ+ )
329 323 260 rpmulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℝ+ )
330 329 219 rpaddcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 3 ) ∈ ℝ+ )
331 325 330 rpdivcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ∈ ℝ+ )
332 328 331 rpmulcld ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ∈ ℝ+ )
333 332 rpcnne0d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ∈ ℂ ∧ ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ≠ 0 ) )
334 divdiv1 ⊢ ( ( 1 ∈ ℂ ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ∈ ℂ ∧ ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ≠ 0 ) ∧ ( ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ∈ ℂ ∧ ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ≠ 0 ) ) → ( ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) = ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) ) )
335 127 322 333 334 syl3anc ⊢ ( 𝑦 ∈ ℕ → ( ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) = ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) ) )
336 335 eqcomd ⊢ ( 𝑦 ∈ ℕ → ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) ) = ( ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) )
337 336 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( π / 2 ) · ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) ) ) = ( ( π / 2 ) · ( ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) ) )
338 64 a1i ⊢ ( 𝑦 ∈ ℕ → ( π / 2 ) ∈ ℂ )
339 321 rpcnd ⊢ ( 𝑦 ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ∈ ℂ )
340 321 rpne0d ⊢ ( 𝑦 ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ≠ 0 )
341 339 340 reccld ⊢ ( 𝑦 ∈ ℕ → ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ∈ ℂ )
342 332 rpcnd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ∈ ℂ )
343 332 rpne0d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ≠ 0 )
344 338 341 342 343 divassd ⊢ ( 𝑦 ∈ ℕ → ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) = ( ( π / 2 ) · ( ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) ) )
345 137 264 eqnetrrd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 1 ) ≠ 0 )
346 199 197 199 211 345 222 divmuldivd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) / ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) ) )
347 346 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) = ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) / ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) ) ) )
348 338 341 mulcld ⊢ ( 𝑦 ∈ ℕ → ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ∈ ℂ )
349 199 199 mulcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ∈ ℂ )
350 197 211 mulcld ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) ∈ ℂ )
351 199 199 203 203 mulne0d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ≠ 0 )
352 197 211 345 222 mulne0d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) ≠ 0 )
353 348 349 350 351 352 divdiv2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) / ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) ) ) = ( ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) · ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ) )
354 348 350 349 351 divassd ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) · ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ) = ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) · ( ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ) ) )
355 353 354 eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) / ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) ) ) = ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) · ( ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ) ) )
356 197 199 199 211 203 222 203 divdivdivd ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) = ( ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ) )
357 356 eqcomd ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ) = ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) )
358 357 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) · ( ( ( ( 2 · 𝑦 ) + 1 ) · ( ( 2 · 𝑦 ) + 3 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ) ) = ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) · ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) )
359 347 355 358 3eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) / ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) = ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) · ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) )
360 337 344 359 3eqtr2d ⊢ ( 𝑦 ∈ ℕ → ( ( π / 2 ) · ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) ) ) = ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) · ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) )
361 60 a1i ⊢ ( 𝑦 ∈ ℕ → π ∈ ℂ )
362 361 halfcld ⊢ ( 𝑦 ∈ ℕ → ( π / 2 ) ∈ ℂ )
363 362 341 mulcld ⊢ ( 𝑦 ∈ ℕ → ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ∈ ℂ )
364 204 223 224 divcld ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ∈ ℂ )
365 363 364 mulcomd ⊢ ( 𝑦 ∈ ℕ → ( ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) · ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) )
366 280 360 365 3eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( π / 2 ) · ( 1 / ( ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) )
367 274 366 eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) )
368 367 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) → ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) ) ) = ( ( ( ( ( 2 · 𝑦 ) + 1 ) / ( 2 · ( 𝑦 + 1 ) ) ) / ( ( 2 · ( 𝑦 + 1 ) ) / ( ( 2 · 𝑦 ) + 3 ) ) ) · ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) )
369 124 245 368 3eqtr4d ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) ) → ( ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) ) ) )
370 369 ex ⊢ ( 𝑦 ∈ ℕ → ( ( ( 𝐼 ‘ ( 2 · 𝑦 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑦 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑦 ) ) ) → ( ( 𝐼 ‘ ( 2 · ( 𝑦 + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · ( 𝑦 + 1 ) ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ ( 𝑦 + 1 ) ) ) ) ) )
371 12 20 28 36 122 370 nnind ⊢ ( 𝑛 ∈ ℕ → ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) ) ) )
372 371 mpteq2ia ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) ) ) )
373 372 3 4 3eqtr4i ⊢ 𝐺 = 𝐻