wallispi2lem2 - Mathbox for Glauco Siliprandi

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

Theorem wallispi2lem2 40289

Description: Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017.)

**Assertion**
Ref	Expression
wallispi2lem2

Proof of Theorem wallispi2lem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6191	. . 3
2		oveq2 6658	. . . . . 6
3	2	oveq2d 6666	. . . . 5
4		fveq2 6191	. . . . . 6
5	4	oveq1d 6665	. . . . 5
6	3, 5	oveq12d 6668	. . . 4
7		oveq2 6658	. . . . . 6
8	7	fveq2d 6195	. . . . 5
9	8	oveq1d 6665	. . . 4
10	6, 9	oveq12d 6668	. . 3
11	1, 10	eqeq12d 2637	. 2
12		fveq2 6191	. . 3
13		oveq2 6658	. . . . . 6
14	13	oveq2d 6666	. . . . 5
15		fveq2 6191	. . . . . 6
16	15	oveq1d 6665	. . . . 5
17	14, 16	oveq12d 6668	. . . 4
18		oveq2 6658	. . . . . 6
19	18	fveq2d 6195	. . . . 5
20	19	oveq1d 6665	. . . 4
21	17, 20	oveq12d 6668	. . 3
22	12, 21	eqeq12d 2637	. 2
23		fveq2 6191	. . 3
24		oveq2 6658	. . . . . 6
25	24	oveq2d 6666	. . . . 5
26		fveq2 6191	. . . . . 6
27	26	oveq1d 6665	. . . . 5
28	25, 27	oveq12d 6668	. . . 4
29		oveq2 6658	. . . . . 6
30	29	fveq2d 6195	. . . . 5
31	30	oveq1d 6665	. . . 4
32	28, 31	oveq12d 6668	. . 3
33	23, 32	eqeq12d 2637	. 2
34		fveq2 6191	. . 3
35		oveq2 6658	. . . . . 6
36	35	oveq2d 6666	. . . . 5
37		fveq2 6191	. . . . . 6
38	37	oveq1d 6665	. . . . 5
39	36, 38	oveq12d 6668	. . . 4
40		oveq2 6658	. . . . . 6
41	40	fveq2d 6195	. . . . 5
42	41	oveq1d 6665	. . . 4
43	39, 42	oveq12d 6668	. . 3
44	34, 43	eqeq12d 2637	. 2
45		1z 11407	. . . 4
46		seq1 12814	. . . 4
47	45, 46	ax-mp 5	. . 3
48		1nn 11031	. . . 4
49		oveq2 6658	. . . . . . 7
50	49	oveq1d 6665	. . . . . 6
51	49	oveq1d 6665	. . . . . . . 8
52	49, 51	oveq12d 6668	. . . . . . 7
53	52	oveq1d 6665	. . . . . 6
54	50, 53	oveq12d 6668	. . . . 5
55		eqid 2622	. . . . 5
56		ovex 6678	. . . . 5
57	54, 55, 56	fvmpt 6282	. . . 4
58	48, 57	ax-mp 5	. . 3
59		2t1e2 11176	. . . . . 6
60	59	oveq1i 6660	. . . . 5
61		2exp4 15794	. . . . . . 7 ;
62		1nn0 11308	. . . . . . . 8
63		6nn0 11313	. . . . . . . 8
64		0nn0 11307	. . . . . . . 8
65		1t1e1 11175	. . . . . . . . . 10
66	65	oveq1i 6660	. . . . . . . . 9
67		1p0e1 11133	. . . . . . . . 9
68	66, 67	eqtri 2644	. . . . . . . 8
69		6cn 11102	. . . . . . . . . 10
70	69	mulid1i 10042	. . . . . . . . 9
71	63	dec0h 11522	. . . . . . . . 9 ;
72	70, 71	eqtri 2644	. . . . . . . 8 ;
73	62, 62, 63, 61, 63, 64, 68, 72	decmul1c 11587	. . . . . . 7 ;
74	61, 73	eqtr4i 2647	. . . . . 6
75		2nn0 11309	. . . . . . . . 9
76		2t2e4 11177	. . . . . . . . 9
77		sq1 12958	. . . . . . . . 9
78	62, 75, 76, 77, 65	numexp2x 15783	. . . . . . . 8
79	78	eqcomi 2631	. . . . . . 7
80	79	oveq2i 6661	. . . . . 6
81		4cn 11098	. . . . . . . . . 10
82	81	mulid1i 10042	. . . . . . . . 9
83	82	eqcomi 2631	. . . . . . . 8
84	83	oveq2i 6661	. . . . . . 7
85		fac1 13064	. . . . . . . . 9
86	85	eqcomi 2631	. . . . . . . 8
87	86	oveq1i 6660	. . . . . . 7
88	84, 87	oveq12i 6662	. . . . . 6
89	74, 80, 88	3eqtri 2648	. . . . 5
90	60, 89	eqtri 2644	. . . 4
91	59	oveq1i 6660	. . . . . . . 8
92		2m1e1 11135	. . . . . . . 8
93	91, 92	eqtri 2644	. . . . . . 7
94	93	oveq2i 6661	. . . . . 6
95	59	oveq1i 6660	. . . . . . 7
96	95, 59	eqtri 2644	. . . . . 6
97	59	fveq2i 6194	. . . . . . . 8
98		fac2 13066	. . . . . . . 8
99	97, 98	eqtri 2644	. . . . . . 7
100	99	eqcomi 2631	. . . . . 6
101	94, 96, 100	3eqtri 2648	. . . . 5
102	101	oveq1i 6660	. . . 4
103	90, 102	oveq12i 6662	. . 3
104	47, 58, 103	3eqtri 2648	. 2
105		elnnuz 11724	. . . . . . 7
106	105	biimpi 206	. . . . . 6
107	106	adantr 481	. . . . 5 $/\$
108		seqp1 12816	. . . . 5
109	107, 108	syl 17	. . . 4 $/\$
110		simpr 477	. . . . 5 $/\$
111	110	oveq1d 6665	. . . 4 $/\$
112		eqidd 2623	. . . . . . . 8
113		oveq2 6658	. . . . . . . . . . 11
114	113	oveq1d 6665	. . . . . . . . . 10
115	113	oveq1d 6665	. . . . . . . . . . . 12
116	113, 115	oveq12d 6668	. . . . . . . . . . 11
117	116	oveq1d 6665	. . . . . . . . . 10
118	114, 117	oveq12d 6668	. . . . . . . . 9
119	118	adantl 482	. . . . . . . 8 $/\$
120		peano2nn 11032	. . . . . . . 8
121		2cnd 11093	. . . . . . . . . . 11
122		nncn 11028	. . . . . . . . . . . 12
123		1cnd 10056	. . . . . . . . . . . 12
124	122, 123	addcld 10059	. . . . . . . . . . 11
125	121, 124	mulcld 10060	. . . . . . . . . 10
126		4nn0 11311	. . . . . . . . . . 11
127	126	a1i 11	. . . . . . . . . 10
128	125, 127	expcld 13008	. . . . . . . . 9
129	125, 123	subcld 10392	. . . . . . . . . . 11
130	125, 129	mulcld 10060	. . . . . . . . . 10
131	130	sqcld 13006	. . . . . . . . 9
132		2pos 11112	. . . . . . . . . . . . . 14
133	132	a1i 11	. . . . . . . . . . . . 13
134	133	gt0ne0d 10592	. . . . . . . . . . . 12
135	120	nnne0d 11065	. . . . . . . . . . . 12
136	121, 124, 134, 135	mulne0d 10679	. . . . . . . . . . 11
137		1red 10055	. . . . . . . . . . . . 13
138		2re 11090	. . . . . . . . . . . . . . 15
139	138	a1i 11	. . . . . . . . . . . . . 14
140		nnre 11027	. . . . . . . . . . . . . . 15
141	140, 137	readdcld 10069	. . . . . . . . . . . . . 14
142		1lt2 11194	. . . . . . . . . . . . . . 15
143	142	a1i 11	. . . . . . . . . . . . . 14
144		nnrp 11842	. . . . . . . . . . . . . . 15
145	137, 144	ltaddrp2d 11906	. . . . . . . . . . . . . 14
146	139, 141, 143, 145	mulgt1d 10960	. . . . . . . . . . . . 13
147	137, 146	gtned 10172	. . . . . . . . . . . 12
148	125, 123, 147	subne0d 10401	. . . . . . . . . . 11
149	125, 129, 136, 148	mulne0d 10679	. . . . . . . . . 10
150		2z 11409	. . . . . . . . . . 11
151	150	a1i 11	. . . . . . . . . 10
152	130, 149, 151	expne0d 13014	. . . . . . . . 9
153	128, 131, 152	divcld 10801	. . . . . . . 8
154	112, 119, 120, 153	fvmptd 6288	. . . . . . 7
155	154	oveq2d 6666	. . . . . 6
156		nnnn0 11299	. . . . . . . . . . 11
157	127, 156	nn0mulcld 11356	. . . . . . . . . 10
158	121, 157	expcld 13008	. . . . . . . . 9
159		faccl 13070	. . . . . . . . . . 11
160		nncn 11028	. . . . . . . . . . 11
161	156, 159, 160	3syl 18	. . . . . . . . . 10
162	161, 127	expcld 13008	. . . . . . . . 9
163	158, 162	mulcld 10060	. . . . . . . 8
164	75	a1i 11	. . . . . . . . . . 11
165	164, 156	nn0mulcld 11356	. . . . . . . . . 10
166		faccl 13070	. . . . . . . . . 10
167		nncn 11028	. . . . . . . . . 10
168	165, 166, 167	3syl 18	. . . . . . . . 9
169	168	sqcld 13006	. . . . . . . 8
170	165, 166	syl 17	. . . . . . . . . 10
171	170	nnne0d 11065	. . . . . . . . 9
172	168, 171, 151	expne0d 13014	. . . . . . . 8
173	163, 169, 128, 131, 172, 152	divmuldivd 10842	. . . . . . 7
174	121, 124, 127	mulexpd 13023	. . . . . . . . . 10
175	174	oveq2d 6666	. . . . . . . . 9
176	121, 127	expcld 13008	. . . . . . . . . 10
177	124, 127	expcld 13008	. . . . . . . . . 10
178	158, 162, 176, 177	mul4d 10248	. . . . . . . . 9
179	161, 124, 127	mulexpd 13023	. . . . . . . . . . 11
180	179	eqcomd 2628	. . . . . . . . . 10
181	180	oveq2d 6666	. . . . . . . . 9
182	175, 178, 181	3eqtrd 2660	. . . . . . . 8
183	121, 122	mulcld 10060	. . . . . . . . . . . . . 14
184	183, 123	addcld 10059	. . . . . . . . . . . . 13
185	125, 184	mulcomd 10061	. . . . . . . . . . . 12
186	185	oveq2d 6666	. . . . . . . . . . 11
187	121, 122, 123	adddid 10064	. . . . . . . . . . . . . . 15
188	187	oveq1d 6665	. . . . . . . . . . . . . 14
189	59, 121	syl5eqel 2705	. . . . . . . . . . . . . . 15
190	183, 189, 123	addsubassd 10412	. . . . . . . . . . . . . 14
191	59	a1i 11	. . . . . . . . . . . . . . . . 17
192	191	oveq1d 6665	. . . . . . . . . . . . . . . 16
193	192, 92	syl6eq 2672	. . . . . . . . . . . . . . 15
194	193	oveq2d 6666	. . . . . . . . . . . . . 14
195	188, 190, 194	3eqtrd 2660	. . . . . . . . . . . . 13
196	195	oveq2d 6666	. . . . . . . . . . . 12
197	196	oveq2d 6666	. . . . . . . . . . 11
198	168, 184, 125	mulassd 10063	. . . . . . . . . . 11
199	186, 197, 198	3eqtr4d 2666	. . . . . . . . . 10
200	199	oveq1d 6665	. . . . . . . . 9
201	168, 130, 164	mulexpd 13023	. . . . . . . . 9
202		df-2 11079	. . . . . . . . . . . . . . 15
203	202	a1i 11	. . . . . . . . . . . . . 14
204	203	oveq2d 6666	. . . . . . . . . . . . 13
205	183, 123, 123	addassd 10062	. . . . . . . . . . . . 13
206	204, 205	eqtr4d 2659	. . . . . . . . . . . 12
207	206	fveq2d 6195	. . . . . . . . . . 11
208	62	a1i 11	. . . . . . . . . . . . 13
209	165, 208	nn0addcld 11355	. . . . . . . . . . . 12
210		facp1 13065	. . . . . . . . . . . 12
211	209, 210	syl 17	. . . . . . . . . . 11
212		facp1 13065	. . . . . . . . . . . . 13
213	165, 212	syl 17	. . . . . . . . . . . 12
214	203	eqcomd 2628	. . . . . . . . . . . . . 14
215	214	oveq2d 6666	. . . . . . . . . . . . 13
216	214, 202, 59	3eqtr4g 2681	. . . . . . . . . . . . . . 15
217	216	oveq2d 6666	. . . . . . . . . . . . . 14
218	217, 187	eqtr4d 2659	. . . . . . . . . . . . 13
219	205, 215, 218	3eqtrd 2660	. . . . . . . . . . . 12
220	213, 219	oveq12d 6668	. . . . . . . . . . 11
221	207, 211, 220	3eqtrrd 2661	. . . . . . . . . 10
222	221	oveq1d 6665	. . . . . . . . 9
223	200, 201, 222	3eqtr3d 2664	. . . . . . . 8
224	182, 223	oveq12d 6668	. . . . . . 7
225	173, 224	eqtrd 2656	. . . . . 6
226	83	a1i 11	. . . . . . . . . . 11
227	226	oveq2d 6666	. . . . . . . . . 10
228	227	oveq2d 6666	. . . . . . . . 9
229	121, 127, 157	expaddd 13010	. . . . . . . . 9
230	81	a1i 11	. . . . . . . . . . . 12
231	230, 122, 123	adddid 10064	. . . . . . . . . . 11
232	231	eqcomd 2628	. . . . . . . . . 10
233	232	oveq2d 6666	. . . . . . . . 9
234	228, 229, 233	3eqtr3d 2664	. . . . . . . 8
235		facp1 13065	. . . . . . . . . . 11
236	156, 235	syl 17	. . . . . . . . . 10
237	236	eqcomd 2628	. . . . . . . . 9
238	237	oveq1d 6665	. . . . . . . 8
239	234, 238	oveq12d 6668	. . . . . . 7
240	218	fveq2d 6195	. . . . . . . 8
241	240	oveq1d 6665	. . . . . . 7
242	239, 241	oveq12d 6668	. . . . . 6
243	155, 225, 242	3eqtrd 2660	. . . . 5
244	243	adantr 481	. . . 4 $/\$
245	109, 111, 244	3eqtrd 2660	. . 3 $/\$
246	245	ex 450	. 2
247	11, 22, 33, 44, 104, 246	nnind 11038	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 384

wceq 1483

wcel 1990 class class class wbr 4653

cmpt 4729

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cmin 10266

cdiv 10684

cn 11020

c2 11070

c4 11072

c6 11074

cn0 11292

cz 11377 ;cdc 11493

cuz 11687

cseq 12801

cexp 12860

cfa 13060

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-rp 11833 df-seq 12802 df-exp 12861 df-fac 13061

This theorem is referenced by: wallispi2 40290

W3C validator