Theorem stirlinglem13 37986

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 3060	. . . . . 6 |- y e. _V
2		stirlinglem13.2	. . . . . . 7 |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3	2	elrnmpt 5100	. . . . . 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 467	. . . . . . 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 37975	. . . . . . . . 9 |- ( n e. NN -> ( A ` n ) e. RR+ )
8	7	relogcld 23621	. . . . . . . 8 |- ( n e. NN -> ( log ` ( A ` n ) ) e. RR )
9	8	adantr 471	. . . . . . 7 |- ( ( n e. NN /\ y = ( log ` ( A ` n ) ) ) -> ( log ` ( A ` n ) ) e. RR )
10	5, 9	eqeltrd 2540	. . . . . 6 |- ( ( n e. NN /\ y = ( log ` ( A ` n ) ) ) -> y e. RR )
11	10	rexlimiva 2887	. . . . 5 |- ( E. n e. NN y = ( log ` ( A ` n ) ) -> y e. RR )
12	4, 11	sylbi 200	. . . 4 |- ( y e. ran B -> y e. RR )
13	12	ssriv 3448	. . 3 |- ran B C_ RR
14		1nn 10648	. . . . . 6 |- 1 e. NN
15	6	stirlinglem2 37975	. . . . . . . 8 |- ( 1 e. NN -> ( A ` 1 ) e. RR+ )
16		relogcl 23574	. . . . . . . 8 |- ( ( A ` 1 ) e. RR+ -> ( log ` ( A ` 1 ) ) e. RR )
17	14, 15, 16	mp2b 10	. . . . . . 7 |- ( log ` ( A ` 1 ) ) e. RR
18		nfcv 2603	. . . . . . . 8 |- F/_ n 1
19		nfcv 2603	. . . . . . . . 9 |- F/_ n log
20		nfmpt1 4506	. . . . . . . . . . 11 |- F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
21	6, 20	nfcxfr 2601	. . . . . . . . . 10 |- F/_ n A
22	21, 18	nffv 5895	. . . . . . . . 9 |- F/_ n ( A ` 1 )
23	19, 22	nffv 5895	. . . . . . . 8 |- F/_ n ( log ` ( A ` 1 ) )
24		fveq2 5888	. . . . . . . . 9 |- ( n = 1 -> ( A ` n ) = ( A ` 1 ) )
25	24	fveq2d 5892	. . . . . . . 8 |- ( n = 1 -> ( log ` ( A ` n ) ) = ( log ` ( A ` 1 ) ) )
26	18, 23, 25, 2	fvmptf 5989	. . . . . . 7 |- ( ( 1 e. NN /\ ( log ` ( A ` 1 ) ) e. RR ) -> ( B ` 1 ) = ( log ` ( A ` 1 ) ) )
27	14, 17, 26	mp2an 683	. . . . . 6 |- ( B ` 1 ) = ( log ` ( A ` 1 ) )
28		fveq2 5888	. . . . . . . . 9 |- ( j = 1 -> ( A ` j ) = ( A ` 1 ) )
29	28	fveq2d 5892	. . . . . . . 8 |- ( j = 1 -> ( log ` ( A ` j ) ) = ( log ` ( A ` 1 ) ) )
30	29	eqeq2d 2472	. . . . . . 7 |- ( j = 1 -> ( ( B ` 1 ) = ( log ` ( A ` j ) ) <-> ( B ` 1 ) = ( log ` ( A ` 1 ) ) ) )
31	30	rspcev 3162	. . . . . 6 |- ( ( 1 e. NN /\ ( B ` 1 ) = ( log ` ( A ` 1 ) ) ) -> E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) ) )
32	14, 27, 31	mp2an 683	. . . . 5 |- E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) )
33	27, 17	eqeltri 2536	. . . . . 6 |- ( B ` 1 ) e. RR
34		nfcv 2603	. . . . . . . . 9 |- F/_ j ( log ` ( A ` n ) )
35		nfcv 2603	. . . . . . . . . . 11 |- F/_ n j
36	21, 35	nffv 5895	. . . . . . . . . 10 |- F/_ n ( A ` j )
37	19, 36	nffv 5895	. . . . . . . . 9 |- F/_ n ( log ` ( A ` j ) )
38		fveq2 5888	. . . . . . . . . 10 |- ( n = j -> ( A ` n ) = ( A ` j ) )
39	38	fveq2d 5892	. . . . . . . . 9 |- ( n = j -> ( log ` ( A ` n ) ) = ( log ` ( A ` j ) ) )
40	34, 37, 39	cbvmpt 4508	. . . . . . . 8 |- ( n e. NN |-> ( log ` ( A ` n ) ) ) = ( j e. NN |-> ( log ` ( A ` j ) ) )
41	2, 40	eqtri 2484	. . . . . . 7 |- B = ( j e. NN |-> ( log ` ( A ` j ) ) )
42	41	elrnmpt 5100	. . . . . 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 214	. . . 4 |- ( B ` 1 ) e. ran B
45	44	ne0ii 3750	. . 3 |- ran B =/= (/)
46		4re 10714	. . . . . . 7 |- 4 e. RR
47		4ne0 10734	. . . . . . 7 |- 4 =/= 0
48	46, 47	rereccli 10400	. . . . . 6 |- ( 1 / 4 ) e. RR
49	33, 48	resubcli 9962	. . . . 5 |- ( ( B ` 1 ) - ( 1 / 4 ) ) e. RR
50		eqid 2462	. . . . . . 7 |- ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )
51	6, 2, 50	stirlinglem12 37985	. . . . . 6 |- ( j e. NN -> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) )
52	51	rgen 2759	. . . . 5 |- A. j e. NN ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j )
53		breq1 4419	. . . . . . 7 |- ( x = ( ( B ` 1 ) - ( 1 / 4 ) ) -> ( x <_ ( B ` j ) <-> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) ) )
54	53	ralbidv 2839	. . . . . 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 3162	. . . . 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 683	. . . 4 |- E. x e. RR A. j e. NN x <_ ( B ` j )
57		simpr 467	. . . . . . . 8 |- ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> y e. ran B )
58	8	rgen 2759	. . . . . . . . 9 |- A. n e. NN ( log ` ( A ` n ) ) e. RR
59	2	fnmpt 5726	. . . . . . . . 9 |- ( A. n e. NN ( log ` ( A ` n ) ) e. RR -> B Fn NN )
60		fvelrnb 5935	. . . . . . . . 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 201	. . . . . . 7 |- ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> E. j e. NN ( B ` j ) = y )
63		nfra1 2781	. . . . . . . . 9 |- F/ j A. j e. NN x <_ ( B ` j )
64		nfv 1772	. . . . . . . . 9 |- F/ j y e. ran B
65	63, 64	nfan 2022	. . . . . . . 8 |- F/ j ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B )
66		nfv 1772	. . . . . . . 8 |- F/ j x <_ y
67		simp1l 1038	. . . . . . . . . . 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 1015	. . . . . . . . . . 11 |- ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> j e. NN )
69		rsp 2766	. . . . . . . . . . 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 1016	. . . . . . . . . 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 4441	. . . . . . . . 9 |- ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> x <_ y )
73	72	3exp 1214	. . . . . . . 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 2883	. . . . . . 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 2814	. . . . 5 |- ( A. j e. NN x <_ ( B ` j ) -> A. y e. ran B x <_ y )
77	76	reximi 2867	. . . 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 10618	. . 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 1373	. 2 |- inf ( ran B , RR , < ) e. RR
81		nnuz 11223	. . . 4 |- NN = ( ZZ>= ` 1 )
82		1zzd 10997	. . . 4 |- ( T. -> 1 e. ZZ )
83	2, 8	fmpti 6068	. . . . 5 |- B : NN --> RR
84	83	a1i 11	. . . 4 |- ( T. -> B : NN --> RR )
85		peano2nn 10649	. . . . . . . 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 467	. . . . . . . . . . . . 13 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> n = ( j + 1 ) )
88	87	fveq2d 5892	. . . . . . . . . . . 12 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ! ` n ) = ( ! ` ( j + 1 ) ) )
89	87	oveq2d 6331	. . . . . . . . . . . . . 14 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( 2 x. n ) = ( 2 x. ( j + 1 ) ) )
90	89	fveq2d 5892	. . . . . . . . . . . . 13 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( sqr ` ( 2 x. n ) ) = ( sqr ` ( 2 x. ( j + 1 ) ) ) )
91	87	oveq1d 6330	. . . . . . . . . . . . . 14 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( n / _e ) = ( ( j + 1 ) / _e ) )
92	91, 87	oveq12d 6333	. . . . . . . . . . . . 13 |- ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ( n / _e ) ^ n ) = ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) )
93	90, 92	oveq12d 6333	. . . . . . . . . . . 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 6333	. . . . . . . . . . 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 10954	. . . . . . . . . . . . 13 |- ( j e. NN -> ( j + 1 ) e. NN0 )
96		faccl 12501	. . . . . . . . . . . . 13 |- ( ( j + 1 ) e. NN0 -> ( ! ` ( j + 1 ) ) e. NN )
97		nncn 10645	. . . . . . . . . . . . 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 10710	. . . . . . . . . . . . . . 15 |- ( j e. NN -> 2 e. CC )
100		nncn 10645	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> j e. CC )
101		1cnd 9685	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> 1 e. CC )
102	100, 101	addcld 9688	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( j + 1 ) e. CC )
103	99, 102	mulcld 9689	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( 2 x. ( j + 1 ) ) e. CC )
104	103	sqrtcld 13548	. . . . . . . . . . . . 13 |- ( j e. NN -> ( sqr ` ( 2 x. ( j + 1 ) ) ) e. CC )
105		ere 14192	. . . . . . . . . . . . . . . . 17 |- _e e. RR
106	105	recni 9681	. . . . . . . . . . . . . . . 16 |- _e e. CC
107	106	a1i 11	. . . . . . . . . . . . . . 15 |- ( j e. NN -> _e e. CC )
108		0re 9669	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
109		epos 14308	. . . . . . . . . . . . . . . . 17 |- 0 < _e
110	108, 109	gtneii 9772	. . . . . . . . . . . . . . . 16 |- _e =/= 0
111	110	a1i 11	. . . . . . . . . . . . . . 15 |- ( j e. NN -> _e =/= 0 )
112	102, 107, 111	divcld 10411	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( ( j + 1 ) / _e ) e. CC )
113	112, 95	expcld 12448	. . . . . . . . . . . . 13 |- ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) e. CC )
114	104, 113	mulcld 9689	. . . . . . . . . . . 12 |- ( j e. NN -> ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) e. CC )
115		2rp 11336	. . . . . . . . . . . . . . . . 17 |- 2 e. RR+
116	115	a1i 11	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> 2 e. RR+ )
117		nnre 10644	. . . . . . . . . . . . . . . . 17 |- ( j e. NN -> j e. RR )
118	108	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> 0 e. RR )
119		1red 9684	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> 1 e. RR )
120		0le1 10165	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 1
121	120	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> 0 <_ 1 )
122		nnge1 10663	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> 1 <_ j )
123	118, 119, 117, 121, 122	letrd 9818	. . . . . . . . . . . . . . . . 17 |- ( j e. NN -> 0 <_ j )
124	117, 123	ge0p1rpd 11397	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> ( j + 1 ) e. RR+ )
125	116, 124	rpmulcld 11386	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( 2 x. ( j + 1 ) ) e. RR+ )
126	125	sqrtgt0d 13523	. . . . . . . . . . . . . 14 |- ( j e. NN -> 0 < ( sqr ` ( 2 x. ( j + 1 ) ) ) )
127	126	gt0ne0d 10206	. . . . . . . . . . . . 13 |- ( j e. NN -> ( sqr ` ( 2 x. ( j + 1 ) ) ) =/= 0 )
128	85	nnne0d 10682	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( j + 1 ) =/= 0 )
129	102, 107, 128, 111	divne0d 10427	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( ( j + 1 ) / _e ) =/= 0 )
130		nnz 10988	. . . . . . . . . . . . . . 15 |- ( j e. NN -> j e. ZZ )
131	130	peano2zd 11072	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( j + 1 ) e. ZZ )
132	112, 129, 131	expne0d 12454	. . . . . . . . . . . . 13 |- ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) =/= 0 )
133	104, 113, 127, 132	mulne0d 10292	. . . . . . . . . . . 12 |- ( j e. NN -> ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) =/= 0 )
134	98, 114, 133	divcld 10411	. . . . . . . . . . 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 5977	. . . . . . . . . 10 |- ( j e. NN -> ( A ` ( j + 1 ) ) = ( ( ! ` ( j + 1 ) ) / ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) )
136		nnrp 11340	. . . . . . . . . . . 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 13522	. . . . . . . . . . . 12 |- ( j e. NN -> ( sqr ` ( 2 x. ( j + 1 ) ) ) e. RR+ )
139		epr 14309	. . . . . . . . . . . . . . 15 |- _e e. RR+
140	139	a1i 11	. . . . . . . . . . . . . 14 |- ( j e. NN -> _e e. RR+ )
141	124, 140	rpdivcld 11387	. . . . . . . . . . . . 13 |- ( j e. NN -> ( ( j + 1 ) / _e ) e. RR+ )
142	141, 131	rpexpcld 12471	. . . . . . . . . . . 12 |- ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) e. RR+ )
143	138, 142	rpmulcld 11386	. . . . . . . . . . 11 |- ( j e. NN -> ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) e. RR+ )
144	137, 143	rpdivcld 11387	. . . . . . . . . 10 |- ( j e. NN -> ( ( ! ` ( j + 1 ) ) / ( ( sqr ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) e. RR+ )
145	135, 144	eqeltrd 2540	. . . . . . . . 9 |- ( j e. NN -> ( A ` ( j + 1 ) ) e. RR+ )
146	145	relogcld 23621	. . . . . . . 8 |- ( j e. NN -> ( log ` ( A ` ( j + 1 ) ) ) e. RR )
147		nfcv 2603	. . . . . . . . 9 |- F/_ n ( j + 1 )
148	21, 147	nffv 5895	. . . . . . . . . 10 |- F/_ n ( A ` ( j + 1 ) )
149	19, 148	nffv 5895	. . . . . . . . 9 |- F/_ n ( log ` ( A ` ( j + 1 ) ) )
150		fveq2 5888	. . . . . . . . . 10 |- ( n = ( j + 1 ) -> ( A ` n ) = ( A ` ( j + 1 ) ) )
151	150	fveq2d 5892	. . . . . . . . 9 |- ( n = ( j + 1 ) -> ( log ` ( A ` n ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
152	147, 149, 151, 2	fvmptf 5989	. . . . . . . 8 |- ( ( ( j + 1 ) e. NN /\ ( log ` ( A ` ( j + 1 ) ) ) e. RR ) -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
153	85, 146, 152	syl2anc 671	. . . . . . 7 |- ( j e. NN -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
154	153, 146	eqeltrd 2540	. . . . . 6 |- ( j e. NN -> ( B ` ( j + 1 ) ) e. RR )
155	83	ffvelrni 6044	. . . . . 6 |- ( j e. NN -> ( B ` j ) e. RR )
156		eqid 2462	. . . . . . 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 37984	. . . . . 6 |- ( j e. NN -> ( B ` ( j + 1 ) ) < ( B ` j ) )
158	154, 155, 157	ltled 9809	. . . . 5 |- ( j e. NN -> ( B ` ( j + 1 ) ) <_ ( B ` j ) )
159	158	adantl 472	. . . 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 37722	. . 3 |- ( T. -> B ~~> inf ( ran B , RR , < ) )
162	161	trud 1464	. 2 |- B ~~> inf ( ran B , RR , < )
163		breq2 4420	. . 3 |- ( d = inf ( ran B , RR , < ) -> ( B ~~> d <-> B ~~> inf ( ran B , RR , < ) ) )
164	163	rspcev 3162	. 2 |- ( (inf ( ran B , RR , < ) e. RR /\ B ~~> inf ( ran B , RR , < ) ) -> E. d e. RR B ~~> d )
165	80, 162, 164	mp2an 683	1 |- E. d e. RR B ~~> d

Syntax hints:   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   T. wtru 1456   e. wcel 1898   =/= wne 2633   A.wral 2749   E.wrex 2750   _Vcvv 3057   C_ wss 3416   (/)c0 3743   class class class wbr 4416   |-> cmpt 4475   ran crn 4854   Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315  infcinf 7981   CCcc 9563   RRcr 9564   0cc0 9565   1c1 9566   + caddc 9568   x. cmul 9570   < clt 9701   <_ cle 9702   - cmin 9886   / cdiv 10297   NNcn 10637   2c2 10687   4c4 10689   NN0cn0 10898   RR+crp 11331   ^cexp 12304   !cfa 12491   sqrcsqrt 13345   ~~> cli 13597   _eceu 14164   logclog 23553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643  ax-addf 9644  ax-mulf 9645

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-of 6558  df-om 6720  df-1st 6820  df-2nd 6821  df-supp 6942  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-map 7500  df-pm 7501  df-ixp 7549  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-fsupp 7910  df-fi 7951  df-sup 7982  df-inf 7983  df-oi 8051  df-card 8399  df-cda 8624  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-q 11294  df-rp 11332  df-xneg 11438  df-xadd 11439  df-xmul 11440  df-ioo 11668  df-ioc 11669  df-ico 11670  df-icc 11671  df-fz 11814  df-fzo 11947  df-fl 12060  df-mod 12129  df-seq 12246  df-exp 12305  df-fac 12492  df-bc 12520  df-hash 12548  df-shft 13179  df-cj 13211  df-re 13212  df-im 13213  df-sqrt 13347  df-abs 13348  df-limsup 13575  df-clim 13601  df-rlim 13602  df-sum 13802  df-ef 14170  df-e 14171  df-sin 14172  df-cos 14173  df-tan 14174  df-pi 14175  df-dvds 14355  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-ress 15177  df-plusg 15252  df-mulr 15253  df-starv 15254  df-sca 15255  df-vsca 15256  df-ip 15257  df-tset 15258  df-ple 15259  df-ds 15261  df-unif 15262  df-hom 15263  df-cco 15264  df-rest 15370  df-topn 15371  df-0g 15389  df-gsum 15390  df-topgen 15391  df-pt 15392  df-prds 15395  df-xrs 15449  df-qtop 15455  df-imas 15456  df-xps 15459  df-mre 15541  df-mrc 15542  df-acs 15544  df-mgm 16537  df-sgrp 16576  df-mnd 16586  df-submnd 16632  df-mulg 16725  df-cntz 17020  df-cmn 17481  df-psmet 19011  df-xmet 19012  df-met 19013  df-bl 19014  df-mopn 19015  df-fbas 19016  df-fg 19017  df-cnfld 19020  df-top 19970  df-bases 19971  df-topon 19972  df-topsp 19973  df-cld 20083  df-ntr 20084  df-cls 20085  df-nei 20163  df-lp 20201  df-perf 20202  df-cn 20292  df-cnp 20293  df-haus 20380  df-cmp 20451  df-tx 20626  df-hmeo 20819  df-fil 20910  df-fm 21002  df-flim 21003  df-flf 21004  df-xms 21384  df-ms 21385  df-tms 21386  df-cncf 21959  df-limc 22870  df-dv 22871  df-ulm 23381  df-log 23555  df-cxp 23556

This theorem is referenced by:  stirlinglem14  37987