wallispilem4 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > wallispilem4		Structured version Unicode version

Theorem wallispilem4 37749

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
wallispilem4.2
wallispilem4.3
wallispilem4.4

**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.

Step	Hyp	Ref	Expression
1		oveq2 6309	. . . . . . 7
2	1	fveq2d 5881	. . . . . 6
3	1	oveq1d 6316	. . . . . . 7
4	3	fveq2d 5881	. . . . . 6
5	2, 4	oveq12d 6319	. . . . 5
6		fveq2 5877	. . . . . . 7
7	6	oveq2d 6317	. . . . . 6
8	7	oveq2d 6317	. . . . 5
9	5, 8	eqeq12d 2444	. . . 4
10		oveq2 6309	. . . . . . 7
11	10	fveq2d 5881	. . . . . 6
12	10	oveq1d 6316	. . . . . . 7
13	12	fveq2d 5881	. . . . . 6
14	11, 13	oveq12d 6319	. . . . 5
15		fveq2 5877	. . . . . . 7
16	15	oveq2d 6317	. . . . . 6
17	16	oveq2d 6317	. . . . 5
18	14, 17	eqeq12d 2444	. . . 4
19		oveq2 6309	. . . . . . 7
20	19	fveq2d 5881	. . . . . 6
21	19	oveq1d 6316	. . . . . . 7
22	21	fveq2d 5881	. . . . . 6
23	20, 22	oveq12d 6319	. . . . 5
24		fveq2 5877	. . . . . . 7
25	24	oveq2d 6317	. . . . . 6
26	25	oveq2d 6317	. . . . 5
27	23, 26	eqeq12d 2444	. . . 4
28		oveq2 6309	. . . . . . 7
29	28	fveq2d 5881	. . . . . 6
30	28	oveq1d 6316	. . . . . . 7
31	30	fveq2d 5881	. . . . . 6
32	29, 31	oveq12d 6319	. . . . 5
33		fveq2 5877	. . . . . . 7
34	33	oveq2d 6317	. . . . . 6
35	34	oveq2d 6317	. . . . 5
36	32, 35	eqeq12d 2444	. . . 4
37		2t1e2 10758	. . . . . . 7
38	37	fveq2i 5880	. . . . . 6
39	37	oveq1i 6311	. . . . . . . 8
40		2p1e3 10733	. . . . . . . 8
41	39, 40	eqtri 2451	. . . . . . 7
42	41	fveq2i 5880	. . . . . 6
43	38, 42	oveq12i 6313	. . . . 5
44		2z 10969	. . . . . . . . 9
45		uzid 11173	. . . . . . . . 9
46	44, 45	ax-mp 5	. . . . . . . 8
47		wallispilem4.2	. . . . . . . . . 10
48	47	wallispilem2 37747	. . . . . . . . 9 $/\$ $/\$
49	48	simp3i 1016	. . . . . . . 8
50	46, 49	ax-mp 5	. . . . . . 7
51		2m1e1 10724	. . . . . . . . 9
52	51	oveq1i 6311	. . . . . . . 8
53		2cn 10680	. . . . . . . . . . 11
54	53	subidi 9945	. . . . . . . . . 10
55	54	fveq2i 5880	. . . . . . . . 9
56	48	simp1i 1014	. . . . . . . . 9
57	55, 56	eqtri 2451	. . . . . . . 8
58	52, 57	oveq12i 6313	. . . . . . 7
59		ax-1cn 9597	. . . . . . . . 9
60		2cnne0 10824	. . . . . . . . 9 $/\$
61		picn 23400	. . . . . . . . 9
62		div32 10290	. . . . . . . . 9 $/\$ $/\$ $/\$
63	59, 60, 61, 62	mp3an 1360	. . . . . . . 8
64		2ne0 10702	. . . . . . . . . 10
65	61, 53, 64	divcli 10349	. . . . . . . . 9
66	65	mulid2i 9646	. . . . . . . 8
67	63, 66	eqtri 2451	. . . . . . 7
68	50, 58, 67	3eqtri 2455	. . . . . 6
69		3z 10970	. . . . . . . . 9
70		2re 10679	. . . . . . . . . 10
71		3re 10683	. . . . . . . . . 10
72		2lt3 10777	. . . . . . . . . 10
73	70, 71, 72	ltleii 9757	. . . . . . . . 9
74		eluz2 11165	. . . . . . . . 9 $/\$ $/\$
75	44, 69, 73, 74	mpbir3an 1187	. . . . . . . 8
76	47	wallispilem2 37747	. . . . . . . . 9 $/\$ $/\$
77	76	simp3i 1016	. . . . . . . 8
78	75, 77	ax-mp 5	. . . . . . 7
79		3m1e2 10726	. . . . . . . . . 10
80	79	eqcomi 2435	. . . . . . . . 9
81	80	oveq1i 6311	. . . . . . . 8
82		3cn 10684	. . . . . . . . . . 11
83	82, 53, 59, 40	subaddrii 9964	. . . . . . . . . 10
84	83	fveq2i 5880	. . . . . . . . 9
85	48	simp2i 1015	. . . . . . . . 9
86	84, 85	eqtr2i 2452	. . . . . . . 8
87	81, 86	oveq12i 6313	. . . . . . 7
88		3ne0 10704	. . . . . . . . 9
89	53, 82, 88	divcli 10349	. . . . . . . 8
90	89, 53	mulcomi 9649	. . . . . . 7
91	78, 87, 90	3eqtr2i 2457	. . . . . 6
92	68, 91	oveq12i 6313	. . . . 5
93		1z 10967	. . . . . . . . 9
94		seq1 12225	. . . . . . . . 9
95	93, 94	ax-mp 5	. . . . . . . 8
96		1nn 10620	. . . . . . . . 9
97		oveq2 6309	. . . . . . . . . . . . . 14
98	97, 37	syl6eq 2479	. . . . . . . . . . . . 13
99	97	oveq1d 6316	. . . . . . . . . . . . . 14
100	37	oveq1i 6311	. . . . . . . . . . . . . . 15
101	100, 51	eqtri 2451	. . . . . . . . . . . . . 14
102	99, 101	syl6eq 2479	. . . . . . . . . . . . 13
103	98, 102	oveq12d 6319	. . . . . . . . . . . 12
104	53	div1i 10335	. . . . . . . . . . . 12
105	103, 104	syl6eq 2479	. . . . . . . . . . 11
106	98	oveq1d 6316	. . . . . . . . . . . . 13
107	106, 40	syl6eq 2479	. . . . . . . . . . . 12
108	98, 107	oveq12d 6319	. . . . . . . . . . 11
109	105, 108	oveq12d 6319	. . . . . . . . . 10
110		wallispilem4.1	. . . . . . . . . 10
111		ovex 6329	. . . . . . . . . 10
112	109, 110, 111	fvmpt 5960	. . . . . . . . 9
113	96, 112	ax-mp 5	. . . . . . . 8
114	95, 113	eqtr2i 2452	. . . . . . 7
115	114	oveq2i 6312	. . . . . 6
116	53, 89	mulcli 9648	. . . . . . . . 9
117	113, 116	eqeltri 2506	. . . . . . . 8
118	95, 117	eqeltri 2506	. . . . . . 7
119	53, 82, 64, 88	divne0i 10355	. . . . . . . . 9
120	53, 89, 64, 119	mulne0i 10255	. . . . . . . 8
121	114, 120	eqnetrri 2721	. . . . . . 7
122	65, 118, 121	divreci 10352	. . . . . 6
123	115, 122	eqtri 2451	. . . . 5
124	43, 92, 123	3eqtri 2455	. . . 4
125		oveq2 6309	. . . . . . 7
126	125	adantl 467	. . . . . 6 $/\$
127		2cnd 10682	. . . . . . . . . . . . . . . 16
128		nncn 10617	. . . . . . . . . . . . . . . 16
129	59	a1i 11	. . . . . . . . . . . . . . . 16
130	127, 128, 129	adddid 9667	. . . . . . . . . . . . . . 15
131	127	mulid1d 9660	. . . . . . . . . . . . . . . 16
132	131	oveq2d 6317	. . . . . . . . . . . . . . 15
133	130, 132	eqtrd 2463	. . . . . . . . . . . . . 14
134	133	oveq1d 6316	. . . . . . . . . . . . 13
135	127, 128	mulcld 9663	. . . . . . . . . . . . . 14
136	135, 127, 129	addsubassd 10006	. . . . . . . . . . . . 13
137	51	a1i 11	. . . . . . . . . . . . . 14
138	137	oveq2d 6317	. . . . . . . . . . . . 13
139	134, 136, 138	3eqtrd 2467	. . . . . . . . . . . 12
140	139	oveq1d 6316	. . . . . . . . . . 11
141	140	oveq1d 6316	. . . . . . . . . 10
142	79	a1i 11	. . . . . . . . . . . . . 14
143	142	oveq2d 6317	. . . . . . . . . . . . 13
144	82	a1i 11	. . . . . . . . . . . . . 14
145	135, 144, 129	addsubassd 10006	. . . . . . . . . . . . 13
146	143, 145, 133	3eqtr4d 2473	. . . . . . . . . . . 12
147	146	oveq1d 6316	. . . . . . . . . . 11
148	147	oveq1d 6316	. . . . . . . . . 10
149	141, 148	oveq12d 6319	. . . . . . . . 9
150	44	a1i 11	. . . . . . . . . . . . . 14
151		nnz 10959	. . . . . . . . . . . . . . 15
152	151	peano2zd 11043	. . . . . . . . . . . . . 14
153	150, 152	zmulcld 11046	. . . . . . . . . . . . 13
154	70	a1i 11	. . . . . . . . . . . . . 14
155		nnre 10616	. . . . . . . . . . . . . . 15
156		1red 9658	. . . . . . . . . . . . . . 15
157	155, 156	readdcld 9670	. . . . . . . . . . . . . 14
158		0le2 10700	. . . . . . . . . . . . . . 15
159	158	a1i 11	. . . . . . . . . . . . . 14
160		nnnn0 10876	. . . . . . . . . . . . . . . 16
161	160	nn0ge0d 10928	. . . . . . . . . . . . . . 15
162	156, 155	addge02d 10202	. . . . . . . . . . . . . . 15
163	161, 162	mpbid 213	. . . . . . . . . . . . . 14
164	154, 157, 159, 163	lemulge11d 10544	. . . . . . . . . . . . 13
165	44	eluz1i 11166	. . . . . . . . . . . . 13 $/\$
166	153, 164, 165	sylanbrc 668	. . . . . . . . . . . 12
167	47, 166	itgsinexp 37650	. . . . . . . . . . 11
168	133	oveq1d 6316	. . . . . . . . . . . . . 14
169	135, 127	pncand 9987	. . . . . . . . . . . . . 14
170	168, 169	eqtrd 2463	. . . . . . . . . . . . 13
171	170	fveq2d 5881	. . . . . . . . . . . 12
172	171	oveq2d 6317	. . . . . . . . . . 11
173	167, 172	eqtrd 2463	. . . . . . . . . 10
174	133	oveq1d 6316	. . . . . . . . . . . . 13
175	135, 127, 129	addassd 9665	. . . . . . . . . . . . 13
176	40	a1i 11	. . . . . . . . . . . . . 14
177	176	oveq2d 6317	. . . . . . . . . . . . 13
178	174, 175, 177	3eqtrd 2467	. . . . . . . . . . . 12
179	178	fveq2d 5881	. . . . . . . . . . 11
180	150, 151	zmulcld 11046	. . . . . . . . . . . . . 14
181	69	a1i 11	. . . . . . . . . . . . . 14
182	180, 181	zaddcld 11044	. . . . . . . . . . . . 13
183	154, 155	remulcld 9671	. . . . . . . . . . . . . 14
184	71	a1i 11	. . . . . . . . . . . . . . 15
185	183, 184	readdcld 9670	. . . . . . . . . . . . . 14
186		nnge1 10635	. . . . . . . . . . . . . . 15
187	154, 155, 159, 186	lemulge11d 10544	. . . . . . . . . . . . . 14
188		0re 9643	. . . . . . . . . . . . . . . 16
189		3pos 10703	. . . . . . . . . . . . . . . 16
190	188, 71, 189	ltleii 9757	. . . . . . . . . . . . . . 15
191	183, 184	addge01d 10201	. . . . . . . . . . . . . . 15
192	190, 191	mpbii 214	. . . . . . . . . . . . . 14
193	154, 183, 185, 187, 192	letrd 9792	. . . . . . . . . . . . 13
194	44	eluz1i 11166	. . . . . . . . . . . . 13 $/\$
195	182, 193, 194	sylanbrc 668	. . . . . . . . . . . 12
196	47, 195	itgsinexp 37650	. . . . . . . . . . 11
197	179, 196	eqtrd 2463	. . . . . . . . . 10
198	173, 197	oveq12d 6319	. . . . . . . . 9
199	135, 129	addcld 9662	. . . . . . . . . . 11
200	128, 129	addcld 9662	. . . . . . . . . . . 12
201	127, 200	mulcld 9663	. . . . . . . . . . 11
202	64	a1i 11	. . . . . . . . . . . 12
203		peano2nn 10621	. . . . . . . . . . . . 13
204	203	nnne0d 10654	. . . . . . . . . . . 12
205	127, 200, 202, 204	mulne0d 10264	. . . . . . . . . . 11
206	199, 201, 205	divcld 10383	. . . . . . . . . 10
207		2nn0 10886	. . . . . . . . . . . . 13
208	207	a1i 11	. . . . . . . . . . . 12
209	208, 160	nn0mulcld 10930	. . . . . . . . . . 11
210	47	wallispilem3 37748	. . . . . . . . . . . 12
211	210	rpcnd 11343	. . . . . . . . . . 11
212	209, 211	syl 17	. . . . . . . . . 10
213	135, 144	addcld 9662	. . . . . . . . . . . 12
214		0red 9644	. . . . . . . . . . . . . 14
215		2pos 10701	. . . . . . . . . . . . . . . 16
216	215	a1i 11	. . . . . . . . . . . . . . 15
217		nngt0 10638	. . . . . . . . . . . . . . 15
218	154, 155, 216, 217	mulgt0d 9790	. . . . . . . . . . . . . 14
219	184, 189	jctir 540	. . . . . . . . . . . . . . . 16 $/\$
220		elrp 11304	. . . . . . . . . . . . . . . 16 $/\$
221	219, 220	sylibr 215	. . . . . . . . . . . . . . 15
222	183, 221	ltaddrpd 11371	. . . . . . . . . . . . . 14
223	214, 183, 185, 218, 222	lttrd 9796	. . . . . . . . . . . . 13
224	223	gt0ne0d 10178	. . . . . . . . . . . 12
225	201, 213, 224	divcld 10383	. . . . . . . . . . 11
226	201, 213, 205, 224	divne0d 10399	. . . . . . . . . . 11
227	182, 150	zsubcld 11045	. . . . . . . . . . . . . 14
228	185, 154	subge0d 10203	. . . . . . . . . . . . . . 15
229	193, 228	mpbird 235	. . . . . . . . . . . . . 14
230		elnn0z 10950	. . . . . . . . . . . . . 14 $/\$
231	227, 229, 230	sylanbrc 668	. . . . . . . . . . . . 13
232	47	wallispilem3 37748	. . . . . . . . . . . . 13
233	231, 232	syl 17	. . . . . . . . . . . 12
234	233	rpcnne0d 11350	. . . . . . . . . . 11 $/\$
235	225, 226, 234	jca31 536	. . . . . . . . . 10 $/\$ $/\$ $/\$
236		divmuldiv 10307	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
237	206, 212, 235, 236	syl21anc 1263	. . . . . . . . 9
238	149, 198, 237	3eqtr4d 2473	. . . . . . . 8
239	135, 144, 127	addsubassd 10006	. . . . . . . . . . . 12
240	83	a1i 11	. . . . . . . . . . . . 13
241	240	oveq2d 6317	. . . . . . . . . . . 12
242	239, 241	eqtrd 2463	. . . . . . . . . . 11
243	242	fveq2d 5881	. . . . . . . . . 10
244	243	oveq2d 6317	. . . . . . . . 9
245	244	oveq2d 6317	. . . . . . . 8
246	238, 245	eqtrd 2463	. . . . . . 7
247	246	adantr 466	. . . . . 6 $/\$
248		elnnuz 11195	. . . . . . . . . . . . 13
249	248	biimpi 197	. . . . . . . . . . . 12
250		seqp1 12227	. . . . . . . . . . . 12
251	249, 250	syl 17	. . . . . . . . . . 11
252	110	a1i 11	. . . . . . . . . . . . 13
253		oveq2 6309	. . . . . . . . . . . . . . . 16
254	253	oveq1d 6316	. . . . . . . . . . . . . . . 16
255	253, 254	oveq12d 6319	. . . . . . . . . . . . . . 15
256	253	oveq1d 6316	. . . . . . . . . . . . . . . 16
257	253, 256	oveq12d 6319	. . . . . . . . . . . . . . 15
258	255, 257	oveq12d 6319	. . . . . . . . . . . . . 14
259	258	adantl 467	. . . . . . . . . . . . 13 $/\$
260	154, 157	remulcld 9671	. . . . . . . . . . . . . . 15
261	260, 156	resubcld 10047	. . . . . . . . . . . . . . 15
262		1lt2 10776	. . . . . . . . . . . . . . . . . . 19
263	262	a1i 11	. . . . . . . . . . . . . . . . . 18
264		nnrp 11311	. . . . . . . . . . . . . . . . . . 19
265	156, 264	ltaddrp2d 11372	. . . . . . . . . . . . . . . . . 18
266	154, 157, 263, 265	mulgt1d 10543	. . . . . . . . . . . . . . . . 17
267	156, 266	gtned 9770	. . . . . . . . . . . . . . . 16
268	201, 129, 267	subne0d 9995	. . . . . . . . . . . . . . 15
269	260, 261, 268	redivcld 10435	. . . . . . . . . . . . . 14
270	178, 185	eqeltrd 2510	. . . . . . . . . . . . . . 15
271	178, 224	eqnetrd 2717	. . . . . . . . . . . . . . 15
272	260, 270, 271	redivcld 10435	. . . . . . . . . . . . . 14
273	269, 272	remulcld 9671	. . . . . . . . . . . . 13
274	252, 259, 203, 273	fvmptd 5966	. . . . . . . . . . . 12
275	274	oveq2d 6317	. . . . . . . . . . 11
276	251, 275	eqtrd 2463	. . . . . . . . . 10
277	276	oveq2d 6317	. . . . . . . . 9
278	277	oveq2d 6317	. . . . . . . 8
279	139	oveq2d 6317	. . . . . . . . . . . . 13
280	178	oveq2d 6317	. . . . . . . . . . . . 13
281	279, 280	oveq12d 6319	. . . . . . . . . . . 12
282	281	oveq2d 6317	. . . . . . . . . . 11
283	282	oveq2d 6317	. . . . . . . . . 10
284	283	oveq2d 6317	. . . . . . . . 9
285		elfznn 11828	. . . . . . . . . . . . . . . . 17
286	285	adantl 467	. . . . . . . . . . . . . . . 16 $/\$
287	110	a1i 11	. . . . . . . . . . . . . . . . . 18
288		oveq2 6309	. . . . . . . . . . . . . . . . . . . . 21
289	288	oveq1d 6316	. . . . . . . . . . . . . . . . . . . . 21
290	288, 289	oveq12d 6319	. . . . . . . . . . . . . . . . . . . 20
291	288	oveq1d 6316	. . . . . . . . . . . . . . . . . . . . 21
292	288, 291	oveq12d 6319	. . . . . . . . . . . . . . . . . . . 20
293	290, 292	oveq12d 6319	. . . . . . . . . . . . . . . . . . 19
294	293	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$
295		id 23	. . . . . . . . . . . . . . . . . 18
296		2rp 11307	. . . . . . . . . . . . . . . . . . . . . 22
297	296	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
298		nnrp 11311	. . . . . . . . . . . . . . . . . . . . 21
299	297, 298	rpmulcld 11357	. . . . . . . . . . . . . . . . . . . 20
300	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
301		nnre 10616	. . . . . . . . . . . . . . . . . . . . . . 23
302	300, 301	remulcld 9671	. . . . . . . . . . . . . . . . . . . . . 22
303		1red 9658	. . . . . . . . . . . . . . . . . . . . . 22
304	302, 303	resubcld 10047	. . . . . . . . . . . . . . . . . . . . 21
305		nnge1 10635	. . . . . . . . . . . . . . . . . . . . . . 23
306		nncn 10617	. . . . . . . . . . . . . . . . . . . . . . . . 25
307	306	mulid2d 9661	. . . . . . . . . . . . . . . . . . . . . . . 24
308	303, 300, 298	ltmul1d 11379	. . . . . . . . . . . . . . . . . . . . . . . . 25
309	262, 308	mpbii 214	. . . . . . . . . . . . . . . . . . . . . . . 24
310	307, 309	eqbrtrrd 4443	. . . . . . . . . . . . . . . . . . . . . . 23
311	303, 301, 302, 305, 310	lelttrd 9793	. . . . . . . . . . . . . . . . . . . . . 22
312	303, 302	posdifd 10200	. . . . . . . . . . . . . . . . . . . . . 22
313	311, 312	mpbid 213	. . . . . . . . . . . . . . . . . . . . 21
314	304, 313	elrpd 11338	. . . . . . . . . . . . . . . . . . . 20
315	299, 314	rpdivcld 11358	. . . . . . . . . . . . . . . . . . 19
316	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
317	298	rpge0d 11345	. . . . . . . . . . . . . . . . . . . . . 22
318	300, 301, 316, 317	mulge0d 10190	. . . . . . . . . . . . . . . . . . . . 21
319	302, 318	ge0p1rpd 11368	. . . . . . . . . . . . . . . . . . . 20
320	299, 319	rpdivcld 11358	. . . . . . . . . . . . . . . . . . 19
321	315, 320	rpmulcld 11357	. . . . . . . . . . . . . . . . . 18
322	287, 294, 295, 321	fvmptd 5966	. . . . . . . . . . . . . . . . 17
323	322, 321	eqeltrd 2510	. . . . . . . . . . . . . . . 16
324	286, 323	syl 17	. . . . . . . . . . . . . . 15 $/\$
325		rpmulcl 11324	. . . . . . . . . . . . . . . 16 $/\$
326	325	adantl 467	. . . . . . . . . . . . . . 15 $/\$ $/\$
327	249, 324, 326	seqcl 12232	. . . . . . . . . . . . . 14
328	327	rpcnne0d 11350	. . . . . . . . . . . . 13 $/\$
329	296	a1i 11	. . . . . . . . . . . . . . . . 17
330	155, 161	ge0p1rpd 11368	. . . . . . . . . . . . . . . . 17
331	329, 330	rpmulcld 11357	. . . . . . . . . . . . . . . 16
332	154, 155, 159, 161	mulge0d 10190	. . . . . . . . . . . . . . . . 17
333	183, 332	ge0p1rpd 11368	. . . . . . . . . . . . . . . 16
334	331, 333	rpdivcld 11358	. . . . . . . . . . . . . . 15
335	329, 264	rpmulcld 11357	. . . . . . . . . . . . . . . . 17
336	335, 221	rpaddcld 11356	. . . . . . . . . . . . . . . 16
337	331, 336	rpdivcld 11358	. . . . . . . . . . . . . . 15
338	334, 337	rpmulcld 11357	. . . . . . . . . . . . . 14
339	338	rpcnne0d 11350	. . . . . . . . . . . . 13 $/\$
340		divdiv1 10318	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
341	129, 328, 339, 340	syl3anc 1264	. . . . . . . . . . . 12
342	341	eqcomd 2430	. . . . . . . . . . 11
343	342	oveq2d 6317	. . . . . . . . . 10
344	65	a1i 11	. . . . . . . . . . 11
345	327	rpcnd 11343	. . . . . . . . . . . 12
346	327	rpne0d 11346	. . . . . . . . . . . 12
347	345, 346	reccld 10376	. . . . . . . . . . 11
348	338	rpcnd 11343	. . . . . . . . . . 11
349	338	rpne0d 11346	. . . . . . . . . . 11
350	344, 347, 348, 349	divassd 10418	. . . . . . . . . 10
351	139, 268	eqnetrrd 2718	. . . . . . . . . . . . 13
352	201, 199, 201, 213, 351, 224	divmuldivd 10424	. . . . . . . . . . . 12
353	352	oveq2d 6317	. . . . . . . . . . 11
354	344, 347	mulcld 9663	. . . . . . . . . . . . 13
355	201, 201	mulcld 9663	. . . . . . . . . . . . 13
356	199, 213	mulcld 9663	. . . . . . . . . . . . 13
357	201, 201, 205, 205	mulne0d 10264	. . . . . . . . . . . . 13
358	199, 213, 351, 224	mulne0d 10264	. . . . . . . . . . . . 13
359	354, 355, 356, 357, 358	divdiv2d 10415	. . . . . . . . . . . 12
360	354, 356, 355, 357	divassd 10418	. . . . . . . . . . . 12
361	359, 360	eqtrd 2463	. . . . . . . . . . 11
362	199, 201, 201, 213, 205, 224, 205	divdivdivd 10430	. . . . . . . . . . . . 13
363	362	eqcomd 2430	. . . . . . . . . . . 12
364	363	oveq2d 6317	. . . . . . . . . . 11
365	353, 361, 364	3eqtrd 2467	. . . . . . . . . 10
366	343, 350, 365	3eqtr2d 2469	. . . . . . . . 9
367	61	a1i 11	. . . . . . . . . . . 12
368	367	halfcld 10857	. . . . . . . . . . 11
369	368, 347	mulcld 9663	. . . . . . . . . 10
370	206, 225, 226	divcld 10383	. . . . . . . . . 10
371	369, 370	mulcomd 9664	. . . . . . . . 9
372	284, 366, 371	3eqtrd 2467	. . . . . . . 8
373	278, 372	eqtrd 2463	. . . . . . 7
374	373	adantr 466	. . . . . 6 $/\$
375	126, 247, 374	3eqtr4d 2473	. . . . 5 $/\$
376	375	ex 435	. . . 4
377	9, 18, 27, 36, 124, 376	nnind 10627	. . 3
378	377	mpteq2ia 4503	. 2
379		wallispilem4.3	. 2
380		wallispilem4.4	. 2
381	378, 379, 380	3eqtr4i 2461	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 370

wceq 1437

wcel 1868

wne 2618 class class class wbr 4420

cmpt 4479

cfv 5597 (class class class)co 6301

cc 9537

cr 9538

cc0 9539

c1 9540

caddc 9542

cmul 9544

clt 9675

cle 9676

cmin 9860

cdiv 10269

cn 10609

c2 10659

c3 10660

cn0 10869

cz 10937

cuz 11159

crp 11302

cioo 11635

cfz 11784

cseq 12212

cexp 12271

csin 14103

cpi 14106

citg 22562

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4551 ax-pow 4598 ax-pr 4656 ax-un 6593 ax-inf2 8148 ax-cc 8865 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 ax-addf 9618 ax-mulf 9619

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-int 4253 df-iun 4298 df-iin 4299 df-disj 4392 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4760 df-id 4764 df-po 4770 df-so 4771 df-fr 4808 df-se 4809 df-we 4810 df-xp 4855 df-rel 4856 df-cnv 4857 df-co 4858 df-dm 4859 df-rn 4860 df-res 4861 df-ima 4862 df-pred 5395 df-ord 5441 df-on 5442 df-lim 5443 df-suc 5444 df-iota 5561 df-fun 5599 df-fn 5600 df-f 5601 df-f1 5602 df-fo 5603 df-f1o 5604 df-fv 5605 df-isom 5606 df-riota 6263 df-ov 6304 df-oprab 6305 df-mpt2 6306 df-of 6541 df-ofr 6542 df-om 6703 df-1st 6803 df-2nd 6804 df-supp 6922 df-wrecs 7032 df-recs 7094 df-rdg 7132 df-1o 7186 df-2o 7187 df-oadd 7190 df-omul 7191 df-er 7367 df-map 7478 df-pm 7479 df-ixp 7527 df-en 7574 df-dom 7575 df-sdom 7576 df-fin 7577 df-fsupp 7886 df-fi 7927 df-sup 7958 df-inf 7959 df-oi 8027 df-card 8374 df-acn 8377 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ioc 11640 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12027 df-mod 12096 df-seq 12213 df-exp 12272 df-fac 12459 df-bc 12487 df-hash 12515 df-shft 13118 df-cj 13150 df-re 13151 df-im 13152 df-sqrt 13286 df-abs 13287 df-limsup 13513 df-clim 13539 df-rlim 13540 df-sum 13740 df-ef 14108 df-sin 14110 df-cos 14111 df-pi 14113 df-struct 15110 df-ndx 15111 df-slot 15112 df-base 15113 df-sets 15114 df-ress 15115 df-plusg 15190 df-mulr 15191 df-starv 15192 df-sca 15193 df-vsca 15194 df-ip 15195 df-tset 15196 df-ple 15197 df-ds 15199 df-unif 15200 df-hom 15201 df-cco 15202 df-rest 15308 df-topn 15309 df-0g 15327 df-gsum 15328 df-topgen 15329 df-pt 15330 df-prds 15333 df-xrs 15387 df-qtop 15393 df-imas 15394 df-xps 15397 df-mre 15479 df-mrc 15480 df-acs 15482 df-mgm 16475 df-sgrp 16514 df-mnd 16524 df-submnd 16570 df-mulg 16663 df-cntz 16958 df-cmn 17419 df-psmet 18949 df-xmet 18950 df-met 18951 df-bl 18952 df-mopn 18953 df-fbas 18954 df-fg 18955 df-cnfld 18958 df-top 19907 df-bases 19908 df-topon 19909 df-topsp 19910 df-cld 20020 df-ntr 20021 df-cls 20022 df-nei 20100 df-lp 20138 df-perf 20139 df-cn 20229 df-cnp 20230 df-haus 20317 df-cmp 20388 df-tx 20563 df-hmeo 20756 df-fil 20847 df-fm 20939 df-flim 20940 df-flf 20941 df-xms 21321 df-ms 21322 df-tms 21323 df-cncf 21896 df-ovol 22402 df-vol 22404 df-mbf 22563 df-itg1 22564 df-itg2 22565 df-ibl 22566 df-itg 22567 df-0p 22614 df-limc 22807 df-dv 22808

This theorem is referenced by: wallispilem5 37750

W3C validator