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 38042

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 6316	. . . . . . 7
2	1	fveq2d 5883	. . . . . 6
3	1	oveq1d 6323	. . . . . . 7
4	3	fveq2d 5883	. . . . . 6
5	2, 4	oveq12d 6326	. . . . 5
6		fveq2 5879	. . . . . . 7
7	6	oveq2d 6324	. . . . . 6
8	7	oveq2d 6324	. . . . 5
9	5, 8	eqeq12d 2486	. . . 4
10		oveq2 6316	. . . . . . 7
11	10	fveq2d 5883	. . . . . 6
12	10	oveq1d 6323	. . . . . . 7
13	12	fveq2d 5883	. . . . . 6
14	11, 13	oveq12d 6326	. . . . 5
15		fveq2 5879	. . . . . . 7
16	15	oveq2d 6324	. . . . . 6
17	16	oveq2d 6324	. . . . 5
18	14, 17	eqeq12d 2486	. . . 4
19		oveq2 6316	. . . . . . 7
20	19	fveq2d 5883	. . . . . 6
21	19	oveq1d 6323	. . . . . . 7
22	21	fveq2d 5883	. . . . . 6
23	20, 22	oveq12d 6326	. . . . 5
24		fveq2 5879	. . . . . . 7
25	24	oveq2d 6324	. . . . . 6
26	25	oveq2d 6324	. . . . 5
27	23, 26	eqeq12d 2486	. . . 4
28		oveq2 6316	. . . . . . 7
29	28	fveq2d 5883	. . . . . 6
30	28	oveq1d 6323	. . . . . . 7
31	30	fveq2d 5883	. . . . . 6
32	29, 31	oveq12d 6326	. . . . 5
33		fveq2 5879	. . . . . . 7
34	33	oveq2d 6324	. . . . . 6
35	34	oveq2d 6324	. . . . 5
36	32, 35	eqeq12d 2486	. . . 4
37		2t1e2 10781	. . . . . . 7
38	37	fveq2i 5882	. . . . . 6
39	37	oveq1i 6318	. . . . . . . 8
40		2p1e3 10756	. . . . . . . 8
41	39, 40	eqtri 2493	. . . . . . 7
42	41	fveq2i 5882	. . . . . 6
43	38, 42	oveq12i 6320	. . . . 5
44		2z 10993	. . . . . . . . 9
45		uzid 11197	. . . . . . . . 9
46	44, 45	ax-mp 5	. . . . . . . 8
47		wallispilem4.2	. . . . . . . . . 10
48	47	wallispilem2 38040	. . . . . . . . 9 $/\$ $/\$
49	48	simp3i 1041	. . . . . . . 8
50	46, 49	ax-mp 5	. . . . . . 7
51		2m1e1 10746	. . . . . . . . 9
52	51	oveq1i 6318	. . . . . . . 8
53		2cn 10702	. . . . . . . . . . 11
54	53	subidi 9965	. . . . . . . . . 10
55	54	fveq2i 5882	. . . . . . . . 9
56	48	simp1i 1039	. . . . . . . . 9
57	55, 56	eqtri 2493	. . . . . . . 8
58	52, 57	oveq12i 6320	. . . . . . 7
59		ax-1cn 9615	. . . . . . . . 9
60		2cnne0 10847	. . . . . . . . 9 $/\$
61		picn 23493	. . . . . . . . 9
62		div32 10312	. . . . . . . . 9 $/\$ $/\$ $/\$
63	59, 60, 61, 62	mp3an 1390	. . . . . . . 8
64		2ne0 10724	. . . . . . . . . 10
65	61, 53, 64	divcli 10371	. . . . . . . . 9
66	65	mulid2i 9664	. . . . . . . 8
67	63, 66	eqtri 2493	. . . . . . 7
68	50, 58, 67	3eqtri 2497	. . . . . 6
69		3z 10994	. . . . . . . . 9
70		2re 10701	. . . . . . . . . 10
71		3re 10705	. . . . . . . . . 10
72		2lt3 10800	. . . . . . . . . 10
73	70, 71, 72	ltleii 9775	. . . . . . . . 9
74		eluz2 11188	. . . . . . . . 9 $/\$ $/\$
75	44, 69, 73, 74	mpbir3an 1212	. . . . . . . 8
76	47	wallispilem2 38040	. . . . . . . . 9 $/\$ $/\$
77	76	simp3i 1041	. . . . . . . 8
78	75, 77	ax-mp 5	. . . . . . 7
79		3m1e2 10748	. . . . . . . . . 10
80	79	eqcomi 2480	. . . . . . . . 9
81	80	oveq1i 6318	. . . . . . . 8
82		3cn 10706	. . . . . . . . . . 11
83	82, 53, 59, 40	subaddrii 9983	. . . . . . . . . 10
84	83	fveq2i 5882	. . . . . . . . 9
85	48	simp2i 1040	. . . . . . . . 9
86	84, 85	eqtr2i 2494	. . . . . . . 8
87	81, 86	oveq12i 6320	. . . . . . 7
88		3ne0 10726	. . . . . . . . 9
89	53, 82, 88	divcli 10371	. . . . . . . 8
90	89, 53	mulcomi 9667	. . . . . . 7
91	78, 87, 90	3eqtr2i 2499	. . . . . 6
92	68, 91	oveq12i 6320	. . . . 5
93		1z 10991	. . . . . . . . 9
94		seq1 12264	. . . . . . . . 9
95	93, 94	ax-mp 5	. . . . . . . 8
96		1nn 10642	. . . . . . . . 9
97		oveq2 6316	. . . . . . . . . . . . . 14
98	97, 37	syl6eq 2521	. . . . . . . . . . . . 13
99	97	oveq1d 6323	. . . . . . . . . . . . . 14
100	37	oveq1i 6318	. . . . . . . . . . . . . . 15
101	100, 51	eqtri 2493	. . . . . . . . . . . . . 14
102	99, 101	syl6eq 2521	. . . . . . . . . . . . 13
103	98, 102	oveq12d 6326	. . . . . . . . . . . 12
104	53	div1i 10357	. . . . . . . . . . . 12
105	103, 104	syl6eq 2521	. . . . . . . . . . 11
106	98	oveq1d 6323	. . . . . . . . . . . . 13
107	106, 40	syl6eq 2521	. . . . . . . . . . . 12
108	98, 107	oveq12d 6326	. . . . . . . . . . 11
109	105, 108	oveq12d 6326	. . . . . . . . . 10
110		wallispilem4.1	. . . . . . . . . 10
111		ovex 6336	. . . . . . . . . 10
112	109, 110, 111	fvmpt 5963	. . . . . . . . 9
113	96, 112	ax-mp 5	. . . . . . . 8
114	95, 113	eqtr2i 2494	. . . . . . 7
115	114	oveq2i 6319	. . . . . 6
116	53, 89	mulcli 9666	. . . . . . . . 9
117	113, 116	eqeltri 2545	. . . . . . . 8
118	95, 117	eqeltri 2545	. . . . . . 7
119	53, 82, 64, 88	divne0i 10377	. . . . . . . . 9
120	53, 89, 64, 119	mulne0i 10277	. . . . . . . 8
121	114, 120	eqnetrri 2714	. . . . . . 7
122	65, 118, 121	divreci 10374	. . . . . 6
123	115, 122	eqtri 2493	. . . . 5
124	43, 92, 123	3eqtri 2497	. . . 4
125		oveq2 6316	. . . . . . 7
126	125	adantl 473	. . . . . 6 $/\$
127		2cnd 10704	. . . . . . . . . . . . . . . 16
128		nncn 10639	. . . . . . . . . . . . . . . 16
129	59	a1i 11	. . . . . . . . . . . . . . . 16
130	127, 128, 129	adddid 9685	. . . . . . . . . . . . . . 15
131	127	mulid1d 9678	. . . . . . . . . . . . . . . 16
132	131	oveq2d 6324	. . . . . . . . . . . . . . 15
133	130, 132	eqtrd 2505	. . . . . . . . . . . . . 14
134	133	oveq1d 6323	. . . . . . . . . . . . 13
135	127, 128	mulcld 9681	. . . . . . . . . . . . . 14
136	135, 127, 129	addsubassd 10025	. . . . . . . . . . . . 13
137	51	a1i 11	. . . . . . . . . . . . . 14
138	137	oveq2d 6324	. . . . . . . . . . . . 13
139	134, 136, 138	3eqtrd 2509	. . . . . . . . . . . 12
140	139	oveq1d 6323	. . . . . . . . . . 11
141	140	oveq1d 6323	. . . . . . . . . 10
142	79	a1i 11	. . . . . . . . . . . . . 14
143	142	oveq2d 6324	. . . . . . . . . . . . 13
144	82	a1i 11	. . . . . . . . . . . . . 14
145	135, 144, 129	addsubassd 10025	. . . . . . . . . . . . 13
146	143, 145, 133	3eqtr4d 2515	. . . . . . . . . . . 12
147	146	oveq1d 6323	. . . . . . . . . . 11
148	147	oveq1d 6323	. . . . . . . . . 10
149	141, 148	oveq12d 6326	. . . . . . . . 9
150	44	a1i 11	. . . . . . . . . . . . . 14
151		nnz 10983	. . . . . . . . . . . . . . 15
152	151	peano2zd 11066	. . . . . . . . . . . . . 14
153	150, 152	zmulcld 11069	. . . . . . . . . . . . 13
154	70	a1i 11	. . . . . . . . . . . . . 14
155		nnre 10638	. . . . . . . . . . . . . . 15
156		1red 9676	. . . . . . . . . . . . . . 15
157	155, 156	readdcld 9688	. . . . . . . . . . . . . 14
158		0le2 10722	. . . . . . . . . . . . . . 15
159	158	a1i 11	. . . . . . . . . . . . . 14
160		nnnn0 10900	. . . . . . . . . . . . . . . 16
161	160	nn0ge0d 10952	. . . . . . . . . . . . . . 15
162	156, 155	addge02d 10223	. . . . . . . . . . . . . . 15
163	161, 162	mpbid 215	. . . . . . . . . . . . . 14
164	154, 157, 159, 163	lemulge11d 10566	. . . . . . . . . . . . 13
165	44	eluz1i 11190	. . . . . . . . . . . . 13 $/\$
166	153, 164, 165	sylanbrc 677	. . . . . . . . . . . 12
167	47, 166	itgsinexp 37928	. . . . . . . . . . 11
168	133	oveq1d 6323	. . . . . . . . . . . . . 14
169	135, 127	pncand 10006	. . . . . . . . . . . . . 14
170	168, 169	eqtrd 2505	. . . . . . . . . . . . 13
171	170	fveq2d 5883	. . . . . . . . . . . 12
172	171	oveq2d 6324	. . . . . . . . . . 11
173	167, 172	eqtrd 2505	. . . . . . . . . 10
174	133	oveq1d 6323	. . . . . . . . . . . . 13
175	135, 127, 129	addassd 9683	. . . . . . . . . . . . 13
176	40	a1i 11	. . . . . . . . . . . . . 14
177	176	oveq2d 6324	. . . . . . . . . . . . 13
178	174, 175, 177	3eqtrd 2509	. . . . . . . . . . . 12
179	178	fveq2d 5883	. . . . . . . . . . 11
180	150, 151	zmulcld 11069	. . . . . . . . . . . . . 14
181	69	a1i 11	. . . . . . . . . . . . . 14
182	180, 181	zaddcld 11067	. . . . . . . . . . . . 13
183	154, 155	remulcld 9689	. . . . . . . . . . . . . 14
184	71	a1i 11	. . . . . . . . . . . . . . 15
185	183, 184	readdcld 9688	. . . . . . . . . . . . . 14
186		nnge1 10657	. . . . . . . . . . . . . . 15
187	154, 155, 159, 186	lemulge11d 10566	. . . . . . . . . . . . . 14
188		0re 9661	. . . . . . . . . . . . . . . 16
189		3pos 10725	. . . . . . . . . . . . . . . 16
190	188, 71, 189	ltleii 9775	. . . . . . . . . . . . . . 15
191	183, 184	addge01d 10222	. . . . . . . . . . . . . . 15
192	190, 191	mpbii 216	. . . . . . . . . . . . . 14
193	154, 183, 185, 187, 192	letrd 9809	. . . . . . . . . . . . 13
194	44	eluz1i 11190	. . . . . . . . . . . . 13 $/\$
195	182, 193, 194	sylanbrc 677	. . . . . . . . . . . 12
196	47, 195	itgsinexp 37928	. . . . . . . . . . 11
197	179, 196	eqtrd 2505	. . . . . . . . . 10
198	173, 197	oveq12d 6326	. . . . . . . . 9
199	135, 129	addcld 9680	. . . . . . . . . . 11
200	128, 129	addcld 9680	. . . . . . . . . . . 12
201	127, 200	mulcld 9681	. . . . . . . . . . 11
202	64	a1i 11	. . . . . . . . . . . 12
203		peano2nn 10643	. . . . . . . . . . . . 13
204	203	nnne0d 10676	. . . . . . . . . . . 12
205	127, 200, 202, 204	mulne0d 10286	. . . . . . . . . . 11
206	199, 201, 205	divcld 10405	. . . . . . . . . 10
207		2nn0 10910	. . . . . . . . . . . . 13
208	207	a1i 11	. . . . . . . . . . . 12
209	208, 160	nn0mulcld 10954	. . . . . . . . . . 11
210	47	wallispilem3 38041	. . . . . . . . . . . 12
211	210	rpcnd 11366	. . . . . . . . . . 11
212	209, 211	syl 17	. . . . . . . . . 10
213	135, 144	addcld 9680	. . . . . . . . . . . 12
214		0red 9662	. . . . . . . . . . . . . 14
215		2pos 10723	. . . . . . . . . . . . . . . 16
216	215	a1i 11	. . . . . . . . . . . . . . 15
217		nngt0 10660	. . . . . . . . . . . . . . 15
218	154, 155, 216, 217	mulgt0d 9807	. . . . . . . . . . . . . 14
219	184, 189	jctir 547	. . . . . . . . . . . . . . . 16 $/\$
220		elrp 11327	. . . . . . . . . . . . . . . 16 $/\$
221	219, 220	sylibr 217	. . . . . . . . . . . . . . 15
222	183, 221	ltaddrpd 11394	. . . . . . . . . . . . . 14
223	214, 183, 185, 218, 222	lttrd 9813	. . . . . . . . . . . . 13
224	223	gt0ne0d 10199	. . . . . . . . . . . 12
225	201, 213, 224	divcld 10405	. . . . . . . . . . 11
226	201, 213, 205, 224	divne0d 10421	. . . . . . . . . . 11
227	182, 150	zsubcld 11068	. . . . . . . . . . . . . 14
228	185, 154	subge0d 10224	. . . . . . . . . . . . . . 15
229	193, 228	mpbird 240	. . . . . . . . . . . . . 14
230		elnn0z 10974	. . . . . . . . . . . . . 14 $/\$
231	227, 229, 230	sylanbrc 677	. . . . . . . . . . . . 13
232	47	wallispilem3 38041	. . . . . . . . . . . . 13
233	231, 232	syl 17	. . . . . . . . . . . 12
234	233	rpcnne0d 11373	. . . . . . . . . . 11 $/\$
235	225, 226, 234	jca31 543	. . . . . . . . . 10 $/\$ $/\$ $/\$
236		divmuldiv 10329	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
237	206, 212, 235, 236	syl21anc 1291	. . . . . . . . 9
238	149, 198, 237	3eqtr4d 2515	. . . . . . . 8
239	135, 144, 127	addsubassd 10025	. . . . . . . . . . . 12
240	83	a1i 11	. . . . . . . . . . . . 13
241	240	oveq2d 6324	. . . . . . . . . . . 12
242	239, 241	eqtrd 2505	. . . . . . . . . . 11
243	242	fveq2d 5883	. . . . . . . . . 10
244	243	oveq2d 6324	. . . . . . . . 9
245	244	oveq2d 6324	. . . . . . . 8
246	238, 245	eqtrd 2505	. . . . . . 7
247	246	adantr 472	. . . . . 6 $/\$
248		elnnuz 11219	. . . . . . . . . . . . 13
249	248	biimpi 199	. . . . . . . . . . . 12
250		seqp1 12266	. . . . . . . . . . . 12
251	249, 250	syl 17	. . . . . . . . . . 11
252	110	a1i 11	. . . . . . . . . . . . 13
253		oveq2 6316	. . . . . . . . . . . . . . . 16
254	253	oveq1d 6323	. . . . . . . . . . . . . . . 16
255	253, 254	oveq12d 6326	. . . . . . . . . . . . . . 15
256	253	oveq1d 6323	. . . . . . . . . . . . . . . 16
257	253, 256	oveq12d 6326	. . . . . . . . . . . . . . 15
258	255, 257	oveq12d 6326	. . . . . . . . . . . . . 14
259	258	adantl 473	. . . . . . . . . . . . 13 $/\$
260	154, 157	remulcld 9689	. . . . . . . . . . . . . . 15
261	260, 156	resubcld 10068	. . . . . . . . . . . . . . 15
262		1lt2 10799	. . . . . . . . . . . . . . . . . . 19
263	262	a1i 11	. . . . . . . . . . . . . . . . . 18
264		nnrp 11334	. . . . . . . . . . . . . . . . . . 19
265	156, 264	ltaddrp2d 11395	. . . . . . . . . . . . . . . . . 18
266	154, 157, 263, 265	mulgt1d 10565	. . . . . . . . . . . . . . . . 17
267	156, 266	gtned 9787	. . . . . . . . . . . . . . . 16
268	201, 129, 267	subne0d 10014	. . . . . . . . . . . . . . 15
269	260, 261, 268	redivcld 10457	. . . . . . . . . . . . . 14
270	178, 185	eqeltrd 2549	. . . . . . . . . . . . . . 15
271	178, 224	eqnetrd 2710	. . . . . . . . . . . . . . 15
272	260, 270, 271	redivcld 10457	. . . . . . . . . . . . . 14
273	269, 272	remulcld 9689	. . . . . . . . . . . . 13
274	252, 259, 203, 273	fvmptd 5969	. . . . . . . . . . . 12
275	274	oveq2d 6324	. . . . . . . . . . 11
276	251, 275	eqtrd 2505	. . . . . . . . . 10
277	276	oveq2d 6324	. . . . . . . . 9
278	277	oveq2d 6324	. . . . . . . 8
279	139	oveq2d 6324	. . . . . . . . . . . . 13
280	178	oveq2d 6324	. . . . . . . . . . . . 13
281	279, 280	oveq12d 6326	. . . . . . . . . . . 12
282	281	oveq2d 6324	. . . . . . . . . . 11
283	282	oveq2d 6324	. . . . . . . . . 10
284	283	oveq2d 6324	. . . . . . . . 9
285		elfznn 11854	. . . . . . . . . . . . . . . . 17
286	285	adantl 473	. . . . . . . . . . . . . . . 16 $/\$
287	110	a1i 11	. . . . . . . . . . . . . . . . . 18
288		oveq2 6316	. . . . . . . . . . . . . . . . . . . . 21
289	288	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . 21
290	288, 289	oveq12d 6326	. . . . . . . . . . . . . . . . . . . 20
291	288	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . 21
292	288, 291	oveq12d 6326	. . . . . . . . . . . . . . . . . . . 20
293	290, 292	oveq12d 6326	. . . . . . . . . . . . . . . . . . 19
294	293	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$
295		id 22	. . . . . . . . . . . . . . . . . 18
296		2rp 11330	. . . . . . . . . . . . . . . . . . . . . 22
297	296	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
298		nnrp 11334	. . . . . . . . . . . . . . . . . . . . 21
299	297, 298	rpmulcld 11380	. . . . . . . . . . . . . . . . . . . 20
300	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
301		nnre 10638	. . . . . . . . . . . . . . . . . . . . . . 23
302	300, 301	remulcld 9689	. . . . . . . . . . . . . . . . . . . . . 22
303		1red 9676	. . . . . . . . . . . . . . . . . . . . . 22
304	302, 303	resubcld 10068	. . . . . . . . . . . . . . . . . . . . 21
305		nnge1 10657	. . . . . . . . . . . . . . . . . . . . . . 23
306		nncn 10639	. . . . . . . . . . . . . . . . . . . . . . . . 25
307	306	mulid2d 9679	. . . . . . . . . . . . . . . . . . . . . . . 24
308	303, 300, 298	ltmul1d 11402	. . . . . . . . . . . . . . . . . . . . . . . . 25
309	262, 308	mpbii 216	. . . . . . . . . . . . . . . . . . . . . . . 24
310	307, 309	eqbrtrrd 4418	. . . . . . . . . . . . . . . . . . . . . . 23
311	303, 301, 302, 305, 310	lelttrd 9810	. . . . . . . . . . . . . . . . . . . . . 22
312	303, 302	posdifd 10221	. . . . . . . . . . . . . . . . . . . . . 22
313	311, 312	mpbid 215	. . . . . . . . . . . . . . . . . . . . 21
314	304, 313	elrpd 11361	. . . . . . . . . . . . . . . . . . . 20
315	299, 314	rpdivcld 11381	. . . . . . . . . . . . . . . . . . 19
316	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
317	298	rpge0d 11368	. . . . . . . . . . . . . . . . . . . . . 22
318	300, 301, 316, 317	mulge0d 10211	. . . . . . . . . . . . . . . . . . . . 21
319	302, 318	ge0p1rpd 11391	. . . . . . . . . . . . . . . . . . . 20
320	299, 319	rpdivcld 11381	. . . . . . . . . . . . . . . . . . 19
321	315, 320	rpmulcld 11380	. . . . . . . . . . . . . . . . . 18
322	287, 294, 295, 321	fvmptd 5969	. . . . . . . . . . . . . . . . 17
323	322, 321	eqeltrd 2549	. . . . . . . . . . . . . . . 16
324	286, 323	syl 17	. . . . . . . . . . . . . . 15 $/\$
325		rpmulcl 11347	. . . . . . . . . . . . . . . 16 $/\$
326	325	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $/\$
327	249, 324, 326	seqcl 12271	. . . . . . . . . . . . . 14
328	327	rpcnne0d 11373	. . . . . . . . . . . . 13 $/\$
329	296	a1i 11	. . . . . . . . . . . . . . . . 17
330	155, 161	ge0p1rpd 11391	. . . . . . . . . . . . . . . . 17
331	329, 330	rpmulcld 11380	. . . . . . . . . . . . . . . 16
332	154, 155, 159, 161	mulge0d 10211	. . . . . . . . . . . . . . . . 17
333	183, 332	ge0p1rpd 11391	. . . . . . . . . . . . . . . 16
334	331, 333	rpdivcld 11381	. . . . . . . . . . . . . . 15
335	329, 264	rpmulcld 11380	. . . . . . . . . . . . . . . . 17
336	335, 221	rpaddcld 11379	. . . . . . . . . . . . . . . 16
337	331, 336	rpdivcld 11381	. . . . . . . . . . . . . . 15
338	334, 337	rpmulcld 11380	. . . . . . . . . . . . . 14
339	338	rpcnne0d 11373	. . . . . . . . . . . . 13 $/\$
340		divdiv1 10340	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
341	129, 328, 339, 340	syl3anc 1292	. . . . . . . . . . . 12
342	341	eqcomd 2477	. . . . . . . . . . 11
343	342	oveq2d 6324	. . . . . . . . . 10
344	65	a1i 11	. . . . . . . . . . 11
345	327	rpcnd 11366	. . . . . . . . . . . 12
346	327	rpne0d 11369	. . . . . . . . . . . 12
347	345, 346	reccld 10398	. . . . . . . . . . 11
348	338	rpcnd 11366	. . . . . . . . . . 11
349	338	rpne0d 11369	. . . . . . . . . . 11
350	344, 347, 348, 349	divassd 10440	. . . . . . . . . 10
351	139, 268	eqnetrrd 2711	. . . . . . . . . . . . 13
352	201, 199, 201, 213, 351, 224	divmuldivd 10446	. . . . . . . . . . . 12
353	352	oveq2d 6324	. . . . . . . . . . 11
354	344, 347	mulcld 9681	. . . . . . . . . . . . 13
355	201, 201	mulcld 9681	. . . . . . . . . . . . 13
356	199, 213	mulcld 9681	. . . . . . . . . . . . 13
357	201, 201, 205, 205	mulne0d 10286	. . . . . . . . . . . . 13
358	199, 213, 351, 224	mulne0d 10286	. . . . . . . . . . . . 13
359	354, 355, 356, 357, 358	divdiv2d 10437	. . . . . . . . . . . 12
360	354, 356, 355, 357	divassd 10440	. . . . . . . . . . . 12
361	359, 360	eqtrd 2505	. . . . . . . . . . 11
362	199, 201, 201, 213, 205, 224, 205	divdivdivd 10452	. . . . . . . . . . . . 13
363	362	eqcomd 2477	. . . . . . . . . . . 12
364	363	oveq2d 6324	. . . . . . . . . . 11
365	353, 361, 364	3eqtrd 2509	. . . . . . . . . 10
366	343, 350, 365	3eqtr2d 2511	. . . . . . . . 9
367	61	a1i 11	. . . . . . . . . . . 12
368	367	halfcld 10880	. . . . . . . . . . 11
369	368, 347	mulcld 9681	. . . . . . . . . 10
370	206, 225, 226	divcld 10405	. . . . . . . . . 10
371	369, 370	mulcomd 9682	. . . . . . . . 9
372	284, 366, 371	3eqtrd 2509	. . . . . . . 8
373	278, 372	eqtrd 2505	. . . . . . 7
374	373	adantr 472	. . . . . 6 $/\$
375	126, 247, 374	3eqtr4d 2515	. . . . 5 $/\$
376	375	ex 441	. . . 4
377	9, 18, 27, 36, 124, 376	nnind 10649	. . 3
378	377	mpteq2ia 4478	. 2
379		wallispilem4.3	. 2
380		wallispilem4.4	. 2
381	378, 379, 380	3eqtr4i 2503	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 376

wceq 1452

wcel 1904

wne 2641 class class class wbr 4395

cmpt 4454

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cdiv 10291

cn 10631

c2 10681

c3 10682

cn0 10893

cz 10961

cuz 11182

crp 11325

cioo 11660

cfz 11810

cseq 12251

cexp 12310

csin 14193

cpi 14196

citg 22655

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cc 8883 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-disj 4367 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-ofr 6551 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-omul 7205 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-acn 8394 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-pi 14203 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-cmp 20479 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-ovol 22494 df-vol 22496 df-mbf 22656 df-itg1 22657 df-itg2 22658 df-ibl 22659 df-itg 22660 df-0p 22707 df-limc 22900 df-dv 22901

This theorem is referenced by: wallispilem5 38043

W3C validator