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	$⊢ F = (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))$
	wallispilem4.2	$⊢ I = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin z}^{n} d z)$
	wallispilem4.3	$⊢ G = (n \in ℕ ⟼ \frac{I (2 n)}{I (2 n + 1)})$
	wallispilem4.4	$⊢ H = (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)}))$
Assertion	wallispilem4	$⊢ G = H$

Proof

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

Metamath Proof Explorer

Theorem wallispilem4

Proof