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 31368

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 6290	. . . . . . 7
2	1	fveq2d 5868	. . . . . 6
3	1	oveq1d 6297	. . . . . . 7
4	3	fveq2d 5868	. . . . . 6
5	2, 4	oveq12d 6300	. . . . 5
6		fveq2 5864	. . . . . . 7
7	6	oveq2d 6298	. . . . . 6
8	7	oveq2d 6298	. . . . 5
9	5, 8	eqeq12d 2489	. . . 4
10		oveq2 6290	. . . . . . 7
11	10	fveq2d 5868	. . . . . 6
12	10	oveq1d 6297	. . . . . . 7
13	12	fveq2d 5868	. . . . . 6
14	11, 13	oveq12d 6300	. . . . 5
15		fveq2 5864	. . . . . . 7
16	15	oveq2d 6298	. . . . . 6
17	16	oveq2d 6298	. . . . 5
18	14, 17	eqeq12d 2489	. . . 4
19		oveq2 6290	. . . . . . 7
20	19	fveq2d 5868	. . . . . 6
21	19	oveq1d 6297	. . . . . . 7
22	21	fveq2d 5868	. . . . . 6
23	20, 22	oveq12d 6300	. . . . 5
24		fveq2 5864	. . . . . . 7
25	24	oveq2d 6298	. . . . . 6
26	25	oveq2d 6298	. . . . 5
27	23, 26	eqeq12d 2489	. . . 4
28		oveq2 6290	. . . . . . 7
29	28	fveq2d 5868	. . . . . 6
30	28	oveq1d 6297	. . . . . . 7
31	30	fveq2d 5868	. . . . . 6
32	29, 31	oveq12d 6300	. . . . 5
33		fveq2 5864	. . . . . . 7
34	33	oveq2d 6298	. . . . . 6
35	34	oveq2d 6298	. . . . 5
36	32, 35	eqeq12d 2489	. . . 4
37		2cn 10602	. . . . . . . 8
38	37	mulid1i 9594	. . . . . . 7
39	38	fveq2i 5867	. . . . . 6
40	38	oveq1i 6292	. . . . . . . 8
41		2p1e3 10655	. . . . . . . 8
42	40, 41	eqtri 2496	. . . . . . 7
43	42	fveq2i 5867	. . . . . 6
44	39, 43	oveq12i 6294	. . . . 5
45		2z 10892	. . . . . . . . 9
46		uzid 11092	. . . . . . . . 9
47	45, 46	ax-mp 5	. . . . . . . 8
48		wallispilem4.2	. . . . . . . . . 10
49	48	wallispilem2 31366	. . . . . . . . 9 $/\$ $/\$
50	49	simp3i 1007	. . . . . . . 8
51	47, 50	ax-mp 5	. . . . . . 7
52		2m1e1 10646	. . . . . . . . 9
53	52	oveq1i 6292	. . . . . . . 8
54	37	subidi 9886	. . . . . . . . . 10
55	54	fveq2i 5867	. . . . . . . . 9
56	49	simp1i 1005	. . . . . . . . 9
57	55, 56	eqtri 2496	. . . . . . . 8
58	53, 57	oveq12i 6294	. . . . . . 7
59		ax-1cn 9546	. . . . . . . . 9
60		2cnne0 10746	. . . . . . . . 9 $/\$
61		pire 22585	. . . . . . . . . 10
62	61	recni 9604	. . . . . . . . 9
63		div32 10223	. . . . . . . . 9 $/\$ $/\$ $/\$
64	59, 60, 62, 63	mp3an 1324	. . . . . . . 8
65		2ne0 10624	. . . . . . . . . 10
66	62, 37, 65	divcli 10282	. . . . . . . . 9
67	66	mulid2i 9595	. . . . . . . 8
68	64, 67	eqtri 2496	. . . . . . 7
69	51, 58, 68	3eqtri 2500	. . . . . 6
70		3z 10893	. . . . . . . . 9
71		2re 10601	. . . . . . . . . 10
72		3re 10605	. . . . . . . . . 10
73		2lt3 10699	. . . . . . . . . 10
74	71, 72, 73	ltleii 9703	. . . . . . . . 9
75		eluz2 11084	. . . . . . . . 9 $/\$ $/\$
76	45, 70, 74, 75	mpbir3an 1178	. . . . . . . 8
77	48	wallispilem2 31366	. . . . . . . . 9 $/\$ $/\$
78	77	simp3i 1007	. . . . . . . 8
79	76, 78	ax-mp 5	. . . . . . 7
80		3m1e2 10648	. . . . . . . . . 10
81	80	eqcomi 2480	. . . . . . . . 9
82	81	oveq1i 6292	. . . . . . . 8
83		3cn 10606	. . . . . . . . . . 11
84	83, 37, 59, 41	subaddrii 9904	. . . . . . . . . 10
85	84	fveq2i 5867	. . . . . . . . 9
86	49	simp2i 1006	. . . . . . . . 9
87	85, 86	eqtr2i 2497	. . . . . . . 8
88	82, 87	oveq12i 6294	. . . . . . 7
89		3ne0 10626	. . . . . . . . 9
90	37, 83, 89	divcli 10282	. . . . . . . 8
91	90, 37	mulcomi 9598	. . . . . . 7
92	79, 88, 91	3eqtr2i 2502	. . . . . 6
93	69, 92	oveq12i 6294	. . . . 5
94		1z 10890	. . . . . . . . 9
95		seq1 12084	. . . . . . . . 9
96	94, 95	ax-mp 5	. . . . . . . 8
97		1nn 10543	. . . . . . . . 9
98		oveq2 6290	. . . . . . . . . . . . . 14
99	98, 38	syl6eq 2524	. . . . . . . . . . . . 13
100	98	oveq1d 6297	. . . . . . . . . . . . . 14
101	38	oveq1i 6292	. . . . . . . . . . . . . . 15
102	101, 52	eqtri 2496	. . . . . . . . . . . . . 14
103	100, 102	syl6eq 2524	. . . . . . . . . . . . 13
104	99, 103	oveq12d 6300	. . . . . . . . . . . 12
105	37	div1i 10268	. . . . . . . . . . . 12
106	104, 105	syl6eq 2524	. . . . . . . . . . 11
107	99	oveq1d 6297	. . . . . . . . . . . . 13
108	107, 41	syl6eq 2524	. . . . . . . . . . . 12
109	99, 108	oveq12d 6300	. . . . . . . . . . 11
110	106, 109	oveq12d 6300	. . . . . . . . . 10
111		wallispilem4.1	. . . . . . . . . 10
112		ovex 6307	. . . . . . . . . 10
113	110, 111, 112	fvmpt 5948	. . . . . . . . 9
114	97, 113	ax-mp 5	. . . . . . . 8
115	96, 114	eqtr2i 2497	. . . . . . 7
116	115	oveq2i 6293	. . . . . 6
117	37, 90	mulcli 9597	. . . . . . . . 9
118	114, 117	eqeltri 2551	. . . . . . . 8
119	96, 118	eqeltri 2551	. . . . . . 7
120	37, 83, 65, 89	divne0i 10288	. . . . . . . . 9
121	37, 90, 65, 120	mulne0i 10188	. . . . . . . 8
122	115, 121	eqnetrri 2764	. . . . . . 7
123	66, 119, 122	divreci 10285	. . . . . 6
124	116, 123	eqtri 2496	. . . . 5
125	44, 93, 124	3eqtri 2500	. . . 4
126		oveq2 6290	. . . . . . 7
127	126	adantl 466	. . . . . 6 $/\$
128		2cnd 10604	. . . . . . . . . . . . . . . 16
129		nncn 10540	. . . . . . . . . . . . . . . 16
130	59	a1i 11	. . . . . . . . . . . . . . . 16
131	128, 129, 130	adddid 9616	. . . . . . . . . . . . . . 15
132	128	mulid1d 9609	. . . . . . . . . . . . . . . 16
133	132	oveq2d 6298	. . . . . . . . . . . . . . 15
134	131, 133	eqtrd 2508	. . . . . . . . . . . . . 14
135	134	oveq1d 6297	. . . . . . . . . . . . 13
136	128, 129	mulcld 9612	. . . . . . . . . . . . . 14
137	136, 128, 130	addsubassd 9946	. . . . . . . . . . . . 13
138	52	a1i 11	. . . . . . . . . . . . . 14
139	138	oveq2d 6298	. . . . . . . . . . . . 13
140	135, 137, 139	3eqtrd 2512	. . . . . . . . . . . 12
141	140	oveq1d 6297	. . . . . . . . . . 11
142	141	oveq1d 6297	. . . . . . . . . 10
143	80	a1i 11	. . . . . . . . . . . . . 14
144	143	oveq2d 6298	. . . . . . . . . . . . 13
145	83	a1i 11	. . . . . . . . . . . . . 14
146	136, 145, 130	addsubassd 9946	. . . . . . . . . . . . 13
147	144, 146, 134	3eqtr4d 2518	. . . . . . . . . . . 12
148	147	oveq1d 6297	. . . . . . . . . . 11
149	148	oveq1d 6297	. . . . . . . . . 10
150	142, 149	oveq12d 6300	. . . . . . . . 9
151	45	a1i 11	. . . . . . . . . . . . . 14
152		nnz 10882	. . . . . . . . . . . . . . 15
153	152	peano2zd 10965	. . . . . . . . . . . . . 14
154	151, 153	zmulcld 10968	. . . . . . . . . . . . 13
155	71	a1i 11	. . . . . . . . . . . . . 14
156		nnre 10539	. . . . . . . . . . . . . . 15
157		1re 9591	. . . . . . . . . . . . . . . 16
158	157	a1i 11	. . . . . . . . . . . . . . 15
159	156, 158	readdcld 9619	. . . . . . . . . . . . . 14
160		0le2 10622	. . . . . . . . . . . . . . 15
161	160	a1i 11	. . . . . . . . . . . . . 14
162		nnnn0 10798	. . . . . . . . . . . . . . . 16
163	162	nn0ge0d 10851	. . . . . . . . . . . . . . 15
164	158, 156	addge02d 10137	. . . . . . . . . . . . . . 15
165	163, 164	mpbid 210	. . . . . . . . . . . . . 14
166	155, 159, 161, 165	lemulge11d 10479	. . . . . . . . . . . . 13
167	45	eluz1i 11085	. . . . . . . . . . . . 13 $/\$
168	154, 166, 167	sylanbrc 664	. . . . . . . . . . . 12
169	48, 168	itgsinexp 31272	. . . . . . . . . . 11
170	134	oveq1d 6297	. . . . . . . . . . . . . 14
171	136, 128	pncand 9927	. . . . . . . . . . . . . 14
172	170, 171	eqtrd 2508	. . . . . . . . . . . . 13
173	172	fveq2d 5868	. . . . . . . . . . . 12
174	173	oveq2d 6298	. . . . . . . . . . 11
175	169, 174	eqtrd 2508	. . . . . . . . . 10
176	134	oveq1d 6297	. . . . . . . . . . . . 13
177	136, 128, 130	addassd 9614	. . . . . . . . . . . . 13
178	41	a1i 11	. . . . . . . . . . . . . 14
179	178	oveq2d 6298	. . . . . . . . . . . . 13
180	176, 177, 179	3eqtrd 2512	. . . . . . . . . . . 12
181	180	fveq2d 5868	. . . . . . . . . . 11
182	151, 152	zmulcld 10968	. . . . . . . . . . . . . 14
183	70	a1i 11	. . . . . . . . . . . . . 14
184	182, 183	zaddcld 10966	. . . . . . . . . . . . 13
185	155, 156	remulcld 9620	. . . . . . . . . . . . . 14
186	72	a1i 11	. . . . . . . . . . . . . . 15
187	185, 186	readdcld 9619	. . . . . . . . . . . . . 14
188		nnge1 10558	. . . . . . . . . . . . . . 15
189	155, 156, 161, 188	lemulge11d 10479	. . . . . . . . . . . . . 14
190		0re 9592	. . . . . . . . . . . . . . . 16
191		3pos 10625	. . . . . . . . . . . . . . . 16
192	190, 72, 191	ltleii 9703	. . . . . . . . . . . . . . 15
193	185, 186	addge01d 10136	. . . . . . . . . . . . . . 15
194	192, 193	mpbii 211	. . . . . . . . . . . . . 14
195	155, 185, 187, 189, 194	letrd 9734	. . . . . . . . . . . . 13
196	45	eluz1i 11085	. . . . . . . . . . . . 13 $/\$
197	184, 195, 196	sylanbrc 664	. . . . . . . . . . . 12
198	48, 197	itgsinexp 31272	. . . . . . . . . . 11
199	181, 198	eqtrd 2508	. . . . . . . . . 10
200	175, 199	oveq12d 6300	. . . . . . . . 9
201	136, 130	addcld 9611	. . . . . . . . . . 11
202	129, 130	addcld 9611	. . . . . . . . . . . 12
203	128, 202	mulcld 9612	. . . . . . . . . . 11
204	65	a1i 11	. . . . . . . . . . . 12
205		peano2nn 10544	. . . . . . . . . . . . 13
206	205	nnne0d 10576	. . . . . . . . . . . 12
207	128, 202, 204, 206	mulne0d 10197	. . . . . . . . . . 11
208	201, 203, 207	divcld 10316	. . . . . . . . . 10
209		2nn0 10808	. . . . . . . . . . . . 13
210	209	a1i 11	. . . . . . . . . . . 12
211	210, 162	nn0mulcld 10853	. . . . . . . . . . 11
212	48	wallispilem3 31367	. . . . . . . . . . . 12
213	212	rpcnd 11254	. . . . . . . . . . 11
214	211, 213	syl 16	. . . . . . . . . 10
215	136, 145	addcld 9611	. . . . . . . . . . . 12
216	190	a1i 11	. . . . . . . . . . . . . 14
217		2pos 10623	. . . . . . . . . . . . . . . 16
218	217	a1i 11	. . . . . . . . . . . . . . 15
219		nngt0 10561	. . . . . . . . . . . . . . 15
220	155, 156, 218, 219	mulgt0d 9732	. . . . . . . . . . . . . 14
221	186, 191	jctir 538	. . . . . . . . . . . . . . . 16 $/\$
222		elrp 11218	. . . . . . . . . . . . . . . 16 $/\$
223	221, 222	sylibr 212	. . . . . . . . . . . . . . 15
224	185, 223	ltaddrpd 11281	. . . . . . . . . . . . . 14
225	216, 185, 187, 220, 224	lttrd 9738	. . . . . . . . . . . . 13
226	225	gt0ne0d 10113	. . . . . . . . . . . 12
227	203, 215, 226	divcld 10316	. . . . . . . . . . 11
228	203, 215, 207, 226	divne0d 10332	. . . . . . . . . . 11
229	184, 151	zsubcld 10967	. . . . . . . . . . . . . 14
230	187, 155	subge0d 10138	. . . . . . . . . . . . . . 15
231	195, 230	mpbird 232	. . . . . . . . . . . . . 14
232		elnn0z 10873	. . . . . . . . . . . . . 14 $/\$
233	229, 231, 232	sylanbrc 664	. . . . . . . . . . . . 13
234	48	wallispilem3 31367	. . . . . . . . . . . . 13
235	233, 234	syl 16	. . . . . . . . . . . 12
236	235	rpcnne0d 11261	. . . . . . . . . . 11 $/\$
237	227, 228, 236	jca31 534	. . . . . . . . . 10 $/\$ $/\$ $/\$
238		divmuldiv 10240	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
239	208, 214, 237, 238	syl21anc 1227	. . . . . . . . 9
240	150, 200, 239	3eqtr4d 2518	. . . . . . . 8
241	136, 145, 128	addsubassd 9946	. . . . . . . . . . . 12
242	84	a1i 11	. . . . . . . . . . . . 13
243	242	oveq2d 6298	. . . . . . . . . . . 12
244	241, 243	eqtrd 2508	. . . . . . . . . . 11
245	244	fveq2d 5868	. . . . . . . . . 10
246	245	oveq2d 6298	. . . . . . . . 9
247	246	oveq2d 6298	. . . . . . . 8
248	240, 247	eqtrd 2508	. . . . . . 7
249	248	adantr 465	. . . . . 6 $/\$
250		elnnuz 11114	. . . . . . . . . . . . 13
251	250	biimpi 194	. . . . . . . . . . . 12
252		seqp1 12086	. . . . . . . . . . . 12
253	251, 252	syl 16	. . . . . . . . . . 11
254	111	a1i 11	. . . . . . . . . . . . 13
255		oveq2 6290	. . . . . . . . . . . . . . . 16
256	255	oveq1d 6297	. . . . . . . . . . . . . . . 16
257	255, 256	oveq12d 6300	. . . . . . . . . . . . . . 15
258	255	oveq1d 6297	. . . . . . . . . . . . . . . 16
259	255, 258	oveq12d 6300	. . . . . . . . . . . . . . 15
260	257, 259	oveq12d 6300	. . . . . . . . . . . . . 14
261	260	adantl 466	. . . . . . . . . . . . 13 $/\$
262	155, 159	remulcld 9620	. . . . . . . . . . . . . . 15
263	262, 158	resubcld 9983	. . . . . . . . . . . . . . 15
264		1lt2 10698	. . . . . . . . . . . . . . . . . . 19
265	264	a1i 11	. . . . . . . . . . . . . . . . . 18
266		nnrp 11225	. . . . . . . . . . . . . . . . . . 19
267	158, 266	ltaddrp2d 11282	. . . . . . . . . . . . . . . . . 18
268	155, 159, 265, 267	mulgt1d 10478	. . . . . . . . . . . . . . . . 17
269	158, 268	gtned 9715	. . . . . . . . . . . . . . . 16
270	203, 130, 269	subne0d 9935	. . . . . . . . . . . . . . 15
271	262, 263, 270	redivcld 10368	. . . . . . . . . . . . . 14
272	180, 187	eqeltrd 2555	. . . . . . . . . . . . . . 15
273	180, 226	eqnetrd 2760	. . . . . . . . . . . . . . 15
274	262, 272, 273	redivcld 10368	. . . . . . . . . . . . . 14
275	271, 274	remulcld 9620	. . . . . . . . . . . . 13
276	254, 261, 205, 275	fvmptd 5953	. . . . . . . . . . . 12
277	276	oveq2d 6298	. . . . . . . . . . 11
278	253, 277	eqtrd 2508	. . . . . . . . . 10
279	278	oveq2d 6298	. . . . . . . . 9
280	279	oveq2d 6298	. . . . . . . 8
281	140	oveq2d 6298	. . . . . . . . . . . . 13
282	180	oveq2d 6298	. . . . . . . . . . . . 13
283	281, 282	oveq12d 6300	. . . . . . . . . . . 12
284	283	oveq2d 6298	. . . . . . . . . . 11
285	284	oveq2d 6298	. . . . . . . . . 10
286	285	oveq2d 6298	. . . . . . . . 9
287		elfznn 11710	. . . . . . . . . . . . . . . . 17
288	287	adantl 466	. . . . . . . . . . . . . . . 16 $/\$
289	111	a1i 11	. . . . . . . . . . . . . . . . . 18
290		oveq2 6290	. . . . . . . . . . . . . . . . . . . . 21
291	290	oveq1d 6297	. . . . . . . . . . . . . . . . . . . . 21
292	290, 291	oveq12d 6300	. . . . . . . . . . . . . . . . . . . 20
293	290	oveq1d 6297	. . . . . . . . . . . . . . . . . . . . 21
294	290, 293	oveq12d 6300	. . . . . . . . . . . . . . . . . . . 20
295	292, 294	oveq12d 6300	. . . . . . . . . . . . . . . . . . 19
296	295	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
297		id 22	. . . . . . . . . . . . . . . . . 18
298		2rp 11221	. . . . . . . . . . . . . . . . . . . . . 22
299	298	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
300		nnrp 11225	. . . . . . . . . . . . . . . . . . . . 21
301	299, 300	rpmulcld 11268	. . . . . . . . . . . . . . . . . . . 20
302	71	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
303		nnre 10539	. . . . . . . . . . . . . . . . . . . . . . 23
304	302, 303	remulcld 9620	. . . . . . . . . . . . . . . . . . . . . 22
305	157	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
306	304, 305	resubcld 9983	. . . . . . . . . . . . . . . . . . . . 21
307		nnge1 10558	. . . . . . . . . . . . . . . . . . . . . . 23
308		nncn 10540	. . . . . . . . . . . . . . . . . . . . . . . . 25
309	308	mulid2d 9610	. . . . . . . . . . . . . . . . . . . . . . . 24
310	305, 302, 300	ltmul1d 11289	. . . . . . . . . . . . . . . . . . . . . . . . 25
311	264, 310	mpbii 211	. . . . . . . . . . . . . . . . . . . . . . . 24
312	309, 311	eqbrtrrd 4469	. . . . . . . . . . . . . . . . . . . . . . 23
313	305, 303, 304, 307, 312	lelttrd 9735	. . . . . . . . . . . . . . . . . . . . . 22
314	305, 304	posdifd 10135	. . . . . . . . . . . . . . . . . . . . . 22
315	313, 314	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21
316	306, 315	elrpd 11250	. . . . . . . . . . . . . . . . . . . 20
317	301, 316	rpdivcld 11269	. . . . . . . . . . . . . . . . . . 19
318	160	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
319	300	rpge0d 11256	. . . . . . . . . . . . . . . . . . . . . 22
320	302, 303, 318, 319	mulge0d 10125	. . . . . . . . . . . . . . . . . . . . 21
321	304, 320	ge0p1rpd 11278	. . . . . . . . . . . . . . . . . . . 20
322	301, 321	rpdivcld 11269	. . . . . . . . . . . . . . . . . . 19
323	317, 322	rpmulcld 11268	. . . . . . . . . . . . . . . . . 18
324	289, 296, 297, 323	fvmptd 5953	. . . . . . . . . . . . . . . . 17
325	324, 323	eqeltrd 2555	. . . . . . . . . . . . . . . 16
326	288, 325	syl 16	. . . . . . . . . . . . . . 15 $/\$
327		rpmulcl 11237	. . . . . . . . . . . . . . . 16 $/\$
328	327	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
329	251, 326, 328	seqcl 12091	. . . . . . . . . . . . . 14
330	329	rpcnne0d 11261	. . . . . . . . . . . . 13 $/\$
331	298	a1i 11	. . . . . . . . . . . . . . . . 17
332	156, 163	ge0p1rpd 11278	. . . . . . . . . . . . . . . . 17
333	331, 332	rpmulcld 11268	. . . . . . . . . . . . . . . 16
334	155, 156, 161, 163	mulge0d 10125	. . . . . . . . . . . . . . . . 17
335	185, 334	ge0p1rpd 11278	. . . . . . . . . . . . . . . 16
336	333, 335	rpdivcld 11269	. . . . . . . . . . . . . . 15
337	331, 266	rpmulcld 11268	. . . . . . . . . . . . . . . . 17
338	337, 223	rpaddcld 11267	. . . . . . . . . . . . . . . 16
339	333, 338	rpdivcld 11269	. . . . . . . . . . . . . . 15
340	336, 339	rpmulcld 11268	. . . . . . . . . . . . . 14
341	340	rpcnne0d 11261	. . . . . . . . . . . . 13 $/\$
342		divdiv1 10251	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
343	130, 330, 341, 342	syl3anc 1228	. . . . . . . . . . . 12
344	343	eqcomd 2475	. . . . . . . . . . 11
345	344	oveq2d 6298	. . . . . . . . . 10
346	66	a1i 11	. . . . . . . . . . 11
347	329	rpcnd 11254	. . . . . . . . . . . 12
348	329	rpne0d 11257	. . . . . . . . . . . 12
349	347, 348	reccld 10309	. . . . . . . . . . 11
350	340	rpcnd 11254	. . . . . . . . . . 11
351	340	rpne0d 11257	. . . . . . . . . . 11
352	346, 349, 350, 351	divassd 10351	. . . . . . . . . 10
353	140, 270	eqnetrrd 2761	. . . . . . . . . . . . 13
354	203, 201, 203, 215, 353, 226	divmuldivd 10357	. . . . . . . . . . . 12
355	354	oveq2d 6298	. . . . . . . . . . 11
356	346, 349	mulcld 9612	. . . . . . . . . . . . 13
357	203, 203	mulcld 9612	. . . . . . . . . . . . 13
358	201, 215	mulcld 9612	. . . . . . . . . . . . 13
359	203, 203, 207, 207	mulne0d 10197	. . . . . . . . . . . . 13
360	201, 215, 353, 226	mulne0d 10197	. . . . . . . . . . . . 13
361	356, 357, 358, 359, 360	divdiv2d 10348	. . . . . . . . . . . 12
362	356, 358, 357, 359	divassd 10351	. . . . . . . . . . . 12
363	361, 362	eqtrd 2508	. . . . . . . . . . 11
364	201, 203, 203, 215, 207, 226, 207	divdivdivd 10363	. . . . . . . . . . . . 13
365	364	eqcomd 2475	. . . . . . . . . . . 12
366	365	oveq2d 6298	. . . . . . . . . . 11
367	355, 363, 366	3eqtrd 2512	. . . . . . . . . 10
368	345, 352, 367	3eqtr2d 2514	. . . . . . . . 9
369	62	a1i 11	. . . . . . . . . . . 12
370	369	halfcld 10779	. . . . . . . . . . 11
371	370, 349	mulcld 9612	. . . . . . . . . 10
372	208, 227, 228	divcld 10316	. . . . . . . . . 10
373	371, 372	mulcomd 9613	. . . . . . . . 9
374	286, 368, 373	3eqtrd 2512	. . . . . . . 8
375	280, 374	eqtrd 2508	. . . . . . 7
376	375	adantr 465	. . . . . 6 $/\$
377	127, 249, 376	3eqtr4d 2518	. . . . 5 $/\$
378	377	ex 434	. . . 4
379	9, 18, 27, 36, 125, 378	nnind 10550	. . 3
380	379	mpteq2ia 4529	. 2
381		wallispilem4.3	. 2
382		wallispilem4.4	. 2
383	380, 381, 382	3eqtr4i 2506	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1379

wcel 1767

wne 2662 class class class wbr 4447

cmpt 4505

cfv 5586 (class class class)co 6282

cc 9486

cr 9487

cc0 9488

c1 9489

caddc 9491

cmul 9493

clt 9624

cle 9625

cmin 9801

cdiv 10202

cn 10532

c2 10581

c3 10582

cn0 10791

cz 10860

cuz 11078

crp 11216

cioo 11525

cfz 11668

cseq 12071

cexp 12130

csin 13657

cpi 13660

citg 21762

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cc 8811 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-ofr 6523 df-om 6679 df-1st 6781 df-2nd 6782 df-supp 6899 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-omul 7132 df-er 7308 df-map 7419 df-pm 7420 df-ixp 7467 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fsupp 7826 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-acn 8319 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10973 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ioc 11530 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-mod 11961 df-seq 12072 df-exp 12131 df-fac 12318 df-bc 12345 df-hash 12370 df-shft 12859 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-limsup 13253 df-clim 13270 df-rlim 13271 df-sum 13468 df-ef 13661 df-sin 13663 df-cos 13664 df-pi 13666 df-struct 14488 df-ndx 14489 df-slot 14490 df-base 14491 df-sets 14492 df-ress 14493 df-plusg 14564 df-mulr 14565 df-starv 14566 df-sca 14567 df-vsca 14568 df-ip 14569 df-tset 14570 df-ple 14571 df-ds 14573 df-unif 14574 df-hom 14575 df-cco 14576 df-rest 14674 df-topn 14675 df-0g 14693 df-gsum 14694 df-topgen 14695 df-pt 14696 df-prds 14699 df-xrs 14753 df-qtop 14758 df-imas 14759 df-xps 14761 df-mre 14837 df-mrc 14838 df-acs 14840 df-mnd 15728 df-submnd 15778 df-mulg 15861 df-cntz 16150 df-cmn 16596 df-psmet 18182 df-xmet 18183 df-met 18184 df-bl 18185 df-mopn 18186 df-fbas 18187 df-fg 18188 df-cnfld 18192 df-top 19166 df-bases 19168 df-topon 19169 df-topsp 19170 df-cld 19286 df-ntr 19287 df-cls 19288 df-nei 19365 df-lp 19403 df-perf 19404 df-cn 19494 df-cnp 19495 df-haus 19582 df-cmp 19653 df-tx 19798 df-hmeo 19991 df-fil 20082 df-fm 20174 df-flim 20175 df-flf 20176 df-xms 20558 df-ms 20559 df-tms 20560 df-cncf 21117 df-ovol 21611 df-vol 21612 df-mbf 21763 df-itg1 21764 df-itg2 21765 df-ibl 21766 df-itg 21767 df-0p 21812 df-limc 22005 df-dv 22006

This theorem is referenced by: wallispilem5 31369

W3C validator