wallispilem4 - Mathbox for Glauco Siliprandi

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

Theorem wallispilem4 27684

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 6048	. . . . . . 7
2	1	fveq2d 5691	. . . . . 6
3	1	oveq1d 6055	. . . . . . 7
4	3	fveq2d 5691	. . . . . 6
5	2, 4	oveq12d 6058	. . . . 5
6		fveq2 5687	. . . . . . 7
7	6	oveq2d 6056	. . . . . 6
8	7	oveq2d 6056	. . . . 5
9	5, 8	eqeq12d 2418	. . . 4
10		oveq2 6048	. . . . . . 7
11	10	fveq2d 5691	. . . . . 6
12	10	oveq1d 6055	. . . . . . 7
13	12	fveq2d 5691	. . . . . 6
14	11, 13	oveq12d 6058	. . . . 5
15		fveq2 5687	. . . . . . 7
16	15	oveq2d 6056	. . . . . 6
17	16	oveq2d 6056	. . . . 5
18	14, 17	eqeq12d 2418	. . . 4
19		oveq2 6048	. . . . . . 7
20	19	fveq2d 5691	. . . . . 6
21	19	oveq1d 6055	. . . . . . 7
22	21	fveq2d 5691	. . . . . 6
23	20, 22	oveq12d 6058	. . . . 5
24		fveq2 5687	. . . . . . 7
25	24	oveq2d 6056	. . . . . 6
26	25	oveq2d 6056	. . . . 5
27	23, 26	eqeq12d 2418	. . . 4
28		oveq2 6048	. . . . . . 7
29	28	fveq2d 5691	. . . . . 6
30	28	oveq1d 6055	. . . . . . 7
31	30	fveq2d 5691	. . . . . 6
32	29, 31	oveq12d 6058	. . . . 5
33		fveq2 5687	. . . . . . 7
34	33	oveq2d 6056	. . . . . 6
35	34	oveq2d 6056	. . . . 5
36	32, 35	eqeq12d 2418	. . . 4
37		2cn 10026	. . . . . . . 8
38	37	mulid1i 9048	. . . . . . 7
39	38	fveq2i 5690	. . . . . 6
40	38	oveq1i 6050	. . . . . . . 8
41		2p1e3 10059	. . . . . . . 8
42	40, 41	eqtri 2424	. . . . . . 7
43	42	fveq2i 5690	. . . . . 6
44	39, 43	oveq12i 6052	. . . . 5
45		2z 10268	. . . . . . . . 9
46		uzid 10456	. . . . . . . . 9
47	45, 46	ax-mp 8	. . . . . . . 8
48		wallispilem4.2	. . . . . . . . . 10
49	48	wallispilem2 27682	. . . . . . . . 9 $/\$ $/\$
50	49	simp3i 968	. . . . . . . 8
51	47, 50	ax-mp 8	. . . . . . 7
52		2m1e1 10051	. . . . . . . . 9
53	52	oveq1i 6050	. . . . . . . 8
54	37	subidi 9327	. . . . . . . . . 10
55	54	fveq2i 5690	. . . . . . . . 9
56	49	simp1i 966	. . . . . . . . 9
57	55, 56	eqtri 2424	. . . . . . . 8
58	53, 57	oveq12i 6052	. . . . . . 7
59		ax-1cn 9004	. . . . . . . . 9
60		2ne0 10039	. . . . . . . . . 10
61	37, 60	pm3.2i 442	. . . . . . . . 9 $/\$
62		pire 20325	. . . . . . . . . 10
63	62	recni 9058	. . . . . . . . 9
64		div32 9654	. . . . . . . . 9 $/\$ $/\$ $/\$
65	59, 61, 63, 64	mp3an 1279	. . . . . . . 8
66	63, 37, 60	divcli 9712	. . . . . . . . 9
67	66	mulid2i 9049	. . . . . . . 8
68	65, 67	eqtri 2424	. . . . . . 7
69	51, 58, 68	3eqtri 2428	. . . . . 6
70		3nn 10090	. . . . . . . . . 10
71	70	nnzi 10261	. . . . . . . . 9
72		2re 10025	. . . . . . . . . 10
73		3re 10027	. . . . . . . . . 10
74		2lt3 10099	. . . . . . . . . 10
75	72, 73, 74	ltleii 9152	. . . . . . . . 9
76		eluz2 10450	. . . . . . . . 9 $/\$ $/\$
77	45, 71, 75, 76	mpbir3an 1136	. . . . . . . 8
78	48	wallispilem2 27682	. . . . . . . . 9 $/\$ $/\$
79	78	simp3i 968	. . . . . . . 8
80	77, 79	ax-mp 8	. . . . . . 7
81		3m1e2 10052	. . . . . . . . . 10
82	81	eqcomi 2408	. . . . . . . . 9
83	82	oveq1i 6050	. . . . . . . 8
84		3cn 10028	. . . . . . . . . . 11
85	84, 37, 59, 41	subaddrii 9345	. . . . . . . . . 10
86	85	fveq2i 5690	. . . . . . . . 9
87	49	simp2i 967	. . . . . . . . 9
88	86, 87	eqtr2i 2425	. . . . . . . 8
89	83, 88	oveq12i 6052	. . . . . . 7
90		3ne0 10041	. . . . . . . . 9
91	37, 84, 90	divcli 9712	. . . . . . . 8
92	91, 37	mulcomi 9052	. . . . . . 7
93	80, 89, 92	3eqtr2i 2430	. . . . . 6
94	69, 93	oveq12i 6052	. . . . 5
95		1z 10267	. . . . . . . . 9
96		seq1 11291	. . . . . . . . 9
97	95, 96	ax-mp 8	. . . . . . . 8
98		1nn 9967	. . . . . . . . 9
99		oveq2 6048	. . . . . . . . . . . . . 14
100	99, 38	syl6eq 2452	. . . . . . . . . . . . 13
101	99	oveq1d 6055	. . . . . . . . . . . . . 14
102	38	oveq1i 6050	. . . . . . . . . . . . . . 15
103	102, 52	eqtri 2424	. . . . . . . . . . . . . 14
104	101, 103	syl6eq 2452	. . . . . . . . . . . . 13
105	100, 104	oveq12d 6058	. . . . . . . . . . . 12
106	37	div1i 9698	. . . . . . . . . . . 12
107	105, 106	syl6eq 2452	. . . . . . . . . . 11
108	100	oveq1d 6055	. . . . . . . . . . . . 13
109	108, 41	syl6eq 2452	. . . . . . . . . . . 12
110	100, 109	oveq12d 6058	. . . . . . . . . . 11
111	107, 110	oveq12d 6058	. . . . . . . . . 10
112		wallispilem4.1	. . . . . . . . . 10
113		ovex 6065	. . . . . . . . . 10
114	111, 112, 113	fvmpt 5765	. . . . . . . . 9
115	98, 114	ax-mp 8	. . . . . . . 8
116	97, 115	eqtr2i 2425	. . . . . . 7
117	116	oveq2i 6051	. . . . . 6
118	37, 91	mulcli 9051	. . . . . . . . 9
119	115, 118	eqeltri 2474	. . . . . . . 8
120	97, 119	eqeltri 2474	. . . . . . 7
121	37, 84, 60, 90	divne0i 9718	. . . . . . . . 9
122	37, 91, 60, 121	mulne0i 9621	. . . . . . . 8
123	116, 122	eqnetrri 2586	. . . . . . 7
124	66, 120, 123	divreci 9715	. . . . . 6
125	117, 124	eqtri 2424	. . . . 5
126	44, 94, 125	3eqtri 2428	. . . 4
127		oveq2 6048	. . . . . . 7
128	127	adantl 453	. . . . . 6 $/\$
129	37	a1i 11	. . . . . . . . . . . . . . . 16
130		nncn 9964	. . . . . . . . . . . . . . . 16
131	59	a1i 11	. . . . . . . . . . . . . . . 16
132	129, 130, 131	adddid 9068	. . . . . . . . . . . . . . 15
133	129	mulid1d 9061	. . . . . . . . . . . . . . . 16
134	133	oveq2d 6056	. . . . . . . . . . . . . . 15
135	132, 134	eqtrd 2436	. . . . . . . . . . . . . 14
136	135	oveq1d 6055	. . . . . . . . . . . . 13
137	129, 130	mulcld 9064	. . . . . . . . . . . . . 14
138	137, 129, 131	addsubassd 9387	. . . . . . . . . . . . 13
139	52	a1i 11	. . . . . . . . . . . . . 14
140	139	oveq2d 6056	. . . . . . . . . . . . 13
141	136, 138, 140	3eqtrd 2440	. . . . . . . . . . . 12
142	141	oveq1d 6055	. . . . . . . . . . 11
143	142	oveq1d 6055	. . . . . . . . . 10
144	81	a1i 11	. . . . . . . . . . . . . 14
145	144	oveq2d 6056	. . . . . . . . . . . . 13
146	84	a1i 11	. . . . . . . . . . . . . 14
147	137, 146, 131	addsubassd 9387	. . . . . . . . . . . . 13
148	145, 147, 135	3eqtr4d 2446	. . . . . . . . . . . 12
149	148	oveq1d 6055	. . . . . . . . . . 11
150	149	oveq1d 6055	. . . . . . . . . 10
151	143, 150	oveq12d 6058	. . . . . . . . 9
152	45	a1i 11	. . . . . . . . . . . . . 14
153		nnz 10259	. . . . . . . . . . . . . . 15
154	153	peano2zd 10334	. . . . . . . . . . . . . 14
155	152, 154	zmulcld 10337	. . . . . . . . . . . . 13
156	72	a1i 11	. . . . . . . . . . . . . 14
157		nnre 9963	. . . . . . . . . . . . . . 15
158		1re 9046	. . . . . . . . . . . . . . . 16
159	158	a1i 11	. . . . . . . . . . . . . . 15
160	157, 159	readdcld 9071	. . . . . . . . . . . . . 14
161		0re 9047	. . . . . . . . . . . . . . . 16
162		2pos 10038	. . . . . . . . . . . . . . . 16
163	161, 72, 162	ltleii 9152	. . . . . . . . . . . . . . 15
164	163	a1i 11	. . . . . . . . . . . . . 14
165		nnnn0 10184	. . . . . . . . . . . . . . . 16
166	165	nn0ge0d 10233	. . . . . . . . . . . . . . 15
167	159, 157	addge02d 9571	. . . . . . . . . . . . . . 15
168	166, 167	mpbid 202	. . . . . . . . . . . . . 14
169	156, 160, 164, 168	lemulge11d 9904	. . . . . . . . . . . . 13
170	45	eluz1i 10451	. . . . . . . . . . . . 13 $/\$
171	155, 169, 170	sylanbrc 646	. . . . . . . . . . . 12
172	48, 171	itgsinexp 27616	. . . . . . . . . . 11
173	135	oveq1d 6055	. . . . . . . . . . . . . 14
174	137, 129	pncand 9368	. . . . . . . . . . . . . 14
175	173, 174	eqtrd 2436	. . . . . . . . . . . . 13
176	175	fveq2d 5691	. . . . . . . . . . . 12
177	176	oveq2d 6056	. . . . . . . . . . 11
178	172, 177	eqtrd 2436	. . . . . . . . . 10
179	135	oveq1d 6055	. . . . . . . . . . . . 13
180	137, 129, 131	addassd 9066	. . . . . . . . . . . . 13
181	41	a1i 11	. . . . . . . . . . . . . 14
182	181	oveq2d 6056	. . . . . . . . . . . . 13
183	179, 180, 182	3eqtrd 2440	. . . . . . . . . . . 12
184	183	fveq2d 5691	. . . . . . . . . . 11
185	152, 153	zmulcld 10337	. . . . . . . . . . . . . 14
186	71	a1i 11	. . . . . . . . . . . . . 14
187	185, 186	zaddcld 10335	. . . . . . . . . . . . 13
188	156, 157	remulcld 9072	. . . . . . . . . . . . . 14
189	73	a1i 11	. . . . . . . . . . . . . . 15
190	188, 189	readdcld 9071	. . . . . . . . . . . . . 14
191		nnge1 9982	. . . . . . . . . . . . . . 15
192	156, 157, 164, 191	lemulge11d 9904	. . . . . . . . . . . . . 14
193		3pos 10040	. . . . . . . . . . . . . . . 16
194	161, 73, 193	ltleii 9152	. . . . . . . . . . . . . . 15
195	188, 189	addge01d 9570	. . . . . . . . . . . . . . 15
196	194, 195	mpbii 203	. . . . . . . . . . . . . 14
197	156, 188, 190, 192, 196	letrd 9183	. . . . . . . . . . . . 13
198	45	eluz1i 10451	. . . . . . . . . . . . 13 $/\$
199	187, 197, 198	sylanbrc 646	. . . . . . . . . . . 12
200	48, 199	itgsinexp 27616	. . . . . . . . . . 11
201	184, 200	eqtrd 2436	. . . . . . . . . 10
202	178, 201	oveq12d 6058	. . . . . . . . 9
203	137, 131	addcld 9063	. . . . . . . . . . 11
204	130, 131	addcld 9063	. . . . . . . . . . . 12
205	129, 204	mulcld 9064	. . . . . . . . . . 11
206	60	a1i 11	. . . . . . . . . . . 12
207		peano2nn 9968	. . . . . . . . . . . . 13
208	207	nnne0d 10000	. . . . . . . . . . . 12
209	129, 204, 206, 208	mulne0d 9630	. . . . . . . . . . 11
210	203, 205, 209	divcld 9746	. . . . . . . . . 10
211		2nn0 10194	. . . . . . . . . . . . 13
212	211	a1i 11	. . . . . . . . . . . 12
213	212, 165	nn0mulcld 10235	. . . . . . . . . . 11
214	48	wallispilem3 27683	. . . . . . . . . . . 12
215	214	rpcnd 10606	. . . . . . . . . . 11
216	213, 215	syl 16	. . . . . . . . . 10
217	137, 146	addcld 9063	. . . . . . . . . . . 12
218	161	a1i 11	. . . . . . . . . . . . . 14
219	162	a1i 11	. . . . . . . . . . . . . . 15
220		nngt0 9985	. . . . . . . . . . . . . . 15
221	156, 157, 219, 220	mulgt0d 9181	. . . . . . . . . . . . . 14
222	189, 193	jctir 525	. . . . . . . . . . . . . . . 16 $/\$
223		elrp 10570	. . . . . . . . . . . . . . . 16 $/\$
224	222, 223	sylibr 204	. . . . . . . . . . . . . . 15
225	188, 224	ltaddrpd 10633	. . . . . . . . . . . . . 14
226	218, 188, 190, 221, 225	lttrd 9187	. . . . . . . . . . . . 13
227	226	gt0ne0d 9547	. . . . . . . . . . . 12
228	205, 217, 227	divcld 9746	. . . . . . . . . . 11
229	205, 217, 209, 227	divne0d 9762	. . . . . . . . . . 11
230	187, 152	zsubcld 10336	. . . . . . . . . . . . . 14
231	190, 156	subge0d 9572	. . . . . . . . . . . . . . 15
232	197, 231	mpbird 224	. . . . . . . . . . . . . 14
233		elnn0z 10250	. . . . . . . . . . . . . 14 $/\$
234	230, 232, 233	sylanbrc 646	. . . . . . . . . . . . 13
235	48	wallispilem3 27683	. . . . . . . . . . . . 13
236	234, 235	syl 16	. . . . . . . . . . . 12
237	236	rpcnne0d 10613	. . . . . . . . . . 11 $/\$
238	228, 229, 237	jca31 521	. . . . . . . . . 10 $/\$ $/\$ $/\$
239		divmuldiv 9670	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
240	210, 216, 238, 239	syl21anc 1183	. . . . . . . . 9
241	151, 202, 240	3eqtr4d 2446	. . . . . . . 8
242	137, 146, 129	addsubassd 9387	. . . . . . . . . . . 12
243	85	a1i 11	. . . . . . . . . . . . 13
244	243	oveq2d 6056	. . . . . . . . . . . 12
245	242, 244	eqtrd 2436	. . . . . . . . . . 11
246	245	fveq2d 5691	. . . . . . . . . 10
247	246	oveq2d 6056	. . . . . . . . 9
248	247	oveq2d 6056	. . . . . . . 8
249	241, 248	eqtrd 2436	. . . . . . 7
250	249	adantr 452	. . . . . 6 $/\$
251		elnnuz 10478	. . . . . . . . . . . . 13
252	251	biimpi 187	. . . . . . . . . . . 12
253		seqp1 11293	. . . . . . . . . . . 12
254	252, 253	syl 16	. . . . . . . . . . 11
255	112	a1i 11	. . . . . . . . . . . . 13
256		oveq2 6048	. . . . . . . . . . . . . . . 16
257	256	oveq1d 6055	. . . . . . . . . . . . . . . 16
258	256, 257	oveq12d 6058	. . . . . . . . . . . . . . 15
259	256	oveq1d 6055	. . . . . . . . . . . . . . . 16
260	256, 259	oveq12d 6058	. . . . . . . . . . . . . . 15
261	258, 260	oveq12d 6058	. . . . . . . . . . . . . 14
262	261	adantl 453	. . . . . . . . . . . . 13 $/\$
263	156, 160	remulcld 9072	. . . . . . . . . . . . . . 15
264	263, 159	resubcld 9421	. . . . . . . . . . . . . . 15
265		1lt2 10098	. . . . . . . . . . . . . . . . . . 19
266	265	a1i 11	. . . . . . . . . . . . . . . . . 18
267		nnrp 10577	. . . . . . . . . . . . . . . . . . 19
268	159, 267	ltaddrp2d 10634	. . . . . . . . . . . . . . . . . 18
269	156, 160, 266, 268	mulgt1d 9903	. . . . . . . . . . . . . . . . 17
270	159, 269	gtned 9164	. . . . . . . . . . . . . . . 16
271	205, 131, 270	subne0d 9376	. . . . . . . . . . . . . . 15
272	263, 264, 271	redivcld 9798	. . . . . . . . . . . . . 14
273	183, 190	eqeltrd 2478	. . . . . . . . . . . . . . 15
274	183, 227	eqnetrd 2585	. . . . . . . . . . . . . . 15
275	263, 273, 274	redivcld 9798	. . . . . . . . . . . . . 14
276	272, 275	remulcld 9072	. . . . . . . . . . . . 13
277	255, 262, 207, 276	fvmptd 5769	. . . . . . . . . . . 12
278	277	oveq2d 6056	. . . . . . . . . . 11
279	254, 278	eqtrd 2436	. . . . . . . . . 10
280	279	oveq2d 6056	. . . . . . . . 9
281	280	oveq2d 6056	. . . . . . . 8
282	141	oveq2d 6056	. . . . . . . . . . . . 13
283	183	oveq2d 6056	. . . . . . . . . . . . 13
284	282, 283	oveq12d 6058	. . . . . . . . . . . 12
285	284	oveq2d 6056	. . . . . . . . . . 11
286	285	oveq2d 6056	. . . . . . . . . 10
287	286	oveq2d 6056	. . . . . . . . 9
288		elfznn 11036	. . . . . . . . . . . . . . . . 17
289	288	adantl 453	. . . . . . . . . . . . . . . 16 $/\$
290	112	a1i 11	. . . . . . . . . . . . . . . . . 18
291		oveq2 6048	. . . . . . . . . . . . . . . . . . . . 21
292	291	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . 21
293	291, 292	oveq12d 6058	. . . . . . . . . . . . . . . . . . . 20
294	291	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . 21
295	291, 294	oveq12d 6058	. . . . . . . . . . . . . . . . . . . 20
296	293, 295	oveq12d 6058	. . . . . . . . . . . . . . . . . . 19
297	296	adantl 453	. . . . . . . . . . . . . . . . . 18 $/\$
298		id 20	. . . . . . . . . . . . . . . . . 18
299		2rp 10573	. . . . . . . . . . . . . . . . . . . . . 22
300	299	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
301		nnrp 10577	. . . . . . . . . . . . . . . . . . . . 21
302	300, 301	rpmulcld 10620	. . . . . . . . . . . . . . . . . . . 20
303	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
304		nnre 9963	. . . . . . . . . . . . . . . . . . . . . . 23
305	303, 304	remulcld 9072	. . . . . . . . . . . . . . . . . . . . . 22
306	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
307	305, 306	resubcld 9421	. . . . . . . . . . . . . . . . . . . . 21
308		nnge1 9982	. . . . . . . . . . . . . . . . . . . . . . 23
309		nncn 9964	. . . . . . . . . . . . . . . . . . . . . . . . 25
310	309	mulid2d 9062	. . . . . . . . . . . . . . . . . . . . . . . 24
311	306, 303, 301	ltmul1d 10641	. . . . . . . . . . . . . . . . . . . . . . . . 25
312	265, 311	mpbii 203	. . . . . . . . . . . . . . . . . . . . . . . 24
313	310, 312	eqbrtrrd 4194	. . . . . . . . . . . . . . . . . . . . . . 23
314	306, 304, 305, 308, 313	lelttrd 9184	. . . . . . . . . . . . . . . . . . . . . 22
315	306, 305	posdifd 9569	. . . . . . . . . . . . . . . . . . . . . 22
316	314, 315	mpbid 202	. . . . . . . . . . . . . . . . . . . . 21
317	307, 316	elrpd 10602	. . . . . . . . . . . . . . . . . . . 20
318	302, 317	rpdivcld 10621	. . . . . . . . . . . . . . . . . . 19
319	163	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
320	301	rpge0d 10608	. . . . . . . . . . . . . . . . . . . . . 22
321	303, 304, 319, 320	mulge0d 9559	. . . . . . . . . . . . . . . . . . . . 21
322	305, 321	ge0p1rpd 10630	. . . . . . . . . . . . . . . . . . . 20
323	302, 322	rpdivcld 10621	. . . . . . . . . . . . . . . . . . 19
324	318, 323	rpmulcld 10620	. . . . . . . . . . . . . . . . . 18
325	290, 297, 298, 324	fvmptd 5769	. . . . . . . . . . . . . . . . 17
326	325, 324	eqeltrd 2478	. . . . . . . . . . . . . . . 16
327	289, 326	syl 16	. . . . . . . . . . . . . . 15 $/\$
328		rpmulcl 10589	. . . . . . . . . . . . . . . 16 $/\$
329	328	adantl 453	. . . . . . . . . . . . . . 15 $/\$ $/\$
330	252, 327, 329	seqcl 11298	. . . . . . . . . . . . . 14
331	330	rpcnne0d 10613	. . . . . . . . . . . . 13 $/\$
332	299	a1i 11	. . . . . . . . . . . . . . . . 17
333	157, 166	ge0p1rpd 10630	. . . . . . . . . . . . . . . . 17
334	332, 333	rpmulcld 10620	. . . . . . . . . . . . . . . 16
335	156, 157, 164, 166	mulge0d 9559	. . . . . . . . . . . . . . . . 17
336	188, 335	ge0p1rpd 10630	. . . . . . . . . . . . . . . 16
337	334, 336	rpdivcld 10621	. . . . . . . . . . . . . . 15
338	332, 267	rpmulcld 10620	. . . . . . . . . . . . . . . . 17
339	338, 224	rpaddcld 10619	. . . . . . . . . . . . . . . 16
340	334, 339	rpdivcld 10621	. . . . . . . . . . . . . . 15
341	337, 340	rpmulcld 10620	. . . . . . . . . . . . . 14
342	341	rpcnne0d 10613	. . . . . . . . . . . . 13 $/\$
343		divdiv1 9681	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
344	131, 331, 342, 343	syl3anc 1184	. . . . . . . . . . . 12
345	344	eqcomd 2409	. . . . . . . . . . 11
346	345	oveq2d 6056	. . . . . . . . . 10
347	66	a1i 11	. . . . . . . . . . 11
348	330	rpcnd 10606	. . . . . . . . . . . 12
349	330	rpne0d 10609	. . . . . . . . . . . 12
350	348, 349	reccld 9739	. . . . . . . . . . 11
351	341	rpcnd 10606	. . . . . . . . . . 11
352	341	rpne0d 10609	. . . . . . . . . . 11
353	347, 350, 351, 352	divassd 9781	. . . . . . . . . 10
354	141, 271	eqnetrrd 2587	. . . . . . . . . . . . 13
355	205, 203, 205, 217, 354, 227	divmuldivd 9787	. . . . . . . . . . . 12
356	355	oveq2d 6056	. . . . . . . . . . 11
357	347, 350	mulcld 9064	. . . . . . . . . . . . 13
358	205, 205	mulcld 9064	. . . . . . . . . . . . 13
359	203, 217	mulcld 9064	. . . . . . . . . . . . 13
360	205, 205, 209, 209	mulne0d 9630	. . . . . . . . . . . . 13
361	203, 217, 354, 227	mulne0d 9630	. . . . . . . . . . . . 13
362	357, 358, 359, 360, 361	divdiv2d 9778	. . . . . . . . . . . 12
363	357, 359, 358, 360	divassd 9781	. . . . . . . . . . . 12
364	362, 363	eqtrd 2436	. . . . . . . . . . 11
365	203, 205, 205, 217, 209, 227, 209	divdivdivd 9793	. . . . . . . . . . . . 13
366	365	eqcomd 2409	. . . . . . . . . . . 12
367	366	oveq2d 6056	. . . . . . . . . . 11
368	356, 364, 367	3eqtrd 2440	. . . . . . . . . 10
369	346, 353, 368	3eqtr2d 2442	. . . . . . . . 9
370	63	a1i 11	. . . . . . . . . . . 12
371	370	halfcld 10168	. . . . . . . . . . 11
372	371, 350	mulcld 9064	. . . . . . . . . 10
373	210, 228, 229	divcld 9746	. . . . . . . . . 10
374	372, 373	mulcomd 9065	. . . . . . . . 9
375	287, 369, 374	3eqtrd 2440	. . . . . . . 8
376	281, 375	eqtrd 2436	. . . . . . 7
377	376	adantr 452	. . . . . 6 $/\$
378	128, 250, 377	3eqtr4d 2446	. . . . 5 $/\$
379	378	ex 424	. . . 4
380	9, 18, 27, 36, 126, 379	nnind 9974	. . 3
381	380	mpteq2ia 4251	. 2
382		wallispilem4.3	. 2
383		wallispilem4.4	. 2
384	381, 382, 383	3eqtr4i 2434	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 359

wceq 1649

wcel 1721

wne 2567 class class class wbr 4172

cmpt 4226

cfv 5413 (class class class)co 6040

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

clt 9076

cle 9077

cmin 9247

cdiv 9633

cn 9956

c2 10005

c3 10006

cn0 10177

cz 10238

cuz 10444

crp 10568

cioo 10872

cfz 10999

cseq 11278

cexp 11337

csin 12621

cpi 12624

citg 19463

This theorem is referenced by: wallispilem5 27685

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cc 8271 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-disj 4143 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-ofr 6265 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-omul 6688 df-er 6864 df-map 6979 df-pm 6980 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-acn 7785 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ioc 10877 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-shft 11837 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-limsup 12220 df-clim 12237 df-rlim 12238 df-sum 12435 df-ef 12625 df-sin 12627 df-cos 12628 df-pi 12630 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-sca 13500 df-vsca 13501 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-hom 13508 df-cco 13509 df-rest 13605 df-topn 13606 df-topgen 13622 df-pt 13623 df-prds 13626 df-xrs 13681 df-0g 13682 df-gsum 13683 df-qtop 13688 df-imas 13689 df-xps 13691 df-mre 13766 df-mrc 13767 df-acs 13769 df-mnd 14645 df-submnd 14694 df-mulg 14770 df-cntz 15071 df-cmn 15369 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-fbas 16654 df-fg 16655 df-cnfld 16659 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cld 17038 df-ntr 17039 df-cls 17040 df-nei 17117 df-lp 17155 df-perf 17156 df-cn 17245 df-cnp 17246 df-haus 17333 df-cmp 17404 df-tx 17547 df-hmeo 17740 df-fil 17831 df-fm 17923 df-flim 17924 df-flf 17925 df-xms 18303 df-ms 18304 df-tms 18305 df-cncf 18861 df-ovol 19314 df-vol 19315 df-mbf 19465 df-itg1 19466 df-itg2 19467 df-ibl 19468 df-itg 19469 df-0p 19515 df-limc 19706 df-dv 19707

W3C validator