wallispilem4 - Mathbox for Glauco Siliprandi

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

Theorem wallispilem4 37930

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 6298	. . . . . . 7
2	1	fveq2d 5869	. . . . . 6
3	1	oveq1d 6305	. . . . . . 7
4	3	fveq2d 5869	. . . . . 6
5	2, 4	oveq12d 6308	. . . . 5
6		fveq2 5865	. . . . . . 7
7	6	oveq2d 6306	. . . . . 6
8	7	oveq2d 6306	. . . . 5
9	5, 8	eqeq12d 2466	. . . 4
10		oveq2 6298	. . . . . . 7
11	10	fveq2d 5869	. . . . . 6
12	10	oveq1d 6305	. . . . . . 7
13	12	fveq2d 5869	. . . . . 6
14	11, 13	oveq12d 6308	. . . . 5
15		fveq2 5865	. . . . . . 7
16	15	oveq2d 6306	. . . . . 6
17	16	oveq2d 6306	. . . . 5
18	14, 17	eqeq12d 2466	. . . 4
19		oveq2 6298	. . . . . . 7
20	19	fveq2d 5869	. . . . . 6
21	19	oveq1d 6305	. . . . . . 7
22	21	fveq2d 5869	. . . . . 6
23	20, 22	oveq12d 6308	. . . . 5
24		fveq2 5865	. . . . . . 7
25	24	oveq2d 6306	. . . . . 6
26	25	oveq2d 6306	. . . . 5
27	23, 26	eqeq12d 2466	. . . 4
28		oveq2 6298	. . . . . . 7
29	28	fveq2d 5869	. . . . . 6
30	28	oveq1d 6305	. . . . . . 7
31	30	fveq2d 5869	. . . . . 6
32	29, 31	oveq12d 6308	. . . . 5
33		fveq2 5865	. . . . . . 7
34	33	oveq2d 6306	. . . . . 6
35	34	oveq2d 6306	. . . . 5
36	32, 35	eqeq12d 2466	. . . 4
37		2t1e2 10758	. . . . . . 7
38	37	fveq2i 5868	. . . . . 6
39	37	oveq1i 6300	. . . . . . . 8
40		2p1e3 10733	. . . . . . . 8
41	39, 40	eqtri 2473	. . . . . . 7
42	41	fveq2i 5868	. . . . . 6
43	38, 42	oveq12i 6302	. . . . 5
44		2z 10969	. . . . . . . . 9
45		uzid 11173	. . . . . . . . 9
46	44, 45	ax-mp 5	. . . . . . . 8
47		wallispilem4.2	. . . . . . . . . 10
48	47	wallispilem2 37928	. . . . . . . . 9 $/\$ $/\$
49	48	simp3i 1019	. . . . . . . 8
50	46, 49	ax-mp 5	. . . . . . 7
51		2m1e1 10724	. . . . . . . . 9
52	51	oveq1i 6300	. . . . . . . 8
53		2cn 10680	. . . . . . . . . . 11
54	53	subidi 9945	. . . . . . . . . 10
55	54	fveq2i 5868	. . . . . . . . 9
56	48	simp1i 1017	. . . . . . . . 9
57	55, 56	eqtri 2473	. . . . . . . 8
58	52, 57	oveq12i 6302	. . . . . . 7
59		ax-1cn 9597	. . . . . . . . 9
60		2cnne0 10824	. . . . . . . . 9 $/\$
61		picn 23414	. . . . . . . . 9
62		div32 10290	. . . . . . . . 9 $/\$ $/\$ $/\$
63	59, 60, 61, 62	mp3an 1364	. . . . . . . 8
64		2ne0 10702	. . . . . . . . . 10
65	61, 53, 64	divcli 10349	. . . . . . . . 9
66	65	mulid2i 9646	. . . . . . . 8
67	63, 66	eqtri 2473	. . . . . . 7
68	50, 58, 67	3eqtri 2477	. . . . . 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 1190	. . . . . . . 8
76	47	wallispilem2 37928	. . . . . . . . 9 $/\$ $/\$
77	76	simp3i 1019	. . . . . . . 8
78	75, 77	ax-mp 5	. . . . . . 7
79		3m1e2 10726	. . . . . . . . . 10
80	79	eqcomi 2460	. . . . . . . . 9
81	80	oveq1i 6300	. . . . . . . 8
82		3cn 10684	. . . . . . . . . . 11
83	82, 53, 59, 40	subaddrii 9964	. . . . . . . . . 10
84	83	fveq2i 5868	. . . . . . . . 9
85	48	simp2i 1018	. . . . . . . . 9
86	84, 85	eqtr2i 2474	. . . . . . . 8
87	81, 86	oveq12i 6302	. . . . . . 7
88		3ne0 10704	. . . . . . . . 9
89	53, 82, 88	divcli 10349	. . . . . . . 8
90	89, 53	mulcomi 9649	. . . . . . 7
91	78, 87, 90	3eqtr2i 2479	. . . . . 6
92	68, 91	oveq12i 6302	. . . . 5
93		1z 10967	. . . . . . . . 9
94		seq1 12226	. . . . . . . . 9
95	93, 94	ax-mp 5	. . . . . . . 8
96		1nn 10620	. . . . . . . . 9
97		oveq2 6298	. . . . . . . . . . . . . 14
98	97, 37	syl6eq 2501	. . . . . . . . . . . . 13
99	97	oveq1d 6305	. . . . . . . . . . . . . 14
100	37	oveq1i 6300	. . . . . . . . . . . . . . 15
101	100, 51	eqtri 2473	. . . . . . . . . . . . . 14
102	99, 101	syl6eq 2501	. . . . . . . . . . . . 13
103	98, 102	oveq12d 6308	. . . . . . . . . . . 12
104	53	div1i 10335	. . . . . . . . . . . 12
105	103, 104	syl6eq 2501	. . . . . . . . . . 11
106	98	oveq1d 6305	. . . . . . . . . . . . 13
107	106, 40	syl6eq 2501	. . . . . . . . . . . 12
108	98, 107	oveq12d 6308	. . . . . . . . . . 11
109	105, 108	oveq12d 6308	. . . . . . . . . 10
110		wallispilem4.1	. . . . . . . . . 10
111		ovex 6318	. . . . . . . . . 10
112	109, 110, 111	fvmpt 5948	. . . . . . . . 9
113	96, 112	ax-mp 5	. . . . . . . 8
114	95, 113	eqtr2i 2474	. . . . . . 7
115	114	oveq2i 6301	. . . . . 6
116	53, 89	mulcli 9648	. . . . . . . . 9
117	113, 116	eqeltri 2525	. . . . . . . 8
118	95, 117	eqeltri 2525	. . . . . . 7
119	53, 82, 64, 88	divne0i 10355	. . . . . . . . 9
120	53, 89, 64, 119	mulne0i 10255	. . . . . . . 8
121	114, 120	eqnetrri 2695	. . . . . . 7
122	65, 118, 121	divreci 10352	. . . . . 6
123	115, 122	eqtri 2473	. . . . 5
124	43, 92, 123	3eqtri 2477	. . . 4
125		oveq2 6298	. . . . . . 7
126	125	adantl 468	. . . . . 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 6306	. . . . . . . . . . . . . . 15
133	130, 132	eqtrd 2485	. . . . . . . . . . . . . 14
134	133	oveq1d 6305	. . . . . . . . . . . . 13
135	127, 128	mulcld 9663	. . . . . . . . . . . . . 14
136	135, 127, 129	addsubassd 10006	. . . . . . . . . . . . 13
137	51	a1i 11	. . . . . . . . . . . . . 14
138	137	oveq2d 6306	. . . . . . . . . . . . 13
139	134, 136, 138	3eqtrd 2489	. . . . . . . . . . . 12
140	139	oveq1d 6305	. . . . . . . . . . 11
141	140	oveq1d 6305	. . . . . . . . . 10
142	79	a1i 11	. . . . . . . . . . . . . 14
143	142	oveq2d 6306	. . . . . . . . . . . . 13
144	82	a1i 11	. . . . . . . . . . . . . 14
145	135, 144, 129	addsubassd 10006	. . . . . . . . . . . . 13
146	143, 145, 133	3eqtr4d 2495	. . . . . . . . . . . 12
147	146	oveq1d 6305	. . . . . . . . . . 11
148	147	oveq1d 6305	. . . . . . . . . 10
149	141, 148	oveq12d 6308	. . . . . . . . 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 214	. . . . . . . . . . . . . 14
164	154, 157, 159, 163	lemulge11d 10544	. . . . . . . . . . . . 13
165	44	eluz1i 11166	. . . . . . . . . . . . 13 $/\$
166	153, 164, 165	sylanbrc 670	. . . . . . . . . . . 12
167	47, 166	itgsinexp 37831	. . . . . . . . . . 11
168	133	oveq1d 6305	. . . . . . . . . . . . . 14
169	135, 127	pncand 9987	. . . . . . . . . . . . . 14
170	168, 169	eqtrd 2485	. . . . . . . . . . . . 13
171	170	fveq2d 5869	. . . . . . . . . . . 12
172	171	oveq2d 6306	. . . . . . . . . . 11
173	167, 172	eqtrd 2485	. . . . . . . . . 10
174	133	oveq1d 6305	. . . . . . . . . . . . 13
175	135, 127, 129	addassd 9665	. . . . . . . . . . . . 13
176	40	a1i 11	. . . . . . . . . . . . . 14
177	176	oveq2d 6306	. . . . . . . . . . . . 13
178	174, 175, 177	3eqtrd 2489	. . . . . . . . . . . 12
179	178	fveq2d 5869	. . . . . . . . . . 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 215	. . . . . . . . . . . . . 14
193	154, 183, 185, 187, 192	letrd 9792	. . . . . . . . . . . . 13
194	44	eluz1i 11166	. . . . . . . . . . . . 13 $/\$
195	182, 193, 194	sylanbrc 670	. . . . . . . . . . . 12
196	47, 195	itgsinexp 37831	. . . . . . . . . . 11
197	179, 196	eqtrd 2485	. . . . . . . . . 10
198	173, 197	oveq12d 6308	. . . . . . . . 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 37929	. . . . . . . . . . . 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 541	. . . . . . . . . . . . . . . 16 $/\$
220		elrp 11304	. . . . . . . . . . . . . . . 16 $/\$
221	219, 220	sylibr 216	. . . . . . . . . . . . . . 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 236	. . . . . . . . . . . . . 14
230		elnn0z 10950	. . . . . . . . . . . . . 14 $/\$
231	227, 229, 230	sylanbrc 670	. . . . . . . . . . . . 13
232	47	wallispilem3 37929	. . . . . . . . . . . . 13
233	231, 232	syl 17	. . . . . . . . . . . 12
234	233	rpcnne0d 11350	. . . . . . . . . . 11 $/\$
235	225, 226, 234	jca31 537	. . . . . . . . . 10 $/\$ $/\$ $/\$
236		divmuldiv 10307	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
237	206, 212, 235, 236	syl21anc 1267	. . . . . . . . 9
238	149, 198, 237	3eqtr4d 2495	. . . . . . . 8
239	135, 144, 127	addsubassd 10006	. . . . . . . . . . . 12
240	83	a1i 11	. . . . . . . . . . . . 13
241	240	oveq2d 6306	. . . . . . . . . . . 12
242	239, 241	eqtrd 2485	. . . . . . . . . . 11
243	242	fveq2d 5869	. . . . . . . . . 10
244	243	oveq2d 6306	. . . . . . . . 9
245	244	oveq2d 6306	. . . . . . . 8
246	238, 245	eqtrd 2485	. . . . . . 7
247	246	adantr 467	. . . . . 6 $/\$
248		elnnuz 11195	. . . . . . . . . . . . 13
249	248	biimpi 198	. . . . . . . . . . . 12
250		seqp1 12228	. . . . . . . . . . . 12
251	249, 250	syl 17	. . . . . . . . . . 11
252	110	a1i 11	. . . . . . . . . . . . 13
253		oveq2 6298	. . . . . . . . . . . . . . . 16
254	253	oveq1d 6305	. . . . . . . . . . . . . . . 16
255	253, 254	oveq12d 6308	. . . . . . . . . . . . . . 15
256	253	oveq1d 6305	. . . . . . . . . . . . . . . 16
257	253, 256	oveq12d 6308	. . . . . . . . . . . . . . 15
258	255, 257	oveq12d 6308	. . . . . . . . . . . . . 14
259	258	adantl 468	. . . . . . . . . . . . 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 2529	. . . . . . . . . . . . . . 15
271	178, 224	eqnetrd 2691	. . . . . . . . . . . . . . 15
272	260, 270, 271	redivcld 10435	. . . . . . . . . . . . . 14
273	269, 272	remulcld 9671	. . . . . . . . . . . . 13
274	252, 259, 203, 273	fvmptd 5954	. . . . . . . . . . . 12
275	274	oveq2d 6306	. . . . . . . . . . 11
276	251, 275	eqtrd 2485	. . . . . . . . . 10
277	276	oveq2d 6306	. . . . . . . . 9
278	277	oveq2d 6306	. . . . . . . 8
279	139	oveq2d 6306	. . . . . . . . . . . . 13
280	178	oveq2d 6306	. . . . . . . . . . . . 13
281	279, 280	oveq12d 6308	. . . . . . . . . . . 12
282	281	oveq2d 6306	. . . . . . . . . . 11
283	282	oveq2d 6306	. . . . . . . . . 10
284	283	oveq2d 6306	. . . . . . . . 9
285		elfznn 11828	. . . . . . . . . . . . . . . . 17
286	285	adantl 468	. . . . . . . . . . . . . . . 16 $/\$
287	110	a1i 11	. . . . . . . . . . . . . . . . . 18
288		oveq2 6298	. . . . . . . . . . . . . . . . . . . . 21
289	288	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . 21
290	288, 289	oveq12d 6308	. . . . . . . . . . . . . . . . . . . 20
291	288	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . 21
292	288, 291	oveq12d 6308	. . . . . . . . . . . . . . . . . . . 20
293	290, 292	oveq12d 6308	. . . . . . . . . . . . . . . . . . 19
294	293	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$
295		id 22	. . . . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . . . . . . . . . . 24
310	307, 309	eqbrtrrd 4425	. . . . . . . . . . . . . . . . . . . . . . 23
311	303, 301, 302, 305, 310	lelttrd 9793	. . . . . . . . . . . . . . . . . . . . . 22
312	303, 302	posdifd 10200	. . . . . . . . . . . . . . . . . . . . . 22
313	311, 312	mpbid 214	. . . . . . . . . . . . . . . . . . . . 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 5954	. . . . . . . . . . . . . . . . 17
323	322, 321	eqeltrd 2529	. . . . . . . . . . . . . . . 16
324	286, 323	syl 17	. . . . . . . . . . . . . . 15 $/\$
325		rpmulcl 11324	. . . . . . . . . . . . . . . 16 $/\$
326	325	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
327	249, 324, 326	seqcl 12233	. . . . . . . . . . . . . 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 1268	. . . . . . . . . . . 12
342	341	eqcomd 2457	. . . . . . . . . . 11
343	342	oveq2d 6306	. . . . . . . . . 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 2692	. . . . . . . . . . . . 13
352	201, 199, 201, 213, 351, 224	divmuldivd 10424	. . . . . . . . . . . 12
353	352	oveq2d 6306	. . . . . . . . . . 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 2485	. . . . . . . . . . 11
362	199, 201, 201, 213, 205, 224, 205	divdivdivd 10430	. . . . . . . . . . . . 13
363	362	eqcomd 2457	. . . . . . . . . . . 12
364	363	oveq2d 6306	. . . . . . . . . . 11
365	353, 361, 364	3eqtrd 2489	. . . . . . . . . 10
366	343, 350, 365	3eqtr2d 2491	. . . . . . . . 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 2489	. . . . . . . 8
373	278, 372	eqtrd 2485	. . . . . . 7
374	373	adantr 467	. . . . . 6 $/\$
375	126, 247, 374	3eqtr4d 2495	. . . . 5 $/\$
376	375	ex 436	. . . 4
377	9, 18, 27, 36, 124, 376	nnind 10627	. . 3
378	377	mpteq2ia 4485	. 2
379		wallispilem4.3	. 2
380		wallispilem4.4	. 2
381	378, 379, 380	3eqtr4i 2483	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 371

wceq 1444

wcel 1887

wne 2622 class class class wbr 4402

cmpt 4461

cfv 5582 (class class class)co 6290

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 12213

cexp 12272

csin 14116

cpi 14119

citg 22576

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 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 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-iin 4281 df-disj 4374 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-ofr 6532 df-om 6693 df-1st 6793 df-2nd 6794 df-supp 6915 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-omul 7187 df-er 7363 df-map 7474 df-pm 7475 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fsupp 7884 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-acn 8376 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 12028 df-mod 12097 df-seq 12214 df-exp 12273 df-fac 12460 df-bc 12488 df-hash 12516 df-shft 13130 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-limsup 13526 df-clim 13552 df-rlim 13553 df-sum 13753 df-ef 14121 df-sin 14123 df-cos 14124 df-pi 14126 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-starv 15205 df-sca 15206 df-vsca 15207 df-ip 15208 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-hom 15214 df-cco 15215 df-rest 15321 df-topn 15322 df-0g 15340 df-gsum 15341 df-topgen 15342 df-pt 15343 df-prds 15346 df-xrs 15400 df-qtop 15406 df-imas 15407 df-xps 15410 df-mre 15492 df-mrc 15493 df-acs 15495 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-submnd 16583 df-mulg 16676 df-cntz 16971 df-cmn 17432 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-fbas 18967 df-fg 18968 df-cnfld 18971 df-top 19921 df-bases 19922 df-topon 19923 df-topsp 19924 df-cld 20034 df-ntr 20035 df-cls 20036 df-nei 20114 df-lp 20152 df-perf 20153 df-cn 20243 df-cnp 20244 df-haus 20331 df-cmp 20402 df-tx 20577 df-hmeo 20770 df-fil 20861 df-fm 20953 df-flim 20954 df-flf 20955 df-xms 21335 df-ms 21336 df-tms 21337 df-cncf 21910 df-ovol 22416 df-vol 22418 df-mbf 22577 df-itg1 22578 df-itg2 22579 df-ibl 22580 df-itg 22581 df-0p 22628 df-limc 22821 df-dv 22822

This theorem is referenced by: wallispilem5 37931

W3C validator