stirlinglem13 - Mathbox for Glauco Siliprandi

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

Theorem stirlinglem13 27835

Description:

is decreasing and has a lower bound, then it converges. Since

, in another theorem it is proven that

converges also. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

**Hypotheses**
Ref	Expression
stirlinglem13.1
stirlinglem13.2

**Assertion**
Ref	Expression
stirlinglem13

Distinct variable group:

Allowed substitution hints:

(

)

(

)

Proof of Theorem stirlinglem13 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2791	. . . . . . . . . 10
2		stirlinglem13.2	. . . . . . . . . . 11
3	2	elrnmpt 4926	. . . . . . . . . 10
4	1, 3	ax-mp 8	. . . . . . . . 9
5	4	biimpi 186	. . . . . . . 8
6		nfv 1605	. . . . . . . . 9
7		simpr 447	. . . . . . . . . . 11 $/\$
8		stirlinglem13.1	. . . . . . . . . . . . . 14
9	8	stirlinglem2 27824	. . . . . . . . . . . . 13
10	9	relogcld 19974	. . . . . . . . . . . 12
11	10	adantr 451	. . . . . . . . . . 11 $/\$
12	7, 11	eqeltrd 2357	. . . . . . . . . 10 $/\$
13	12	ex 423	. . . . . . . . 9
14	6, 13	rexlimi 2660	. . . . . . . 8
15	5, 14	syl 15	. . . . . . 7
16	15	rgen 2608	. . . . . 6
17		dfss3 3170	. . . . . 6
18	16, 17	mpbir 200	. . . . 5
19		1nn 9757	. . . . . . . . 9
20	8	stirlinglem2 27824	. . . . . . . . . . . . 13
21	19, 20	ax-mp 8	. . . . . . . . . . . 12
22		relogcl 19932	. . . . . . . . . . . 12
23	21, 22	ax-mp 8	. . . . . . . . . . 11
24	19, 23	pm3.2i 441	. . . . . . . . . 10 $/\$
25		nfcv 2419	. . . . . . . . . . 11
26		nfcv 2419	. . . . . . . . . . . 12
27		nfmpt1 4109	. . . . . . . . . . . . . 14
28	8, 27	nfcxfr 2416	. . . . . . . . . . . . 13
29	28, 25	nffv 5532	. . . . . . . . . . . 12
30	26, 29	nffv 5532	. . . . . . . . . . 11
31		fveq2 5525	. . . . . . . . . . . 12
32	31	fveq2d 5529	. . . . . . . . . . 11
33	25, 30, 32, 2	fvmptf 5616	. . . . . . . . . 10 $/\$
34	24, 33	ax-mp 8	. . . . . . . . 9
35	19, 34	pm3.2i 441	. . . . . . . 8 $/\$
36		fveq2 5525	. . . . . . . . . . 11
37	36	fveq2d 5529	. . . . . . . . . 10
38	37	eqeq2d 2294	. . . . . . . . 9
39	38	rspcev 2884	. . . . . . . 8 $/\$
40	35, 39	ax-mp 8	. . . . . . 7
41	24	simpri 448	. . . . . . . . 9
42	34, 41	eqeltri 2353	. . . . . . . 8
43		nfcv 2419	. . . . . . . . . . 11
44		nfcv 2419	. . . . . . . . . . . . 13
45	28, 44	nffv 5532	. . . . . . . . . . . 12
46	26, 45	nffv 5532	. . . . . . . . . . 11
47		fveq2 5525	. . . . . . . . . . . 12
48	47	fveq2d 5529	. . . . . . . . . . 11
49	43, 46, 48	cbvmpt 4110	. . . . . . . . . 10
50	2, 49	eqtri 2303	. . . . . . . . 9
51	50	elrnmpt 4926	. . . . . . . 8
52	42, 51	ax-mp 8	. . . . . . 7
53	40, 52	mpbir 200	. . . . . 6
54		ne0i 3461	. . . . . 6
55	53, 54	ax-mp 8	. . . . 5
56		4re 9819	. . . . . . . . . . 11
57		0re 8838	. . . . . . . . . . . 12
58		4pos 9832	. . . . . . . . . . . 12
59	57, 58	gtneii 8930	. . . . . . . . . . 11
60	56, 59	rereccli 9525	. . . . . . . . . 10
61	42, 60	resubcli 9109	. . . . . . . . 9
62		eqid 2283	. . . . . . . . . . 11
63	8, 2, 62	stirlinglem12 27834	. . . . . . . . . 10
64	63	rgen 2608	. . . . . . . . 9
65	61, 64	pm3.2i 441	. . . . . . . 8 $/\$
66		breq1 4026	. . . . . . . . . 10
67	66	ralbidv 2563	. . . . . . . . 9
68	67	rspcev 2884	. . . . . . . 8 $/\$
69	65, 68	ax-mp 8	. . . . . . 7
70	69	idi 2	. . . . . 6
71		nfv 1605	. . . . . . . 8
72		simpr 447	. . . . . . . . . . 11 $/\$
73	10	rgen 2608	. . . . . . . . . . . . 13
74	2	fnmpt 5370	. . . . . . . . . . . . 13
75	73, 74	ax-mp 8	. . . . . . . . . . . 12
76		fvelrnb 5570	. . . . . . . . . . . 12
77	75, 76	ax-mp 8	. . . . . . . . . . 11
78	72, 77	sylib 188	. . . . . . . . . 10 $/\$
79		nfra1 2593	. . . . . . . . . . . 12
80		nfv 1605	. . . . . . . . . . . 12
81	79, 80	nfan 1771	. . . . . . . . . . 11 $/\$
82		nfv 1605	. . . . . . . . . . 11
83		simp1l 979	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
84		simp2 956	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
85	83, 84	jca 518	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
86		rsp 2603	. . . . . . . . . . . . . . 15
87	86	imp 418	. . . . . . . . . . . . . 14 $/\$
88	85, 87	syl 15	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
89		simp3 957	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
90	88, 89	breqtrd 4047	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
91	90	3exp 1150	. . . . . . . . . . 11 $/\$
92	81, 82, 91	rexlimd 2664	. . . . . . . . . 10 $/\$
93	78, 92	mpd 14	. . . . . . . . 9 $/\$
94	93	ex 423	. . . . . . . 8
95	71, 94	ralrimi 2624	. . . . . . 7
96	95	reximi 2650	. . . . . 6
97	70, 96	ax-mp 8	. . . . 5
98	18, 55, 97	3pm3.2i 1130	. . . 4 $/\$ $/\$
99		infmrcl 9733	. . . 4 $/\$ $/\$
100	98, 99	ax-mp 8	. . 3
101		nftru 1541	. . . . 5
102		nfcv 2419	. . . . . 6
103	2, 102	nfcxfr 2416	. . . . 5
104		nnuz 10263	. . . . 5
105		1z 10053	. . . . . 6
106	105	a1i 10	. . . . 5
107	2	fmpt 5681	. . . . . . 7
108	73, 107	mpbi 199	. . . . . 6
109	108	a1i 10	. . . . 5
110		peano2nn 9758	. . . . . . . . . 10
111	8	a1i 10	. . . . . . . . . . . . 13
112		simpr 447	. . . . . . . . . . . . . . 15 $/\$
113	112	fveq2d 5529	. . . . . . . . . . . . . 14 $/\$
114	112	oveq2d 5874	. . . . . . . . . . . . . . . 16 $/\$
115	114	fveq2d 5529	. . . . . . . . . . . . . . 15 $/\$
116	112	oveq1d 5873	. . . . . . . . . . . . . . . 16 $/\$
117	116, 112	oveq12d 5876	. . . . . . . . . . . . . . 15 $/\$
118	115, 117	oveq12d 5876	. . . . . . . . . . . . . 14 $/\$
119	113, 118	oveq12d 5876	. . . . . . . . . . . . 13 $/\$
120	110	nnnn0d 10018	. . . . . . . . . . . . . . 15
121		faccl 11298	. . . . . . . . . . . . . . 15
122		nncn 9754	. . . . . . . . . . . . . . 15
123	120, 121, 122	3syl 18	. . . . . . . . . . . . . 14
124		2cn 9816	. . . . . . . . . . . . . . . . . 18
125	124	a1i 10	. . . . . . . . . . . . . . . . 17
126		nncn 9754	. . . . . . . . . . . . . . . . . 18
127		ax-1cn 8795	. . . . . . . . . . . . . . . . . . 19
128	127	a1i 10	. . . . . . . . . . . . . . . . . 18
129	126, 128	addcld 8854	. . . . . . . . . . . . . . . . 17
130	125, 129	mulcld 8855	. . . . . . . . . . . . . . . 16
131	130	sqrcld 11919	. . . . . . . . . . . . . . 15
132		ere 12370	. . . . . . . . . . . . . . . . . . 19
133	132	recni 8849	. . . . . . . . . . . . . . . . . 18
134	133	a1i 10	. . . . . . . . . . . . . . . . 17
135		epos 12485	. . . . . . . . . . . . . . . . . . 19
136	57, 132	ltnei 8943	. . . . . . . . . . . . . . . . . . 19
137	135, 136	ax-mp 8	. . . . . . . . . . . . . . . . . 18
138	137	a1i 10	. . . . . . . . . . . . . . . . 17
139	129, 134, 138	divcld 9536	. . . . . . . . . . . . . . . 16
140	139, 120	expcld 11245	. . . . . . . . . . . . . . 15
141	131, 140	mulcld 8855	. . . . . . . . . . . . . 14
142	57	a1i 10	. . . . . . . . . . . . . . . 16
143		2rp 10359	. . . . . . . . . . . . . . . . . . 19
144	143	a1i 10	. . . . . . . . . . . . . . . . . 18
145		nnre 9753	. . . . . . . . . . . . . . . . . . 19
146		1re 8837	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 10	. . . . . . . . . . . . . . . . . . . 20
148		0le1 9297	. . . . . . . . . . . . . . . . . . . . 21
149	148	a1i 10	. . . . . . . . . . . . . . . . . . . 20
150		nnge1 9772	. . . . . . . . . . . . . . . . . . . 20
151	142, 147, 145, 149, 150	letrd 8973	. . . . . . . . . . . . . . . . . . 19
152	145, 151	ge0p1rpd 10416	. . . . . . . . . . . . . . . . . 18
153	144, 152	rpmulcld 10406	. . . . . . . . . . . . . . . . 17
154	153	sqrgt0d 11895	. . . . . . . . . . . . . . . 16
155	142, 154	gtned 8954	. . . . . . . . . . . . . . 15
156	110	nnne0d 9790	. . . . . . . . . . . . . . . . 17
157	129, 134, 156, 138	divne0d 9552	. . . . . . . . . . . . . . . 16
158		nnz 10045	. . . . . . . . . . . . . . . . 17
159	158	peano2zd 10120	. . . . . . . . . . . . . . . 16
160	139, 157, 159	expne0d 11251	. . . . . . . . . . . . . . 15
161	131, 140, 155, 160	mulne0d 9420	. . . . . . . . . . . . . 14
162	123, 141, 161	divcld 9536	. . . . . . . . . . . . 13
163	111, 119, 110, 162	fvmptd 5606	. . . . . . . . . . . 12
164		nnrp 10363	. . . . . . . . . . . . . 14
165	120, 121, 164	3syl 18	. . . . . . . . . . . . 13
166	153	rpsqrcld 11894	. . . . . . . . . . . . . 14
167		epr 12486	. . . . . . . . . . . . . . . . 17
168	167	a1i 10	. . . . . . . . . . . . . . . 16
169	152, 168	rpdivcld 10407	. . . . . . . . . . . . . . 15
170	169, 159	rpexpcld 11268	. . . . . . . . . . . . . 14
171	166, 170	rpmulcld 10406	. . . . . . . . . . . . 13
172	165, 171	rpdivcld 10407	. . . . . . . . . . . 12
173	163, 172	eqeltrd 2357	. . . . . . . . . . 11
174	173	relogcld 19974	. . . . . . . . . 10
175	110, 174	jca 518	. . . . . . . . 9 $/\$
176		nfcv 2419	. . . . . . . . . 10
177	28, 176	nffv 5532	. . . . . . . . . . 11
178	26, 177	nffv 5532	. . . . . . . . . 10
179		fveq2 5525	. . . . . . . . . . 11
180	179	fveq2d 5529	. . . . . . . . . 10
181	176, 178, 180, 2	fvmptf 5616	. . . . . . . . 9 $/\$
182	175, 181	syl 15	. . . . . . . 8
183	182, 174	eqeltrd 2357	. . . . . . 7
184	108	ffvelrni 5664	. . . . . . 7
185		eqid 2283	. . . . . . . 8
186	8, 2, 185	stirlinglem11 27833	. . . . . . 7
187	183, 184, 186	ltled 8967	. . . . . 6
188	187	adantl 452	. . . . 5 $/\$
189	69	a1i 10	. . . . 5
190	101, 103, 104, 106, 109, 188, 189	climinff 27737	. . . 4
191	190	trud 1314	. . 3
192	100, 191	pm3.2i 441	. 2 $/\$
193		breq2 4027	. . 3
194	193	rspcev 2884	. 2 $/\$
195	192, 194	ax-mp 8	1

Colors of variables: wff set class

Syntax hints:

wb 176 $/\$ wa 358 $/\$ w3a 934

wtru 1307

wceq 1623

wcel 1684

wne 2446

wral 2543

wrex 2544

cvv 2788

wss 3152

c0 3455 class class class wbr 4023

cmpt 4077

ccnv 4688

crn 4690

wfn 5250

wf 5251

cfv 5255 (class class class)co 5858

csup 7193

cc 8735

cr 8736

cc0 8737

c1 8738

caddc 8740

cmul 8742

clt 8867

cle 8868

cmin 9037

cdiv 9423

cn 9746

c2 9795

c4 9797

cn0 9965

cz 10024

crp 10354

cexp 11104

cfa 11288

csqr 11718

cli 11958

ceu 12344

clog 19912

This theorem is referenced by: stirlinglem14 27836

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1533 ax-5 1544 ax-17 1603 ax-9 1635 ax-8 1643 ax-13 1686 ax-14 1688 ax-6 1703 ax-7 1708 ax-11 1715 ax-12 1866 ax-ext 2264 ax-rep 4131 ax-sep 4141 ax-nul 4149 ax-pow 4188 ax-pr 4214 ax-un 4512 ax-inf2 7342 ax-cnex 8793 ax-resscn 8794 ax-1cn 8795 ax-icn 8796 ax-addcl 8797 ax-addrcl 8798 ax-mulcl 8799 ax-mulrcl 8800 ax-mulcom 8801 ax-addass 8802 ax-mulass 8803 ax-distr 8804 ax-i2m1 8805 ax-1ne0 8806 ax-1rid 8807 ax-rnegex 8808 ax-rrecex 8809 ax-cnre 8810 ax-pre-lttri 8811 ax-pre-lttrn 8812 ax-pre-ltadd 8813 ax-pre-mulgt0 8814 ax-pre-sup 8815 ax-addf 8816 ax-mulf 8817

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-tru 1310 df-ex 1529 df-nf 1532 df-sb 1630 df-eu 2147 df-mo 2148 df-clab 2270 df-cleq 2276 df-clel 2279 df-nfc 2408 df-ne 2448 df-nel 2449 df-ral 2548 df-rex 2549 df-reu 2550 df-rmo 2551 df-rab 2552 df-v 2790 df-sbc 2992 df-csb 3082 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-pss 3168 df-nul 3456 df-if 3566 df-pw 3627 df-sn 3646 df-pr 3647 df-tp 3648 df-op 3649 df-uni 3828 df-int 3863 df-iun 3907 df-iin 3908 df-br 4024 df-opab 4078 df-mpt 4079 df-tr 4114 df-eprel 4305 df-id 4309 df-po 4314 df-so 4315 df-fr 4352 df-se 4353 df-we 4354 df-ord 4395 df-on 4396 df-lim 4397 df-suc 4398 df-om 4657 df-xp 4695 df-rel 4696 df-cnv 4697 df-co 4698 df-dm 4699 df-rn 4700 df-res 4701 df-ima 4702 df-iota 5219 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-isom 5264 df-ov 5861 df-oprab 5862 df-mpt2 5863 df-of 6078 df-1st 6122 df-2nd 6123 df-riota 6304 df-recs 6388 df-rdg 6423 df-1o 6479 df-2o 6480 df-oadd 6483 df-er 6660 df-map 6774 df-pm 6775 df-ixp 6818 df-en 6864 df-dom 6865 df-sdom 6866 df-fin 6867 df-fi 7165 df-sup 7194 df-oi 7225 df-card 7572 df-cda 7794 df-pnf 8869 df-mnf 8870 df-xr 8871 df-ltxr 8872 df-le 8873 df-sub 9039 df-neg 9040 df-div 9424 df-nn 9747 df-2 9804 df-3 9805 df-4 9806 df-5 9807 df-6 9808 df-7 9809 df-8 9810 df-9 9811 df-10 9812 df-n0 9966 df-z 10025 df-dec 10125 df-uz 10231 df-q 10317 df-rp 10355 df-xneg 10452 df-xadd 10453 df-xmul 10454 df-ioo 10660 df-ioc 10661 df-ico 10662 df-icc 10663 df-fz 10783 df-fzo 10871 df-fl 10925 df-mod 10974 df-seq 11047 df-exp 11105 df-fac 11289 df-bc 11316 df-hash 11338 df-shft 11562 df-cj 11584 df-re 11585 df-im 11586 df-sqr 11720 df-abs 11721 df-limsup 11945 df-clim 11962 df-rlim 11963 df-sum 12159 df-ef 12349 df-e 12350 df-sin 12351 df-cos 12352 df-tan 12353 df-pi 12354 df-dvds 12532 df-struct 13150 df-ndx 13151 df-slot 13152 df-base 13153 df-sets 13154 df-ress 13155 df-plusg 13221 df-mulr 13222 df-starv 13223 df-sca 13224 df-vsca 13225 df-tset 13227 df-ple 13228 df-ds 13230 df-hom 13232 df-cco 13233 df-rest 13327 df-topn 13328 df-topgen 13344 df-pt 13345 df-prds 13348 df-xrs 13403 df-0g 13404 df-gsum 13405 df-qtop 13410 df-imas 13411 df-xps 13413 df-mre 13488 df-mrc 13489 df-acs 13491 df-mnd 14367 df-submnd 14416 df-mulg 14492 df-cntz 14793 df-cmn 15091 df-xmet 16373 df-met 16374 df-bl 16375 df-mopn 16376 df-cnfld 16378 df-top 16636 df-bases 16638 df-topon 16639 df-topsp 16640 df-cld 16756 df-ntr 16757 df-cls 16758 df-nei 16835 df-lp 16868 df-perf 16869 df-cn 16957 df-cnp 16958 df-haus 17043 df-cmp 17114 df-tx 17257 df-hmeo 17446 df-fbas 17520 df-fg 17521 df-fil 17541 df-fm 17633 df-flim 17634 df-flf 17635 df-xms 17885 df-ms 17886 df-tms 17887 df-cncf 18382 df-limc 19216 df-dv 19217 df-ulm 19756 df-log 19914 df-cxp 19915

W3C validator