Theorem stirlinglem13 37767

Description: B is decreasing and has a lower bound, then it converges. Since B is log A, in another theorem it is proven that A converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Hypotheses

Ref	Expression
stirlinglem13.1	|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
stirlinglem13.2	|- B = ( n e. NN |-> ( log ` ( A ` n ) ) )

Assertion

Ref	Expression
stirlinglem13	|- E. d e. RR B ~~> d

Distinct variable group:   B, d

Allowed substitution hints:   A( n, d)   B( n)

Proof of Theorem stirlinglem13

Dummy variables j x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3084	. . . . . 6 |- y e. _V
2		stirlinglem13.2	. . . . . . 7 |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3	2	elrnmpt 5096	. . . . . 6 |- ( y e. _V -> ( y e. ran B <-> E. n e. NN y = ( log ` ( A ` n ) ) ) )
4	1, 3	ax-mp 5	. . . . 5 |- ( y e. ran B <-> E. n e. NN y = ( log ` ( A ` n ) ) )
5		simpr 462	. . . . . . 7 |- ( ( n e. NN /\ y = ( log ` ( A ` n ) ) ) -> y = ( log ` ( A ` n ) ) )
6		stirlinglem13.1	. . . . . . . . . 10 |- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
7	6	stirlinglem2 37756	. . . . . . . . 9 |- ( n e. NN -> ( A ` n ) e. RR+ )
8	7	relogcld 23558	. . . . . . . 8 |- ( n e. NN -> ( log ` ( A ` n ) ) e. RR )
9	8	adantr 466	. . . . . . 7 |- ( ( n e. NN /\ y = ( log ` ( A ` n ) ) ) -> ( log ` ( A ` n ) ) e. RR )
10	5, 9	eqeltrd 2510	. . . . . 6 |- ( ( n e. NN /\ y = ( log ` ( A ` n ) ) ) -> y e. RR )
11	10	rexlimiva 2913	. . . . 5 |- ( E. n e. NN y = ( log ` ( A ` n ) ) -> y e. RR )
12	4, 11	sylbi 198	. . . 4 |- ( y e. ran B -> y e. RR )
13	12	ssriv 3468	. . 3 |- ran B C_ RR
14		1nn 10620	. . . . . 6 |- 1 e. NN
15	6	stirlinglem2 37756	. . . . . . . 8 |- ( 1 e. NN -> ( A ` 1 ) e. RR+ )
16		relogcl 23511	. . . . . . . 8 |- ( ( A ` 1 ) e. RR+ -> ( log ` ( A ` 1 ) ) e. RR )
17	14, 15, 16	mp2b 10	. . . . . . 7 |- ( log ` ( A ` 1 ) ) e. RR
18		nfcv 2584	. . . . . . . 8 |- F/_ n 1
19		nfcv 2584	. . . . . . . . 9 |- F/_ n log
20		nfmpt1 4510	. . . . . . . . . . 11 |- F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
21	6, 20	nfcxfr 2582	. . . . . . . . . 10 |- F/_ n A
22	21, 18	nffv 5884	. . . . . . . . 9 |- F/_ n ( A ` 1 )
23	19, 22	nffv 5884	. . . . . . . 8 |- F/_ n ( log ` ( A ` 1 ) )
24		fveq2 5877	. . . . . . . . 9 |- ( n = 1 -> ( A ` n ) = ( A ` 1 ) )
25	24	fveq2d 5881	. . . . . . . 8 |- ( n = 1 -> ( log ` ( A ` n ) ) = ( log ` ( A ` 1 ) ) )
26	18, 23, 25, 2	fvmptf 5978	. . . . . . 7 |- ( ( 1 e. NN /\ ( log ` ( A ` 1 ) ) e. RR ) -> ( B ` 1 ) = ( log ` ( A ` 1 ) ) )
27	14, 17, 26	mp2an 676	. . . . . 6 |- ( B ` 1 ) = ( log ` ( A ` 1 ) )
28		fveq2 5877	. . . . . . . . 9 |- ( j = 1 -> ( A ` j ) = ( A ` 1 ) )
29	28	fveq2d 5881	. . . . . . . 8 |- ( j = 1 -> ( log ` ( A ` j ) ) = ( log ` ( A ` 1 ) ) )
30	29	eqeq2d 2436	. . . . . . 7 |- ( j = 1 -> ( ( B ` 1 ) = ( log ` ( A ` j ) ) <-> ( B ` 1 ) = ( log ` ( A ` 1 ) ) ) )
31	30	rspcev 3182	. . . . . 6 |- ( ( 1 e. NN /\ ( B ` 1 ) = ( log ` ( A ` 1 ) ) ) -> E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) ) )
32	14, 27, 31	mp2an 676	. . . . 5 |- E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) )
33	27, 17	eqeltri 2506	. . . . . 6 |- ( B ` 1 ) e. RR
34		nfcv 2584	. . . . . . . . 9 |- F/_ j ( log ` ( A ` n ) )
35		nfcv 2584	. . . . . . . . . . 11 |- F/_ n j
36	21, 35	nffv 5884	. . . . . . . . . 10 |- F/_ n ( A ` j )
37	19, 36	nffv 5884	. . . . . . . . 9 |- F/_ n ( log ` ( A ` j ) )
38		fveq2 5877	. . . . . . . . . 10 |- ( n = j -> ( A ` n ) = ( A ` j ) )
39	38	fveq2d 5881	. . . . . . . . 9 |- ( n = j -> ( log ` ( A ` n ) ) = ( log ` ( A ` j ) ) )
40	34, 37, 39	cbvmpt 4512	. . . . . . . 8 |- ( n e. NN |-> ( log ` ( A ` n ) ) ) = ( j e. NN |-> ( log ` ( A ` j ) ) )
41	2, 40	eqtri 2451	. . . . . . 7 |- B = ( j e. NN |-> ( log ` ( A ` j ) ) )
42	41	elrnmpt 5096	. . . . . 6 |- ( ( B ` 1 ) e. RR -> ( ( B ` 1 ) e. ran B <-> E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) ) ) )
43	33, 42	ax-mp 5	. . . . 5 |- ( ( B ` 1 ) e. ran B <-> E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) ) )
44	32, 43	mpbir 212	. . . 4 |- ( B ` 1 ) e. ran B
45	44	ne0ii 3768	. . 3 |- ran B =/= (/)
46		4re 10686	. . . . . . 7 |- 4 e. RR
47		4ne0 10706	. . . . . . 7 |- 4 =/= 0
48	46, 47	rereccli 10372	. . . . . 6 |- ( 1 / 4 ) e. RR
49	33, 48	resubcli 9936	. . . . 5 |- ( ( B ` 1 ) - ( 1 / 4 ) ) e. RR
50		eqid 2422	. . . . . . 7 |- ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )
51	6, 2, 50	stirlinglem12 37766	. . . . . 6 |- ( j e. NN -> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) )
52	51	rgen 2785	. . . . 5 |- A. j e. NN ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j )
53		breq1 4423	. . . . . . 7 |- ( x = ( ( B ` 1 ) - ( 1 / 4 ) ) -> ( x <_ ( B ` j ) <-> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) ) )
54	53	ralbidv 2864	. . . . . 6 |- ( x = ( ( B ` 1 ) - ( 1 / 4 ) ) -> ( A. j e. NN x <_ ( B ` j ) <-> A. j e. NN ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) ) )
55	54	rspcev 3182	. . . . 5 |- ( ( ( ( B ` 1 ) - ( 1 / 4 ) ) e. RR /\ A. j e. NN ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) ) -> E. x e. RR A. j e. NN x <_ ( B ` j ) )
56	49, 52, 55	mp2an 676	. . . 4 |- E. x e. RR A. j e. NN x <_ ( B ` j )
57		simpr 462	. . . . . . . 8 |- ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> y e. ran B )
58	8	rgen 2785	. . . . . . . . 9 |- A. n e. NN ( log ` ( A ` n ) ) e. RR
59	2	fnmpt 5718	. . . . . . . . 9 |- ( A. n e. NN ( log ` ( A ` n ) ) e. RR -> B Fn NN )
60		fvelrnb 5924	. . . . . . . . 9 |- ( B Fn NN -> ( y e. ran B <-> E. j e. NN ( B ` j ) = y ) )
61	58, 59, 60	mp2b 10	. . . . . . . 8 |- ( y e. ran B <-> E. j e. NN ( B ` j ) = y )
62	57, 61	sylib 199	. . . . . . 7 |- ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> E. j e. NN ( B ` j ) = y )
63		nfra1 2806	. . . . . . . . 9 |- F/ j A. j e. NN x <_ ( B ` j )
64		nfv 1751	. . . . . . . . 9 |- F/ j y e. ran B
65	63, 64	nfan 1984	. . . . . . . 8 |- F/ j ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B )
66		nfv 1751	. . . . . . . 8 |- F/ j x <_ y
67		simp1l 1029	. . . . . . . . . . 11 |- ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> A. j e. NN x <_ ( B ` j ) )
68		simp2 1006	. . . . . . . . . . 11 |- ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> j e. NN )
69		rsp 2791	. . . . . . . . . . 11 |- ( A. j e. NN x <_ ( B ` j ) -> ( j e. NN -> x <_ ( B ` j ) ) )
70	67, 68, 69	sylc 62	. . . . . . . . . 10 |- ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> x <_ ( B ` j ) )
71		simp3 1007	. . . . . . . . . 10 |- ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> ( B ` j ) = y )
72	70, 71	breqtrd 4445	. . . . . . . . 9 |- ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> x <_ y )
73	72	3exp 1204	. . . . . . . 8 |- ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> ( j e. NN -> ( ( B ` j ) = y -> x <_ y ) ) )
74	65, 66, 73	rexlimd 2909	. . . . . . 7 |- ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> ( E. j e. NN ( B ` j ) = y -> x <_ y ) )
75	62, 74	mpd 15	. . . . . 6 |- ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> x <_ y )
76	75	ralrimiva 2839	. . . . 5 |- ( A. j e. NN x <_ ( B ` j ) -> A. y e. ran B x <_ y )
77	76	reximi 2893	. . . 4 |- ( E. x e. RR A. j e. NN x <_ ( B ` j ) -> E. x e. RR A. y e. ran B x <_ y )
78	56, 77	ax-mp 5	. . 3 |- E. x e. RR A. y e. ran B x <_ y
79		infrecl 10590	. . 3 |- ( ( ran B C_ RR /\ ran B =/= (/) /\ E. x e. RR A. y e. ran B x <_ y ) -> inf ( ran B , RR , < ) e. RR )
80	13, 45, 78, 79	mp3an 1360	. 2 |- inf ( ran B , RR , < ) e. RR
81		nnuz 11194	. . . 4 |- NN = ( ZZ>= ` 1 )
82		1zzd 10968	. . . 4 |- ( T. -> 1 e. ZZ )
83	2, 8	fmpti 6056	. . . . 5 |- B : NN --> RR
84	83	a1i 11	. . . 4 |- ( T. -> B : NN --> RR )
85		peano2nn 10621	. . . . . . . 8 |- ( j e. NN -> ( j + 1 ) e. NN )
86	6	a1i 11	. . . . . . . . . . 11 |- ( j e. NN -> A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) )
87		simpr 462	. . . . . . . . . . . . 13 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> n = ( j + 1 ) )
88	87	fveq2d 5881	. . . . . . . . . . . 12 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ! ` n ) = ( ! ` ( j + 1 ) ) )
89	87	oveq2d 6317	. . . . . . . . . . . . . 14 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( 2 x. n ) = ( 2 x. ( j + 1 ) ) )
90	89	fveq2d 5881	. . . . . . . . . . . . 13 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( sqr ` ( 2 x. n ) ) = ( sqr ` ( 2 x. ( j + 1 ) ) ) )
91	87	oveq1d 6316	. . . . . . . . . . . . . 14 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( n / _e ) = ( ( j + 1 ) / _e ) )
92	91, 87	oveq12d 6319	. . . . . . . . . . . . 13 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ( n / _e ) ^ n ) = ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) )
93	90, 92	oveq12d 6319	. . . . . . . . . . . 12 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) )
94	88, 93	oveq12d 6319	. . . . . . . . . . 11 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` ( j + 1 ) ) / ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) )
95	85	nnnn0d 10925	. . . . . . . . . . . . 13 |- ( j e. NN -> ( j + 1 ) e. NN0 )
96		faccl 12468	. . . . . . . . . . . . 13 |- ( ( j + 1 ) e. NN0 -> ( ! ` ( j + 1 ) ) e. NN )
97		nncn 10617	. . . . . . . . . . . . 13 |- ( ( ! ` ( j + 1 ) ) e. NN -> ( ! ` ( j + 1 ) ) e. CC )
98	95, 96, 97	3syl 18	. . . . . . . . . . . 12 |- ( j e. NN -> ( ! ` ( j + 1 ) ) e. CC )
99		2cnd 10682	. . . . . . . . . . . . . . 15 |- ( j e. NN -> 2 e. CC )
100		nncn 10617	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> j e. CC )
101		1cnd 9659	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> 1 e. CC )
102	100, 101	addcld 9662	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( j + 1 ) e. CC )
103	99, 102	mulcld 9663	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( 2 x. ( j + 1 ) ) e. CC )
104	103	sqrtcld 13486	. . . . . . . . . . . . 13 |- ( j e. NN -> ( sqr ` ( 2 x. ( j + 1 ) ) ) e. CC )
105		ere 14130	. . . . . . . . . . . . . . . . 17 |- _e e. RR
106	105	recni 9655	. . . . . . . . . . . . . . . 16 |- _e e. CC
107	106	a1i 11	. . . . . . . . . . . . . . 15 |- ( j e. NN -> _e e. CC )
108		0re 9643	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
109		epos 14246	. . . . . . . . . . . . . . . . 17 |- 0 < _e
110	108, 109	gtneii 9746	. . . . . . . . . . . . . . . 16 |- _e =/= 0
111	110	a1i 11	. . . . . . . . . . . . . . 15 |- ( j e. NN -> _e =/= 0 )
112	102, 107, 111	divcld 10383	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( ( j + 1 ) / _e ) e. CC )
113	112, 95	expcld 12415	. . . . . . . . . . . . 13 |- ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) e. CC )
114	104, 113	mulcld 9663	. . . . . . . . . . . 12 |- ( j e. NN -> ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) e. CC )
115		2rp 11307	. . . . . . . . . . . . . . . . 17 |- 2 e. RR+
116	115	a1i 11	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> 2 e. RR+ )
117		nnre 10616	. . . . . . . . . . . . . . . . 17 |- ( j e. NN -> j e. RR )
118	108	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> 0 e. RR )
119		1red 9658	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> 1 e. RR )
120		0le1 10137	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 1
121	120	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> 0 <_ 1 )
122		nnge1 10635	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> 1 <_ j )
123	118, 119, 117, 121, 122	letrd 9792	. . . . . . . . . . . . . . . . 17 |- ( j e. NN -> 0 <_ j )
124	117, 123	ge0p1rpd 11368	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> ( j + 1 ) e. RR+ )
125	116, 124	rpmulcld 11357	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( 2 x. ( j + 1 ) ) e. RR+ )
126	125	sqrtgt0d 13462	. . . . . . . . . . . . . 14 |- ( j e. NN -> 0 < ( sqr ` ( 2 x. ( j + 1 ) ) ) )
127	126	gt0ne0d 10178	. . . . . . . . . . . . 13 |- ( j e. NN -> ( sqr ` ( 2 x. ( j + 1 ) ) ) =/= 0 )
128	85	nnne0d 10654	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( j + 1 ) =/= 0 )
129	102, 107, 128, 111	divne0d 10399	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( ( j + 1 ) / _e ) =/= 0 )
130		nnz 10959	. . . . . . . . . . . . . . 15 |- ( j e. NN -> j e. ZZ )
131	130	peano2zd 11043	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( j + 1 ) e. ZZ )
132	112, 129, 131	expne0d 12421	. . . . . . . . . . . . 13 |- ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) =/= 0 )
133	104, 113, 127, 132	mulne0d 10264	. . . . . . . . . . . 12 |- ( j e. NN -> ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) =/= 0 )
134	98, 114, 133	divcld 10383	. . . . . . . . . . 11 |- ( j e. NN -> ( ( ! ` ( j + 1 ) ) / ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) e. CC )
135	86, 94, 85, 134	fvmptd 5966	. . . . . . . . . 10 |- ( j e. NN -> ( A ` ( j + 1 ) ) = ( ( ! ` ( j + 1 ) ) / ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) )
136		nnrp 11311	. . . . . . . . . . . 12 |- ( ( ! ` ( j + 1 ) ) e. NN -> ( ! ` ( j + 1 ) ) e. RR+ )
137	95, 96, 136	3syl 18	. . . . . . . . . . 11 |- ( j e. NN -> ( ! ` ( j + 1 ) ) e. RR+ )
138	125	rpsqrtcld 13461	. . . . . . . . . . . 12 |- ( j e. NN -> ( sqr ` ( 2 x. ( j + 1 ) ) ) e. RR+ )
139		epr 14247	. . . . . . . . . . . . . . 15 |- _e e. RR+
140	139	a1i 11	. . . . . . . . . . . . . 14 |- ( j e. NN -> _e e. RR+ )
141	124, 140	rpdivcld 11358	. . . . . . . . . . . . 13 |- ( j e. NN -> ( ( j + 1 ) / _e ) e. RR+ )
142	141, 131	rpexpcld 12438	. . . . . . . . . . . 12 |- ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) e. RR+ )
143	138, 142	rpmulcld 11357	. . . . . . . . . . 11 |- ( j e. NN -> ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) e. RR+ )
144	137, 143	rpdivcld 11358	. . . . . . . . . 10 |- ( j e. NN -> ( ( ! ` ( j + 1 ) ) / ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) e. RR+ )
145	135, 144	eqeltrd 2510	. . . . . . . . 9 |- ( j e. NN -> ( A ` ( j + 1 ) ) e. RR+ )
146	145	relogcld 23558	. . . . . . . 8 |- ( j e. NN -> ( log ` ( A ` ( j + 1 ) ) ) e. RR )
147		nfcv 2584	. . . . . . . . 9 |- F/_ n ( j + 1 )
148	21, 147	nffv 5884	. . . . . . . . . 10 |- F/_ n ( A ` ( j + 1 ) )
149	19, 148	nffv 5884	. . . . . . . . 9 |- F/_ n ( log ` ( A ` ( j + 1 ) ) )
150		fveq2 5877	. . . . . . . . . 10 |- ( n = ( j + 1 ) -> ( A ` n ) = ( A ` ( j + 1 ) ) )
151	150	fveq2d 5881	. . . . . . . . 9 |- ( n = ( j + 1 ) -> ( log ` ( A ` n ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
152	147, 149, 151, 2	fvmptf 5978	. . . . . . . 8 |- ( ( ( j + 1 ) e. NN /\ ( log ` ( A ` ( j + 1 ) ) ) e. RR ) -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
153	85, 146, 152	syl2anc 665	. . . . . . 7 |- ( j e. NN -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
154	153, 146	eqeltrd 2510	. . . . . 6 |- ( j e. NN -> ( B ` ( j + 1 ) ) e. RR )
155	83	ffvelrni 6032	. . . . . 6 |- ( j e. NN -> ( B ` j ) e. RR )
156		eqid 2422	. . . . . . 7 |- ( z e. NN |-> ( ( 1 / ( ( 2 x. z ) + 1 ) ) x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) ^ ( 2 x. z ) ) ) ) = ( z e. NN |-> ( ( 1 / ( ( 2 x. z ) + 1 ) ) x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) ^ ( 2 x. z ) ) ) )
157	6, 2, 156	stirlinglem11 37765	. . . . . 6 |- ( j e. NN -> ( B ` ( j + 1 ) ) < ( B ` j ) )
158	154, 155, 157	ltled 9783	. . . . 5 |- ( j e. NN -> ( B ` ( j + 1 ) ) <_ ( B ` j ) )
159	158	adantl 467	. . . 4 |- ( ( T. /\ j e. NN ) -> ( B ` ( j + 1 ) ) <_ ( B ` j ) )
160	56	a1i 11	. . . 4 |- ( T. -> E. x e. RR A. j e. NN x <_ ( B ` j ) )
161	81, 82, 84, 159, 160	climinf 37503	. . 3 |- ( T. -> B ~~> inf ( ran B , RR , < ) )
162	161	trud 1446	. 2 |- B ~~> inf ( ran B , RR , < )
163		breq2 4424	. . 3 |- ( d = inf ( ran B , RR , < ) -> ( B ~~> d <-> B ~~> inf ( ran B , RR , < ) ) )
164	163	rspcev 3182	. 2 |- ( (inf ( ran B , RR , < ) e. RR /\ B ~~> inf ( ran B , RR , < ) ) -> E. d e. RR B ~~> d )
165	80, 162, 164	mp2an 676	1 |- E. d e. RR B ~~> d

Syntax hints:   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   T. wtru 1438   e. wcel 1868   =/= wne 2618   A.wral 2775   E.wrex 2776   _Vcvv 3081   C_ wss 3436   (/)c0 3761   class class class wbr 4420   |-> cmpt 4479   ran crn 4850   Fn wfn 5592   -->wf 5593   ` cfv 5597  (class class class)co 6301  infcinf 7957   CCcc 9537   RRcr 9538   0cc0 9539   1c1 9540   + caddc 9542   x. cmul 9544   < clt 9675   <_ cle 9676   - cmin 9860   / cdiv 10269   NNcn 10609   2c2 10659   4c4 10661   NN0cn0 10869   RR+crp 11302   ^cexp 12271   !cfa 12458   sqrcsqrt 13284   ~~> cli 13535   _eceu 14102   logclog 23490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617  ax-addf 9618  ax-mulf 9619

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-of 6541  df-om 6703  df-1st 6803  df-2nd 6804  df-supp 6922  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-2o 7187  df-oadd 7190  df-er 7367  df-map 7478  df-pm 7479  df-ixp 7527  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-fsupp 7886  df-fi 7927  df-sup 7958  df-inf 7959  df-oi 8027  df-card 8374  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ioc 11640  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-fl 12027  df-mod 12096  df-seq 12213  df-exp 12272  df-fac 12459  df-bc 12487  df-hash 12515  df-shft 13118  df-cj 13150  df-re 13151  df-im 13152  df-sqrt 13286  df-abs 13287  df-limsup 13513  df-clim 13539  df-rlim 13540  df-sum 13740  df-ef 14108  df-e 14109  df-sin 14110  df-cos 14111  df-tan 14112  df-pi 14113  df-dvds 14293  df-struct 15110  df-ndx 15111  df-slot 15112  df-base 15113  df-sets 15114  df-ress 15115  df-plusg 15190  df-mulr 15191  df-starv 15192  df-sca 15193  df-vsca 15194  df-ip 15195  df-tset 15196  df-ple 15197  df-ds 15199  df-unif 15200  df-hom 15201  df-cco 15202  df-rest 15308  df-topn 15309  df-0g 15327  df-gsum 15328  df-topgen 15329  df-pt 15330  df-prds 15333  df-xrs 15387  df-qtop 15393  df-imas 15394  df-xps 15397  df-mre 15479  df-mrc 15480  df-acs 15482  df-mgm 16475  df-sgrp 16514  df-mnd 16524  df-submnd 16570  df-mulg 16663  df-cntz 16958  df-cmn 17419  df-psmet 18949  df-xmet 18950  df-met 18951  df-bl 18952  df-mopn 18953  df-fbas 18954  df-fg 18955  df-cnfld 18958  df-top 19907  df-bases 19908  df-topon 19909  df-topsp 19910  df-cld 20020  df-ntr 20021  df-cls 20022  df-nei 20100  df-lp 20138  df-perf 20139  df-cn 20229  df-cnp 20230  df-haus 20317  df-cmp 20388  df-tx 20563  df-hmeo 20756  df-fil 20847  df-fm 20939  df-flim 20940  df-flf 20941  df-xms 21321  df-ms 21322  df-tms 21323  df-cncf 21896  df-limc 22807  df-dv 22808  df-ulm 23318  df-log 23492  df-cxp 23493

This theorem is referenced by:  stirlinglem14  37768