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 32053

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 6304	. . . . . . 7
2	1	fveq2d 5876	. . . . . 6
3	1	oveq1d 6311	. . . . . . 7
4	3	fveq2d 5876	. . . . . 6
5	2, 4	oveq12d 6314	. . . . 5
6		fveq2 5872	. . . . . . 7
7	6	oveq2d 6312	. . . . . 6
8	7	oveq2d 6312	. . . . 5
9	5, 8	eqeq12d 2479	. . . 4
10		oveq2 6304	. . . . . . 7
11	10	fveq2d 5876	. . . . . 6
12	10	oveq1d 6311	. . . . . . 7
13	12	fveq2d 5876	. . . . . 6
14	11, 13	oveq12d 6314	. . . . 5
15		fveq2 5872	. . . . . . 7
16	15	oveq2d 6312	. . . . . 6
17	16	oveq2d 6312	. . . . 5
18	14, 17	eqeq12d 2479	. . . 4
19		oveq2 6304	. . . . . . 7
20	19	fveq2d 5876	. . . . . 6
21	19	oveq1d 6311	. . . . . . 7
22	21	fveq2d 5876	. . . . . 6
23	20, 22	oveq12d 6314	. . . . 5
24		fveq2 5872	. . . . . . 7
25	24	oveq2d 6312	. . . . . 6
26	25	oveq2d 6312	. . . . 5
27	23, 26	eqeq12d 2479	. . . 4
28		oveq2 6304	. . . . . . 7
29	28	fveq2d 5876	. . . . . 6
30	28	oveq1d 6311	. . . . . . 7
31	30	fveq2d 5876	. . . . . 6
32	29, 31	oveq12d 6314	. . . . 5
33		fveq2 5872	. . . . . . 7
34	33	oveq2d 6312	. . . . . 6
35	34	oveq2d 6312	. . . . 5
36	32, 35	eqeq12d 2479	. . . 4
37		2t1e2 10705	. . . . . . 7
38	37	fveq2i 5875	. . . . . 6
39	37	oveq1i 6306	. . . . . . . 8
40		2p1e3 10680	. . . . . . . 8
41	39, 40	eqtri 2486	. . . . . . 7
42	41	fveq2i 5875	. . . . . 6
43	38, 42	oveq12i 6308	. . . . 5
44		2z 10917	. . . . . . . . 9
45		uzid 11120	. . . . . . . . 9
46	44, 45	ax-mp 5	. . . . . . . 8
47		wallispilem4.2	. . . . . . . . . 10
48	47	wallispilem2 32051	. . . . . . . . 9 $/\$ $/\$
49	48	simp3i 1007	. . . . . . . 8
50	46, 49	ax-mp 5	. . . . . . 7
51		2m1e1 10671	. . . . . . . . 9
52	51	oveq1i 6306	. . . . . . . 8
53		2cn 10627	. . . . . . . . . . 11
54	53	subidi 9909	. . . . . . . . . 10
55	54	fveq2i 5875	. . . . . . . . 9
56	48	simp1i 1005	. . . . . . . . 9
57	55, 56	eqtri 2486	. . . . . . . 8
58	52, 57	oveq12i 6308	. . . . . . 7
59		ax-1cn 9567	. . . . . . . . 9
60		2cnne0 10771	. . . . . . . . 9 $/\$
61		picn 22978	. . . . . . . . 9
62		div32 10248	. . . . . . . . 9 $/\$ $/\$ $/\$
63	59, 60, 61, 62	mp3an 1324	. . . . . . . 8
64		2ne0 10649	. . . . . . . . . 10
65	61, 53, 64	divcli 10307	. . . . . . . . 9
66	65	mulid2i 9616	. . . . . . . 8
67	63, 66	eqtri 2486	. . . . . . 7
68	50, 58, 67	3eqtri 2490	. . . . . 6
69		3z 10918	. . . . . . . . 9
70		2re 10626	. . . . . . . . . 10
71		3re 10630	. . . . . . . . . 10
72		2lt3 10724	. . . . . . . . . 10
73	70, 71, 72	ltleii 9724	. . . . . . . . 9
74		eluz2 11112	. . . . . . . . 9 $/\$ $/\$
75	44, 69, 73, 74	mpbir3an 1178	. . . . . . . 8
76	47	wallispilem2 32051	. . . . . . . . 9 $/\$ $/\$
77	76	simp3i 1007	. . . . . . . 8
78	75, 77	ax-mp 5	. . . . . . 7
79		3m1e2 10673	. . . . . . . . . 10
80	79	eqcomi 2470	. . . . . . . . 9
81	80	oveq1i 6306	. . . . . . . 8
82		3cn 10631	. . . . . . . . . . 11
83	82, 53, 59, 40	subaddrii 9928	. . . . . . . . . 10
84	83	fveq2i 5875	. . . . . . . . 9
85	48	simp2i 1006	. . . . . . . . 9
86	84, 85	eqtr2i 2487	. . . . . . . 8
87	81, 86	oveq12i 6308	. . . . . . 7
88		3ne0 10651	. . . . . . . . 9
89	53, 82, 88	divcli 10307	. . . . . . . 8
90	89, 53	mulcomi 9619	. . . . . . 7
91	78, 87, 90	3eqtr2i 2492	. . . . . 6
92	68, 91	oveq12i 6308	. . . . 5
93		1z 10915	. . . . . . . . 9
94		seq1 12123	. . . . . . . . 9
95	93, 94	ax-mp 5	. . . . . . . 8
96		1nn 10567	. . . . . . . . 9
97		oveq2 6304	. . . . . . . . . . . . . 14
98	97, 37	syl6eq 2514	. . . . . . . . . . . . 13
99	97	oveq1d 6311	. . . . . . . . . . . . . 14
100	37	oveq1i 6306	. . . . . . . . . . . . . . 15
101	100, 51	eqtri 2486	. . . . . . . . . . . . . 14
102	99, 101	syl6eq 2514	. . . . . . . . . . . . 13
103	98, 102	oveq12d 6314	. . . . . . . . . . . 12
104	53	div1i 10293	. . . . . . . . . . . 12
105	103, 104	syl6eq 2514	. . . . . . . . . . 11
106	98	oveq1d 6311	. . . . . . . . . . . . 13
107	106, 40	syl6eq 2514	. . . . . . . . . . . 12
108	98, 107	oveq12d 6314	. . . . . . . . . . 11
109	105, 108	oveq12d 6314	. . . . . . . . . 10
110		wallispilem4.1	. . . . . . . . . 10
111		ovex 6324	. . . . . . . . . 10
112	109, 110, 111	fvmpt 5956	. . . . . . . . 9
113	96, 112	ax-mp 5	. . . . . . . 8
114	95, 113	eqtr2i 2487	. . . . . . 7
115	114	oveq2i 6307	. . . . . 6
116	53, 89	mulcli 9618	. . . . . . . . 9
117	113, 116	eqeltri 2541	. . . . . . . 8
118	95, 117	eqeltri 2541	. . . . . . 7
119	53, 82, 64, 88	divne0i 10313	. . . . . . . . 9
120	53, 89, 64, 119	mulne0i 10213	. . . . . . . 8
121	114, 120	eqnetrri 2754	. . . . . . 7
122	65, 118, 121	divreci 10310	. . . . . 6
123	115, 122	eqtri 2486	. . . . 5
124	43, 92, 123	3eqtri 2490	. . . 4
125		oveq2 6304	. . . . . . 7
126	125	adantl 466	. . . . . 6 $/\$
127		2cnd 10629	. . . . . . . . . . . . . . . 16
128		nncn 10564	. . . . . . . . . . . . . . . 16
129	59	a1i 11	. . . . . . . . . . . . . . . 16
130	127, 128, 129	adddid 9637	. . . . . . . . . . . . . . 15
131	127	mulid1d 9630	. . . . . . . . . . . . . . . 16
132	131	oveq2d 6312	. . . . . . . . . . . . . . 15
133	130, 132	eqtrd 2498	. . . . . . . . . . . . . 14
134	133	oveq1d 6311	. . . . . . . . . . . . 13
135	127, 128	mulcld 9633	. . . . . . . . . . . . . 14
136	135, 127, 129	addsubassd 9970	. . . . . . . . . . . . 13
137	51	a1i 11	. . . . . . . . . . . . . 14
138	137	oveq2d 6312	. . . . . . . . . . . . 13
139	134, 136, 138	3eqtrd 2502	. . . . . . . . . . . 12
140	139	oveq1d 6311	. . . . . . . . . . 11
141	140	oveq1d 6311	. . . . . . . . . 10
142	79	a1i 11	. . . . . . . . . . . . . 14
143	142	oveq2d 6312	. . . . . . . . . . . . 13
144	82	a1i 11	. . . . . . . . . . . . . 14
145	135, 144, 129	addsubassd 9970	. . . . . . . . . . . . 13
146	143, 145, 133	3eqtr4d 2508	. . . . . . . . . . . 12
147	146	oveq1d 6311	. . . . . . . . . . 11
148	147	oveq1d 6311	. . . . . . . . . 10
149	141, 148	oveq12d 6314	. . . . . . . . 9
150	44	a1i 11	. . . . . . . . . . . . . 14
151		nnz 10907	. . . . . . . . . . . . . . 15
152	151	peano2zd 10993	. . . . . . . . . . . . . 14
153	150, 152	zmulcld 10996	. . . . . . . . . . . . 13
154	70	a1i 11	. . . . . . . . . . . . . 14
155		nnre 10563	. . . . . . . . . . . . . . 15
156		1red 9628	. . . . . . . . . . . . . . 15
157	155, 156	readdcld 9640	. . . . . . . . . . . . . 14
158		0le2 10647	. . . . . . . . . . . . . . 15
159	158	a1i 11	. . . . . . . . . . . . . 14
160		nnnn0 10823	. . . . . . . . . . . . . . . 16
161	160	nn0ge0d 10876	. . . . . . . . . . . . . . 15
162	156, 155	addge02d 10162	. . . . . . . . . . . . . . 15
163	161, 162	mpbid 210	. . . . . . . . . . . . . 14
164	154, 157, 159, 163	lemulge11d 10503	. . . . . . . . . . . . 13
165	44	eluz1i 11113	. . . . . . . . . . . . 13 $/\$
166	153, 164, 165	sylanbrc 664	. . . . . . . . . . . 12
167	47, 166	itgsinexp 31956	. . . . . . . . . . 11
168	133	oveq1d 6311	. . . . . . . . . . . . . 14
169	135, 127	pncand 9951	. . . . . . . . . . . . . 14
170	168, 169	eqtrd 2498	. . . . . . . . . . . . 13
171	170	fveq2d 5876	. . . . . . . . . . . 12
172	171	oveq2d 6312	. . . . . . . . . . 11
173	167, 172	eqtrd 2498	. . . . . . . . . 10
174	133	oveq1d 6311	. . . . . . . . . . . . 13
175	135, 127, 129	addassd 9635	. . . . . . . . . . . . 13
176	40	a1i 11	. . . . . . . . . . . . . 14
177	176	oveq2d 6312	. . . . . . . . . . . . 13
178	174, 175, 177	3eqtrd 2502	. . . . . . . . . . . 12
179	178	fveq2d 5876	. . . . . . . . . . 11
180	150, 151	zmulcld 10996	. . . . . . . . . . . . . 14
181	69	a1i 11	. . . . . . . . . . . . . 14
182	180, 181	zaddcld 10994	. . . . . . . . . . . . 13
183	154, 155	remulcld 9641	. . . . . . . . . . . . . 14
184	71	a1i 11	. . . . . . . . . . . . . . 15
185	183, 184	readdcld 9640	. . . . . . . . . . . . . 14
186		nnge1 10582	. . . . . . . . . . . . . . 15
187	154, 155, 159, 186	lemulge11d 10503	. . . . . . . . . . . . . 14
188		0re 9613	. . . . . . . . . . . . . . . 16
189		3pos 10650	. . . . . . . . . . . . . . . 16
190	188, 71, 189	ltleii 9724	. . . . . . . . . . . . . . 15
191	183, 184	addge01d 10161	. . . . . . . . . . . . . . 15
192	190, 191	mpbii 211	. . . . . . . . . . . . . 14
193	154, 183, 185, 187, 192	letrd 9756	. . . . . . . . . . . . 13
194	44	eluz1i 11113	. . . . . . . . . . . . 13 $/\$
195	182, 193, 194	sylanbrc 664	. . . . . . . . . . . 12
196	47, 195	itgsinexp 31956	. . . . . . . . . . 11
197	179, 196	eqtrd 2498	. . . . . . . . . 10
198	173, 197	oveq12d 6314	. . . . . . . . 9
199	135, 129	addcld 9632	. . . . . . . . . . 11
200	128, 129	addcld 9632	. . . . . . . . . . . 12
201	127, 200	mulcld 9633	. . . . . . . . . . 11
202	64	a1i 11	. . . . . . . . . . . 12
203		peano2nn 10568	. . . . . . . . . . . . 13
204	203	nnne0d 10601	. . . . . . . . . . . 12
205	127, 200, 202, 204	mulne0d 10222	. . . . . . . . . . 11
206	199, 201, 205	divcld 10341	. . . . . . . . . 10
207		2nn0 10833	. . . . . . . . . . . . 13
208	207	a1i 11	. . . . . . . . . . . 12
209	208, 160	nn0mulcld 10878	. . . . . . . . . . 11
210	47	wallispilem3 32052	. . . . . . . . . . . 12
211	210	rpcnd 11283	. . . . . . . . . . 11
212	209, 211	syl 16	. . . . . . . . . 10
213	135, 144	addcld 9632	. . . . . . . . . . . 12
214		0red 9614	. . . . . . . . . . . . . 14
215		2pos 10648	. . . . . . . . . . . . . . . 16
216	215	a1i 11	. . . . . . . . . . . . . . 15
217		nngt0 10585	. . . . . . . . . . . . . . 15
218	154, 155, 216, 217	mulgt0d 9754	. . . . . . . . . . . . . 14
219	184, 189	jctir 538	. . . . . . . . . . . . . . . 16 $/\$
220		elrp 11247	. . . . . . . . . . . . . . . 16 $/\$
221	219, 220	sylibr 212	. . . . . . . . . . . . . . 15
222	183, 221	ltaddrpd 11310	. . . . . . . . . . . . . 14
223	214, 183, 185, 218, 222	lttrd 9760	. . . . . . . . . . . . 13
224	223	gt0ne0d 10138	. . . . . . . . . . . 12
225	201, 213, 224	divcld 10341	. . . . . . . . . . 11
226	201, 213, 205, 224	divne0d 10357	. . . . . . . . . . 11
227	182, 150	zsubcld 10995	. . . . . . . . . . . . . 14
228	185, 154	subge0d 10163	. . . . . . . . . . . . . . 15
229	193, 228	mpbird 232	. . . . . . . . . . . . . 14
230		elnn0z 10898	. . . . . . . . . . . . . 14 $/\$
231	227, 229, 230	sylanbrc 664	. . . . . . . . . . . . 13
232	47	wallispilem3 32052	. . . . . . . . . . . . 13
233	231, 232	syl 16	. . . . . . . . . . . 12
234	233	rpcnne0d 11290	. . . . . . . . . . 11 $/\$
235	225, 226, 234	jca31 534	. . . . . . . . . 10 $/\$ $/\$ $/\$
236		divmuldiv 10265	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
237	206, 212, 235, 236	syl21anc 1227	. . . . . . . . 9
238	149, 198, 237	3eqtr4d 2508	. . . . . . . 8
239	135, 144, 127	addsubassd 9970	. . . . . . . . . . . 12
240	83	a1i 11	. . . . . . . . . . . . 13
241	240	oveq2d 6312	. . . . . . . . . . . 12
242	239, 241	eqtrd 2498	. . . . . . . . . . 11
243	242	fveq2d 5876	. . . . . . . . . 10
244	243	oveq2d 6312	. . . . . . . . 9
245	244	oveq2d 6312	. . . . . . . 8
246	238, 245	eqtrd 2498	. . . . . . 7
247	246	adantr 465	. . . . . 6 $/\$
248		elnnuz 11142	. . . . . . . . . . . . 13
249	248	biimpi 194	. . . . . . . . . . . 12
250		seqp1 12125	. . . . . . . . . . . 12
251	249, 250	syl 16	. . . . . . . . . . 11
252	110	a1i 11	. . . . . . . . . . . . 13
253		oveq2 6304	. . . . . . . . . . . . . . . 16
254	253	oveq1d 6311	. . . . . . . . . . . . . . . 16
255	253, 254	oveq12d 6314	. . . . . . . . . . . . . . 15
256	253	oveq1d 6311	. . . . . . . . . . . . . . . 16
257	253, 256	oveq12d 6314	. . . . . . . . . . . . . . 15
258	255, 257	oveq12d 6314	. . . . . . . . . . . . . 14
259	258	adantl 466	. . . . . . . . . . . . 13 $/\$
260	154, 157	remulcld 9641	. . . . . . . . . . . . . . 15
261	260, 156	resubcld 10008	. . . . . . . . . . . . . . 15
262		1lt2 10723	. . . . . . . . . . . . . . . . . . 19
263	262	a1i 11	. . . . . . . . . . . . . . . . . 18
264		nnrp 11254	. . . . . . . . . . . . . . . . . . 19
265	156, 264	ltaddrp2d 11311	. . . . . . . . . . . . . . . . . 18
266	154, 157, 263, 265	mulgt1d 10502	. . . . . . . . . . . . . . . . 17
267	156, 266	gtned 9737	. . . . . . . . . . . . . . . 16
268	201, 129, 267	subne0d 9959	. . . . . . . . . . . . . . 15
269	260, 261, 268	redivcld 10393	. . . . . . . . . . . . . 14
270	178, 185	eqeltrd 2545	. . . . . . . . . . . . . . 15
271	178, 224	eqnetrd 2750	. . . . . . . . . . . . . . 15
272	260, 270, 271	redivcld 10393	. . . . . . . . . . . . . 14
273	269, 272	remulcld 9641	. . . . . . . . . . . . 13
274	252, 259, 203, 273	fvmptd 5961	. . . . . . . . . . . 12
275	274	oveq2d 6312	. . . . . . . . . . 11
276	251, 275	eqtrd 2498	. . . . . . . . . 10
277	276	oveq2d 6312	. . . . . . . . 9
278	277	oveq2d 6312	. . . . . . . 8
279	139	oveq2d 6312	. . . . . . . . . . . . 13
280	178	oveq2d 6312	. . . . . . . . . . . . 13
281	279, 280	oveq12d 6314	. . . . . . . . . . . 12
282	281	oveq2d 6312	. . . . . . . . . . 11
283	282	oveq2d 6312	. . . . . . . . . 10
284	283	oveq2d 6312	. . . . . . . . 9
285		elfznn 11739	. . . . . . . . . . . . . . . . 17
286	285	adantl 466	. . . . . . . . . . . . . . . 16 $/\$
287	110	a1i 11	. . . . . . . . . . . . . . . . . 18
288		oveq2 6304	. . . . . . . . . . . . . . . . . . . . 21
289	288	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . 21
290	288, 289	oveq12d 6314	. . . . . . . . . . . . . . . . . . . 20
291	288	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . 21
292	288, 291	oveq12d 6314	. . . . . . . . . . . . . . . . . . . 20
293	290, 292	oveq12d 6314	. . . . . . . . . . . . . . . . . . 19
294	293	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
295		id 22	. . . . . . . . . . . . . . . . . 18
296		2rp 11250	. . . . . . . . . . . . . . . . . . . . . 22
297	296	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
298		nnrp 11254	. . . . . . . . . . . . . . . . . . . . 21
299	297, 298	rpmulcld 11297	. . . . . . . . . . . . . . . . . . . 20
300	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
301		nnre 10563	. . . . . . . . . . . . . . . . . . . . . . 23
302	300, 301	remulcld 9641	. . . . . . . . . . . . . . . . . . . . . 22
303		1red 9628	. . . . . . . . . . . . . . . . . . . . . 22
304	302, 303	resubcld 10008	. . . . . . . . . . . . . . . . . . . . 21
305		nnge1 10582	. . . . . . . . . . . . . . . . . . . . . . 23
306		nncn 10564	. . . . . . . . . . . . . . . . . . . . . . . . 25
307	306	mulid2d 9631	. . . . . . . . . . . . . . . . . . . . . . . 24
308	303, 300, 298	ltmul1d 11318	. . . . . . . . . . . . . . . . . . . . . . . . 25
309	262, 308	mpbii 211	. . . . . . . . . . . . . . . . . . . . . . . 24
310	307, 309	eqbrtrrd 4478	. . . . . . . . . . . . . . . . . . . . . . 23
311	303, 301, 302, 305, 310	lelttrd 9757	. . . . . . . . . . . . . . . . . . . . . 22
312	303, 302	posdifd 10160	. . . . . . . . . . . . . . . . . . . . . 22
313	311, 312	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21
314	304, 313	elrpd 11279	. . . . . . . . . . . . . . . . . . . 20
315	299, 314	rpdivcld 11298	. . . . . . . . . . . . . . . . . . 19
316	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
317	298	rpge0d 11285	. . . . . . . . . . . . . . . . . . . . . 22
318	300, 301, 316, 317	mulge0d 10150	. . . . . . . . . . . . . . . . . . . . 21
319	302, 318	ge0p1rpd 11307	. . . . . . . . . . . . . . . . . . . 20
320	299, 319	rpdivcld 11298	. . . . . . . . . . . . . . . . . . 19
321	315, 320	rpmulcld 11297	. . . . . . . . . . . . . . . . . 18
322	287, 294, 295, 321	fvmptd 5961	. . . . . . . . . . . . . . . . 17
323	322, 321	eqeltrd 2545	. . . . . . . . . . . . . . . 16
324	286, 323	syl 16	. . . . . . . . . . . . . . 15 $/\$
325		rpmulcl 11266	. . . . . . . . . . . . . . . 16 $/\$
326	325	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
327	249, 324, 326	seqcl 12130	. . . . . . . . . . . . . 14
328	327	rpcnne0d 11290	. . . . . . . . . . . . 13 $/\$
329	296	a1i 11	. . . . . . . . . . . . . . . . 17
330	155, 161	ge0p1rpd 11307	. . . . . . . . . . . . . . . . 17
331	329, 330	rpmulcld 11297	. . . . . . . . . . . . . . . 16
332	154, 155, 159, 161	mulge0d 10150	. . . . . . . . . . . . . . . . 17
333	183, 332	ge0p1rpd 11307	. . . . . . . . . . . . . . . 16
334	331, 333	rpdivcld 11298	. . . . . . . . . . . . . . 15
335	329, 264	rpmulcld 11297	. . . . . . . . . . . . . . . . 17
336	335, 221	rpaddcld 11296	. . . . . . . . . . . . . . . 16
337	331, 336	rpdivcld 11298	. . . . . . . . . . . . . . 15
338	334, 337	rpmulcld 11297	. . . . . . . . . . . . . 14
339	338	rpcnne0d 11290	. . . . . . . . . . . . 13 $/\$
340		divdiv1 10276	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
341	129, 328, 339, 340	syl3anc 1228	. . . . . . . . . . . 12
342	341	eqcomd 2465	. . . . . . . . . . 11
343	342	oveq2d 6312	. . . . . . . . . 10
344	65	a1i 11	. . . . . . . . . . 11
345	327	rpcnd 11283	. . . . . . . . . . . 12
346	327	rpne0d 11286	. . . . . . . . . . . 12
347	345, 346	reccld 10334	. . . . . . . . . . 11
348	338	rpcnd 11283	. . . . . . . . . . 11
349	338	rpne0d 11286	. . . . . . . . . . 11
350	344, 347, 348, 349	divassd 10376	. . . . . . . . . 10
351	139, 268	eqnetrrd 2751	. . . . . . . . . . . . 13
352	201, 199, 201, 213, 351, 224	divmuldivd 10382	. . . . . . . . . . . 12
353	352	oveq2d 6312	. . . . . . . . . . 11
354	344, 347	mulcld 9633	. . . . . . . . . . . . 13
355	201, 201	mulcld 9633	. . . . . . . . . . . . 13
356	199, 213	mulcld 9633	. . . . . . . . . . . . 13
357	201, 201, 205, 205	mulne0d 10222	. . . . . . . . . . . . 13
358	199, 213, 351, 224	mulne0d 10222	. . . . . . . . . . . . 13
359	354, 355, 356, 357, 358	divdiv2d 10373	. . . . . . . . . . . 12
360	354, 356, 355, 357	divassd 10376	. . . . . . . . . . . 12
361	359, 360	eqtrd 2498	. . . . . . . . . . 11
362	199, 201, 201, 213, 205, 224, 205	divdivdivd 10388	. . . . . . . . . . . . 13
363	362	eqcomd 2465	. . . . . . . . . . . 12
364	363	oveq2d 6312	. . . . . . . . . . 11
365	353, 361, 364	3eqtrd 2502	. . . . . . . . . 10
366	343, 350, 365	3eqtr2d 2504	. . . . . . . . 9
367	61	a1i 11	. . . . . . . . . . . 12
368	367	halfcld 10804	. . . . . . . . . . 11
369	368, 347	mulcld 9633	. . . . . . . . . 10
370	206, 225, 226	divcld 10341	. . . . . . . . . 10
371	369, 370	mulcomd 9634	. . . . . . . . 9
372	284, 366, 371	3eqtrd 2502	. . . . . . . 8
373	278, 372	eqtrd 2498	. . . . . . 7
374	373	adantr 465	. . . . . 6 $/\$
375	126, 247, 374	3eqtr4d 2508	. . . . 5 $/\$
376	375	ex 434	. . . 4
377	9, 18, 27, 36, 124, 376	nnind 10574	. . 3
378	377	mpteq2ia 4539	. 2
379		wallispilem4.3	. 2
380		wallispilem4.4	. 2
381	378, 379, 380	3eqtr4i 2496	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1395

wcel 1819

wne 2652 class class class wbr 4456

cmpt 4515

cfv 5594 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

cmul 9514

clt 9645

cle 9646

cmin 9824

cdiv 10227

cn 10556

c2 10606

c3 10607

cn0 10816

cz 10885

cuz 11106

crp 11245

cioo 11554

cfz 11697

cseq 12110

cexp 12169

csin 13811

cpi 13814

citg 22153

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cc 8832 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587 ax-addf 9588 ax-mulf 9589

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-iin 4335 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-ofr 6540 df-om 6700 df-1st 6799 df-2nd 6800 df-supp 6918 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-omul 7153 df-er 7329 df-map 7440 df-pm 7441 df-ixp 7489 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fsupp 7848 df-fi 7889 df-sup 7919 df-oi 7953 df-card 8337 df-acn 8340 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-ioo 11558 df-ioc 11559 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11822 df-fl 11932 df-mod 12000 df-seq 12111 df-exp 12170 df-fac 12357 df-bc 12384 df-hash 12409 df-shft 12912 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-limsup 13306 df-clim 13323 df-rlim 13324 df-sum 13521 df-ef 13815 df-sin 13817 df-cos 13818 df-pi 13820 df-struct 14646 df-ndx 14647 df-slot 14648 df-base 14649 df-sets 14650 df-ress 14651 df-plusg 14725 df-mulr 14726 df-starv 14727 df-sca 14728 df-vsca 14729 df-ip 14730 df-tset 14731 df-ple 14732 df-ds 14734 df-unif 14735 df-hom 14736 df-cco 14737 df-rest 14840 df-topn 14841 df-0g 14859 df-gsum 14860 df-topgen 14861 df-pt 14862 df-prds 14865 df-xrs 14919 df-qtop 14924 df-imas 14925 df-xps 14927 df-mre 15003 df-mrc 15004 df-acs 15006 df-mgm 15999 df-sgrp 16038 df-mnd 16048 df-submnd 16094 df-mulg 16187 df-cntz 16482 df-cmn 16927 df-psmet 18538 df-xmet 18539 df-met 18540 df-bl 18541 df-mopn 18542 df-fbas 18543 df-fg 18544 df-cnfld 18548 df-top 19526 df-bases 19528 df-topon 19529 df-topsp 19530 df-cld 19647 df-ntr 19648 df-cls 19649 df-nei 19726 df-lp 19764 df-perf 19765 df-cn 19855 df-cnp 19856 df-haus 19943 df-cmp 20014 df-tx 20189 df-hmeo 20382 df-fil 20473 df-fm 20565 df-flim 20566 df-flf 20567 df-xms 20949 df-ms 20950 df-tms 20951 df-cncf 21508 df-ovol 22002 df-vol 22003 df-mbf 22154 df-itg1 22155 df-itg2 22156 df-ibl 22157 df-itg 22158 df-0p 22203 df-limc 22396 df-dv 22397

This theorem is referenced by: wallispilem5 32054

W3C validator