Theorem stirlinglem12 30023

Description: The sequence B is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Hypotheses

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

Assertion

Ref	Expression
stirlinglem12	|- ( N e. NN -> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` N ) )

Distinct variable group:   n, N

Allowed substitution hints:   A( n)   B( n)   F( n)

Proof of Theorem stirlinglem12

Dummy variables i j k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1nn 10439	. . . . 5 |- 1 e. NN
2		stirlinglem12.1	. . . . . . 7 |- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
3	2	stirlinglem2 30013	. . . . . 6 |- ( 1 e. NN -> ( A ` 1 ) e. RR+ )
4		relogcl 22155	. . . . . 6 |- ( ( A ` 1 ) e. RR+ -> ( log ` ( A ` 1 ) ) e. RR )
5	1, 3, 4	mp2b 10	. . . . 5 |- ( log ` ( A ` 1 ) ) e. RR
6		nfcv 2614	. . . . . 6 |- F/_ n 1
7		nfcv 2614	. . . . . . 7 |- F/_ n log
8		nfmpt1 4484	. . . . . . . . 9 |- F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
9	2, 8	nfcxfr 2612	. . . . . . . 8 |- F/_ n A
10	9, 6	nffv 5801	. . . . . . 7 |- F/_ n ( A ` 1 )
11	7, 10	nffv 5801	. . . . . 6 |- F/_ n ( log ` ( A ` 1 ) )
12		fveq2 5794	. . . . . . 7 |- ( n = 1 -> ( A ` n ) = ( A ` 1 ) )
13	12	fveq2d 5798	. . . . . 6 |- ( n = 1 -> ( log ` ( A ` n ) ) = ( log ` ( A ` 1 ) ) )
14		stirlinglem12.2	. . . . . 6 |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
15	6, 11, 13, 14	fvmptf 5894	. . . . 5 |- ( ( 1 e. NN /\ ( log ` ( A ` 1 ) ) e. RR ) -> ( B ` 1 ) = ( log ` ( A ` 1 ) ) )
16	1, 5, 15	mp2an 672	. . . 4 |- ( B ` 1 ) = ( log ` ( A ` 1 ) )
17	16, 5	eqeltri 2536	. . 3 |- ( B ` 1 ) e. RR
18	17	a1i 11	. 2 |- ( N e. NN -> ( B ` 1 ) e. RR )
19	2	stirlinglem2 30013	. . . . 5 |- ( N e. NN -> ( A ` N ) e. RR+ )
20	19	relogcld 22200	. . . 4 |- ( N e. NN -> ( log ` ( A ` N ) ) e. RR )
21		nfcv 2614	. . . . 5 |- F/_ n N
22	9, 21	nffv 5801	. . . . . 6 |- F/_ n ( A ` N )
23	7, 22	nffv 5801	. . . . 5 |- F/_ n ( log ` ( A ` N ) )
24		fveq2 5794	. . . . . 6 |- ( n = N -> ( A ` n ) = ( A ` N ) )
25	24	fveq2d 5798	. . . . 5 |- ( n = N -> ( log ` ( A ` n ) ) = ( log ` ( A ` N ) ) )
26	21, 23, 25, 14	fvmptf 5894	. . . 4 |- ( ( N e. NN /\ ( log ` ( A ` N ) ) e. RR ) -> ( B ` N ) = ( log ` ( A ` N ) ) )
27	20, 26	mpdan 668	. . 3 |- ( N e. NN -> ( B ` N ) = ( log ` ( A ` N ) ) )
28	27, 20	eqeltrd 2540	. 2 |- ( N e. NN -> ( B ` N ) e. RR )
29		4re 10504	. . . 4 |- 4 e. RR
30		4ne0 10524	. . . 4 |- 4 =/= 0
31	29, 30	rereccli 10202	. . 3 |- ( 1 / 4 ) e. RR
32	31	a1i 11	. 2 |- ( N e. NN -> ( 1 / 4 ) e. RR )
33		fveq2 5794	. . . . 5 |- ( k = j -> ( B ` k ) = ( B ` j ) )
34		fveq2 5794	. . . . 5 |- ( k = ( j + 1 ) -> ( B ` k ) = ( B ` ( j + 1 ) ) )
35		fveq2 5794	. . . . 5 |- ( k = 1 -> ( B ` k ) = ( B ` 1 ) )
36		fveq2 5794	. . . . 5 |- ( k = N -> ( B ` k ) = ( B ` N ) )
37		elnnuz 11003	. . . . . 6 |- ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
38	37	biimpi 194	. . . . 5 |- ( N e. NN -> N e. ( ZZ>= ` 1 ) )
39		elfznn 11590	. . . . . . . 8 |- ( k e. ( 1 ... N ) -> k e. NN )
40	2	stirlinglem2 30013	. . . . . . . . . 10 |- ( k e. NN -> ( A ` k ) e. RR+ )
41	39, 40	syl 16	. . . . . . . . 9 |- ( k e. ( 1 ... N ) -> ( A ` k ) e. RR+ )
42	41	relogcld 22200	. . . . . . . 8 |- ( k e. ( 1 ... N ) -> ( log ` ( A ` k ) ) e. RR )
43		nfcv 2614	. . . . . . . . 9 |- F/_ n k
44	9, 43	nffv 5801	. . . . . . . . . 10 |- F/_ n ( A ` k )
45	7, 44	nffv 5801	. . . . . . . . 9 |- F/_ n ( log ` ( A ` k ) )
46		fveq2 5794	. . . . . . . . . 10 |- ( n = k -> ( A ` n ) = ( A ` k ) )
47	46	fveq2d 5798	. . . . . . . . 9 |- ( n = k -> ( log ` ( A ` n ) ) = ( log ` ( A ` k ) ) )
48	43, 45, 47, 14	fvmptf 5894	. . . . . . . 8 |- ( ( k e. NN /\ ( log ` ( A ` k ) ) e. RR ) -> ( B ` k ) = ( log ` ( A ` k ) ) )
49	39, 42, 48	syl2anc 661	. . . . . . 7 |- ( k e. ( 1 ... N ) -> ( B ` k ) = ( log ` ( A ` k ) ) )
50	49	adantl 466	. . . . . 6 |- ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( B ` k ) = ( log ` ( A ` k ) ) )
51	41	rpcnd 11135	. . . . . . . 8 |- ( k e. ( 1 ... N ) -> ( A ` k ) e. CC )
52	51	adantl 466	. . . . . . 7 |- ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. CC )
53	40	rpne0d 11138	. . . . . . . . 9 |- ( k e. NN -> ( A ` k ) =/= 0 )
54	39, 53	syl 16	. . . . . . . 8 |- ( k e. ( 1 ... N ) -> ( A ` k ) =/= 0 )
55	54	adantl 466	. . . . . . 7 |- ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( A ` k ) =/= 0 )
56	52, 55	logcld 22150	. . . . . 6 |- ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( log ` ( A ` k ) ) e. CC )
57	50, 56	eqeltrd 2540	. . . . 5 |- ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. CC )
58	33, 34, 35, 36, 38, 57	fsumtscopo 13378	. . . 4 |- ( N e. NN -> sum_ j e. ( 1..^ N ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) = ( ( B ` 1 ) - ( B ` N ) ) )
59		nnz 10774	. . . . . 6 |- ( N e. NN -> N e. ZZ )
60		fzoval 11666	. . . . . 6 |- ( N e. ZZ -> ( 1..^ N ) = ( 1 ... ( N - 1 ) ) )
61	59, 60	syl 16	. . . . 5 |- ( N e. NN -> ( 1..^ N ) = ( 1 ... ( N - 1 ) ) )
62	61	sumeq1d 13291	. . . 4 |- ( N e. NN -> sum_ j e. ( 1..^ N ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) = sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) )
63	58, 62	eqtr3d 2495	. . 3 |- ( N e. NN -> ( ( B ` 1 ) - ( B ` N ) ) = sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) )
64		fzfid 11907	. . . . 5 |- ( N e. NN -> ( 1 ... ( N - 1 ) ) e. Fin )
65		elfznn 11590	. . . . . . . 8 |- ( j e. ( 1 ... ( N - 1 ) ) -> j e. NN )
66	65	adantl 466	. . . . . . 7 |- ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> j e. NN )
67	2	stirlinglem2 30013	. . . . . . . . . 10 |- ( j e. NN -> ( A ` j ) e. RR+ )
68	67	relogcld 22200	. . . . . . . . 9 |- ( j e. NN -> ( log ` ( A ` j ) ) e. RR )
69		nfcv 2614	. . . . . . . . . 10 |- F/_ n j
70	9, 69	nffv 5801	. . . . . . . . . . 11 |- F/_ n ( A ` j )
71	7, 70	nffv 5801	. . . . . . . . . 10 |- F/_ n ( log ` ( A ` j ) )
72		fveq2 5794	. . . . . . . . . . 11 |- ( n = j -> ( A ` n ) = ( A ` j ) )
73	72	fveq2d 5798	. . . . . . . . . 10 |- ( n = j -> ( log ` ( A ` n ) ) = ( log ` ( A ` j ) ) )
74	69, 71, 73, 14	fvmptf 5894	. . . . . . . . 9 |- ( ( j e. NN /\ ( log ` ( A ` j ) ) e. RR ) -> ( B ` j ) = ( log ` ( A ` j ) ) )
75	68, 74	mpdan 668	. . . . . . . 8 |- ( j e. NN -> ( B ` j ) = ( log ` ( A ` j ) ) )
76	75, 68	eqeltrd 2540	. . . . . . 7 |- ( j e. NN -> ( B ` j ) e. RR )
77	66, 76	syl 16	. . . . . 6 |- ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( B ` j ) e. RR )
78		peano2nn 10440	. . . . . . . . . 10 |- ( j e. NN -> ( j + 1 ) e. NN )
79	2	stirlinglem2 30013	. . . . . . . . . . . 12 |- ( ( j + 1 ) e. NN -> ( A ` ( j + 1 ) ) e. RR+ )
80	78, 79	syl 16	. . . . . . . . . . 11 |- ( j e. NN -> ( A ` ( j + 1 ) ) e. RR+ )
81	80	relogcld 22200	. . . . . . . . . 10 |- ( j e. NN -> ( log ` ( A ` ( j + 1 ) ) ) e. RR )
82		nfcv 2614	. . . . . . . . . . 11 |- F/_ n ( j + 1 )
83	9, 82	nffv 5801	. . . . . . . . . . . 12 |- F/_ n ( A ` ( j + 1 ) )
84	7, 83	nffv 5801	. . . . . . . . . . 11 |- F/_ n ( log ` ( A ` ( j + 1 ) ) )
85		fveq2 5794	. . . . . . . . . . . 12 |- ( n = ( j + 1 ) -> ( A ` n ) = ( A ` ( j + 1 ) ) )
86	85	fveq2d 5798	. . . . . . . . . . 11 |- ( n = ( j + 1 ) -> ( log ` ( A ` n ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
87	82, 84, 86, 14	fvmptf 5894	. . . . . . . . . 10 |- ( ( ( j + 1 ) e. NN /\ ( log ` ( A ` ( j + 1 ) ) ) e. RR ) -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
88	78, 81, 87	syl2anc 661	. . . . . . . . 9 |- ( j e. NN -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
89	88, 81	eqeltrd 2540	. . . . . . . 8 |- ( j e. NN -> ( B ` ( j + 1 ) ) e. RR )
90	65, 89	syl 16	. . . . . . 7 |- ( j e. ( 1 ... ( N - 1 ) ) -> ( B ` ( j + 1 ) ) e. RR )
91	90	adantl 466	. . . . . 6 |- ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( B ` ( j + 1 ) ) e. RR )
92	77, 91	resubcld 9882	. . . . 5 |- ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( ( B ` j ) - ( B ` ( j + 1 ) ) ) e. RR )
93	64, 92	fsumrecl 13324	. . . 4 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) e. RR )
94	31	a1i 11	. . . . . 6 |- ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( 1 / 4 ) e. RR )
95	65	nnred 10443	. . . . . . . . 9 |- ( j e. ( 1 ... ( N - 1 ) ) -> j e. RR )
96		1re 9491	. . . . . . . . . . 11 |- 1 e. RR
97	96	a1i 11	. . . . . . . . . 10 |- ( j e. ( 1 ... ( N - 1 ) ) -> 1 e. RR )
98	95, 97	readdcld 9519	. . . . . . . . 9 |- ( j e. ( 1 ... ( N - 1 ) ) -> ( j + 1 ) e. RR )
99	95, 98	remulcld 9520	. . . . . . . 8 |- ( j e. ( 1 ... ( N - 1 ) ) -> ( j x. ( j + 1 ) ) e. RR )
100	95	recnd 9518	. . . . . . . . 9 |- ( j e. ( 1 ... ( N - 1 ) ) -> j e. CC )
101		ax-1cn 9446	. . . . . . . . . . 11 |- 1 e. CC
102	101	a1i 11	. . . . . . . . . 10 |- ( j e. ( 1 ... ( N - 1 ) ) -> 1 e. CC )
103	100, 102	addcld 9511	. . . . . . . . 9 |- ( j e. ( 1 ... ( N - 1 ) ) -> ( j + 1 ) e. CC )
104	65	nnne0d 10472	. . . . . . . . 9 |- ( j e. ( 1 ... ( N - 1 ) ) -> j =/= 0 )
105	78	nnne0d 10472	. . . . . . . . . 10 |- ( j e. NN -> ( j + 1 ) =/= 0 )
106	65, 105	syl 16	. . . . . . . . 9 |- ( j e. ( 1 ... ( N - 1 ) ) -> ( j + 1 ) =/= 0 )
107	100, 103, 104, 106	mulne0d 10094	. . . . . . . 8 |- ( j e. ( 1 ... ( N - 1 ) ) -> ( j x. ( j + 1 ) ) =/= 0 )
108	99, 107	rereccld 10264	. . . . . . 7 |- ( j e. ( 1 ... ( N - 1 ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
109	108	adantl 466	. . . . . 6 |- ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
110	94, 109	remulcld 9520	. . . . 5 |- ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) e. RR )
111	64, 110	fsumrecl 13324	. . . 4 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) e. RR )
112		eqid 2452	. . . . . . 7 |- ( i e. NN |-> ( ( 1 / ( ( 2 x. i ) + 1 ) ) x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) ^ ( 2 x. i ) ) ) ) = ( i e. NN |-> ( ( 1 / ( ( 2 x. i ) + 1 ) ) x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) ^ ( 2 x. i ) ) ) )
113		eqid 2452	. . . . . . 7 |- ( i e. NN |-> ( ( 1 / ( ( ( 2 x. j ) + 1 ) ^ 2 ) ) ^ i ) ) = ( i e. NN |-> ( ( 1 / ( ( ( 2 x. j ) + 1 ) ^ 2 ) ) ^ i ) )
114	2, 14, 112, 113	stirlinglem10 30021	. . . . . 6 |- ( j e. NN -> ( ( B ` j ) - ( B ` ( j + 1 ) ) ) <_ ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) )
115	66, 114	syl 16	. . . . 5 |- ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( ( B ` j ) - ( B ` ( j + 1 ) ) ) <_ ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) )
116	64, 92, 110, 115	fsumle 13375	. . . 4 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) <_ sum_ j e. ( 1 ... ( N - 1 ) ) ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) )
117	64, 109	fsumrecl 13324	. . . . . 6 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
118	96	a1i 11	. . . . . 6 |- ( N e. NN -> 1 e. RR )
119		4pos 10523	. . . . . . . . 9 |- 0 < 4
120	29, 119	elrpii 11100	. . . . . . . 8 |- 4 e. RR+
121	120	a1i 11	. . . . . . 7 |- ( N e. NN -> 4 e. RR+ )
122		0re 9492	. . . . . . . . 9 |- 0 e. RR
123	122	a1i 11	. . . . . . . 8 |- ( N e. NN -> 0 e. RR )
124		0lt1 9968	. . . . . . . . 9 |- 0 < 1
125	124	a1i 11	. . . . . . . 8 |- ( N e. NN -> 0 < 1 )
126	123, 118, 125	ltled 9628	. . . . . . 7 |- ( N e. NN -> 0 <_ 1 )
127	118, 121, 126	divge0d 11169	. . . . . 6 |- ( N e. NN -> 0 <_ ( 1 / 4 ) )
128		eqid 2452	. . . . . . . . . 10 |- ( ZZ>= ` N ) = ( ZZ>= ` N )
129		nnuz 11002	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
130	129	uztrn2 10984	. . . . . . . . . . 11 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j e. NN )
131		stirlinglem12.3	. . . . . . . . . . . . 13 |- F = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )
132	131	a1i 11	. . . . . . . . . . . 12 |- ( j e. NN -> F = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) )
133		simpr 461	. . . . . . . . . . . . . 14 |- ( ( j e. NN /\ n = j ) -> n = j )
134	133	oveq1d 6210	. . . . . . . . . . . . . 14 |- ( ( j e. NN /\ n = j ) -> ( n + 1 ) = ( j + 1 ) )
135	133, 134	oveq12d 6213	. . . . . . . . . . . . 13 |- ( ( j e. NN /\ n = j ) -> ( n x. ( n + 1 ) ) = ( j x. ( j + 1 ) ) )
136	135	oveq2d 6211	. . . . . . . . . . . 12 |- ( ( j e. NN /\ n = j ) -> ( 1 / ( n x. ( n + 1 ) ) ) = ( 1 / ( j x. ( j + 1 ) ) ) )
137		id 22	. . . . . . . . . . . 12 |- ( j e. NN -> j e. NN )
138		nnre 10435	. . . . . . . . . . . . . 14 |- ( j e. NN -> j e. RR )
139	96	a1i 11	. . . . . . . . . . . . . . 15 |- ( j e. NN -> 1 e. RR )
140	138, 139	readdcld 9519	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( j + 1 ) e. RR )
141	138, 140	remulcld 9520	. . . . . . . . . . . . 13 |- ( j e. NN -> ( j x. ( j + 1 ) ) e. RR )
142		nncn 10436	. . . . . . . . . . . . . 14 |- ( j e. NN -> j e. CC )
143	101	a1i 11	. . . . . . . . . . . . . . 15 |- ( j e. NN -> 1 e. CC )
144	142, 143	addcld 9511	. . . . . . . . . . . . . 14 |- ( j e. NN -> ( j + 1 ) e. CC )
145		nnne0 10460	. . . . . . . . . . . . . 14 |- ( j e. NN -> j =/= 0 )
146	142, 144, 145, 105	mulne0d 10094	. . . . . . . . . . . . 13 |- ( j e. NN -> ( j x. ( j + 1 ) ) =/= 0 )
147	141, 146	rereccld 10264	. . . . . . . . . . . 12 |- ( j e. NN -> ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
148	132, 136, 137, 147	fvmptd 5883	. . . . . . . . . . 11 |- ( j e. NN -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
149	130, 148	syl 16	. . . . . . . . . 10 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
150	130	nnred 10443	. . . . . . . . . . . 12 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j e. RR )
151	96	a1i 11	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 1 e. RR )
152	150, 151	readdcld 9519	. . . . . . . . . . . 12 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j + 1 ) e. RR )
153	150, 152	remulcld 9520	. . . . . . . . . . 11 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j x. ( j + 1 ) ) e. RR )
154	150	recnd 9518	. . . . . . . . . . . 12 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j e. CC )
155	101	a1i 11	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 1 e. CC )
156	154, 155	addcld 9511	. . . . . . . . . . . 12 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j + 1 ) e. CC )
157	130	nnne0d 10472	. . . . . . . . . . . 12 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j =/= 0 )
158	130, 105	syl 16	. . . . . . . . . . . 12 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j + 1 ) =/= 0 )
159	154, 156, 157, 158	mulne0d 10094	. . . . . . . . . . 11 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j x. ( j + 1 ) ) =/= 0 )
160	153, 159	rereccld 10264	. . . . . . . . . 10 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
161		seqeq1 11921	. . . . . . . . . . . . 13 |- ( N = 1 -> seq N ( + , F ) = seq 1 ( + , F ) )
162	131	trireciplem 13437	. . . . . . . . . . . . . . 15 |- seq 1 ( + , F ) ~~> 1
163		climrel 13083	. . . . . . . . . . . . . . . 16 |- Rel ~~>
164	163	releldmi 5179	. . . . . . . . . . . . . . 15 |- ( seq 1 ( + , F ) ~~> 1 -> seq 1 ( + , F ) e. dom ~~> )
165	162, 164	ax-mp 5	. . . . . . . . . . . . . 14 |- seq 1 ( + , F ) e. dom ~~>
166	165	a1i 11	. . . . . . . . . . . . 13 |- ( N = 1 -> seq 1 ( + , F ) e. dom ~~> )
167	161, 166	eqeltrd 2540	. . . . . . . . . . . 12 |- ( N = 1 -> seq N ( + , F ) e. dom ~~> )
168	167	adantl 466	. . . . . . . . . . 11 |- ( ( N e. NN /\ N = 1 ) -> seq N ( + , F ) e. dom ~~> )
169		simpl 457	. . . . . . . . . . . 12 |- ( ( N e. NN /\ -. N = 1 ) -> N e. NN )
170		simpr 461	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ -. N = 1 ) -> -. N = 1 )
171		elnn1uz2 11037	. . . . . . . . . . . . . . . 16 |- ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
172	169, 171	sylib 196	. . . . . . . . . . . . . . 15 |- ( ( N e. NN /\ -. N = 1 ) -> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
173	172	ord 377	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ -. N = 1 ) -> ( -. N = 1 -> N e. ( ZZ>= ` 2 ) ) )
174	170, 173	mpd 15	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ -. N = 1 ) -> N e. ( ZZ>= ` 2 ) )
175		uz2m1nn 11035	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
176	174, 175	syl 16	. . . . . . . . . . . 12 |- ( ( N e. NN /\ -. N = 1 ) -> ( N - 1 ) e. NN )
177		nncn 10436	. . . . . . . . . . . . . . . . . 18 |- ( N e. NN -> N e. CC )
178	177	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( N e. NN /\ ( N - 1 ) e. NN ) -> N e. CC )
179	101	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( N e. NN /\ ( N - 1 ) e. NN ) -> 1 e. CC )
180	178, 179	npcand 9829	. . . . . . . . . . . . . . . 16 |- ( ( N e. NN /\ ( N - 1 ) e. NN ) -> ( ( N - 1 ) + 1 ) = N )
181	180	eqcomd 2460	. . . . . . . . . . . . . . 15 |- ( ( N e. NN /\ ( N - 1 ) e. NN ) -> N = ( ( N - 1 ) + 1 ) )
182	181	seqeq1d 11924	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ ( N - 1 ) e. NN ) -> seq N ( + , F ) = seq ( ( N - 1 ) + 1 ) ( + , F ) )
183		id 22	. . . . . . . . . . . . . . . 16 |- ( ( N - 1 ) e. NN -> ( N - 1 ) e. NN )
184	147	recnd 9518	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
185	148, 184	eqeltrd 2540	. . . . . . . . . . . . . . . . 17 |- ( j e. NN -> ( F ` j ) e. CC )
186	185	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ( N - 1 ) e. NN /\ j e. NN ) -> ( F ` j ) e. CC )
187	162	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( N - 1 ) e. NN -> seq 1 ( + , F ) ~~> 1 )
188	129, 183, 186, 187	clim2ser 13245	. . . . . . . . . . . . . . 15 |- ( ( N - 1 ) e. NN -> seq ( ( N - 1 ) + 1 ) ( + , F ) ~~> ( 1 - ( seq 1 ( + , F ) ` ( N - 1 ) ) ) )
189	188	adantl 466	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ ( N - 1 ) e. NN ) -> seq ( ( N - 1 ) + 1 ) ( + , F ) ~~> ( 1 - ( seq 1 ( + , F ) ` ( N - 1 ) ) ) )
190	182, 189	eqbrtrd 4415	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ ( N - 1 ) e. NN ) -> seq N ( + , F ) ~~> ( 1 - ( seq 1 ( + , F ) ` ( N - 1 ) ) ) )
191	163	releldmi 5179	. . . . . . . . . . . . 13 |- ( seq N ( + , F ) ~~> ( 1 - ( seq 1 ( + , F ) ` ( N - 1 ) ) ) -> seq N ( + , F ) e. dom ~~> )
192	190, 191	syl 16	. . . . . . . . . . . 12 |- ( ( N e. NN /\ ( N - 1 ) e. NN ) -> seq N ( + , F ) e. dom ~~> )
193	169, 176, 192	syl2anc 661	. . . . . . . . . . 11 |- ( ( N e. NN /\ -. N = 1 ) -> seq N ( + , F ) e. dom ~~> )
194	168, 193	pm2.61dan 789	. . . . . . . . . 10 |- ( N e. NN -> seq N ( + , F ) e. dom ~~> )
195	128, 59, 149, 160, 194	isumrecl 13345	. . . . . . . . 9 |- ( N e. NN -> sum_ j e. ( ZZ>= ` N ) ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
196	130	nnrpd 11132	. . . . . . . . . . . 12 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j e. RR+ )
197	196	rpge0d 11137	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 0 <_ j )
198	150, 197	ge0p1rpd 11159	. . . . . . . . . . . 12 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j + 1 ) e. RR+ )
199	196, 198	rpmulcld 11149	. . . . . . . . . . 11 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j x. ( j + 1 ) ) e. RR+ )
200	126	adantr 465	. . . . . . . . . . 11 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 0 <_ 1 )
201	151, 199, 200	divge0d 11169	. . . . . . . . . 10 |- ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 0 <_ ( 1 / ( j x. ( j + 1 ) ) ) )
202	128, 59, 149, 160, 194, 201	isumge0 13346	. . . . . . . . 9 |- ( N e. NN -> 0 <_ sum_ j e. ( ZZ>= ` N ) ( 1 / ( j x. ( j + 1 ) ) ) )
203	123, 195, 117, 202	leadd2dd 10060	. . . . . . . 8 |- ( N e. NN -> ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + 0 ) <_ ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + sum_ j e. ( ZZ>= ` N ) ( 1 / ( j x. ( j + 1 ) ) ) ) )
204	117	recnd 9518	. . . . . . . . . 10 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
205	204	addid1d 9675	. . . . . . . . 9 |- ( N e. NN -> ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + 0 ) = sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) )
206	205	eqcomd 2460	. . . . . . . 8 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) = ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + 0 ) )
207		id 22	. . . . . . . . 9 |- ( N e. NN -> N e. NN )
208	148	adantl 466	. . . . . . . . 9 |- ( ( N e. NN /\ j e. NN ) -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
209	142	adantl 466	. . . . . . . . . . 11 |- ( ( N e. NN /\ j e. NN ) -> j e. CC )
210	101	a1i 11	. . . . . . . . . . . 12 |- ( ( N e. NN /\ j e. NN ) -> 1 e. CC )
211	209, 210	addcld 9511	. . . . . . . . . . 11 |- ( ( N e. NN /\ j e. NN ) -> ( j + 1 ) e. CC )
212	209, 211	mulcld 9512	. . . . . . . . . 10 |- ( ( N e. NN /\ j e. NN ) -> ( j x. ( j + 1 ) ) e. CC )
213	145	adantl 466	. . . . . . . . . . 11 |- ( ( N e. NN /\ j e. NN ) -> j =/= 0 )
214	105	adantl 466	. . . . . . . . . . 11 |- ( ( N e. NN /\ j e. NN ) -> ( j + 1 ) =/= 0 )
215	209, 211, 213, 214	mulne0d 10094	. . . . . . . . . 10 |- ( ( N e. NN /\ j e. NN ) -> ( j x. ( j + 1 ) ) =/= 0 )
216	212, 215	reccld 10206	. . . . . . . . 9 |- ( ( N e. NN /\ j e. NN ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
217	165	a1i 11	. . . . . . . . 9 |- ( N e. NN -> seq 1 ( + , F ) e. dom ~~> )
218	129, 128, 207, 208, 216, 217	isumsplit 13416	. . . . . . . 8 |- ( N e. NN -> sum_ j e. NN ( 1 / ( j x. ( j + 1 ) ) ) = ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + sum_ j e. ( ZZ>= ` N ) ( 1 / ( j x. ( j + 1 ) ) ) ) )
219	203, 206, 218	3brtr4d 4425	. . . . . . 7 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) <_ sum_ j e. NN ( 1 / ( j x. ( j + 1 ) ) ) )
220		1z 10782	. . . . . . . . . . 11 |- 1 e. ZZ
221	220	a1i 11	. . . . . . . . . 10 |- ( T. -> 1 e. ZZ )
222	148	adantl 466	. . . . . . . . . 10 |- ( ( T. /\ j e. NN ) -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
223	184	adantl 466	. . . . . . . . . 10 |- ( ( T. /\ j e. NN ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
224	162	a1i 11	. . . . . . . . . 10 |- ( T. -> seq 1 ( + , F ) ~~> 1 )
225	129, 221, 222, 223, 224	isumclim 13337	. . . . . . . . 9 |- ( T. -> sum_ j e. NN ( 1 / ( j x. ( j + 1 ) ) ) = 1 )
226	225	trud 1379	. . . . . . . 8 |- sum_ j e. NN ( 1 / ( j x. ( j + 1 ) ) ) = 1
227	226	a1i 11	. . . . . . 7 |- ( N e. NN -> sum_ j e. NN ( 1 / ( j x. ( j + 1 ) ) ) = 1 )
228	219, 227	breqtrd 4419	. . . . . 6 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) <_ 1 )
229	117, 118, 32, 127, 228	lemul2ad 10379	. . . . 5 |- ( N e. NN -> ( ( 1 / 4 ) x. sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) ) <_ ( ( 1 / 4 ) x. 1 ) )
230		4cn 10505	. . . . . . . 8 |- 4 e. CC
231	230	a1i 11	. . . . . . 7 |- ( N e. NN -> 4 e. CC )
232	119	a1i 11	. . . . . . . 8 |- ( N e. NN -> 0 < 4 )
233	232	gt0ne0d 10010	. . . . . . 7 |- ( N e. NN -> 4 =/= 0 )
234	231, 233	reccld 10206	. . . . . 6 |- ( N e. NN -> ( 1 / 4 ) e. CC )
235	109	recnd 9518	. . . . . 6 |- ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
236	64, 234, 235	fsummulc2 13364	. . . . 5 |- ( N e. NN -> ( ( 1 / 4 ) x. sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) ) = sum_ j e. ( 1 ... ( N - 1 ) ) ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) )
237	234	mulid1d 9509	. . . . 5 |- ( N e. NN -> ( ( 1 / 4 ) x. 1 ) = ( 1 / 4 ) )
238	229, 236, 237	3brtr3d 4424	. . . 4 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) <_ ( 1 / 4 ) )
239	93, 111, 32, 116, 238	letrd 9634	. . 3 |- ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) <_ ( 1 / 4 ) )
240	63, 239	eqbrtrd 4415	. 2 |- ( N e. NN -> ( ( B ` 1 ) - ( B ` N ) ) <_ ( 1 / 4 ) )
241	18, 28, 32, 240	subled 10048	1 |- ( N e. NN -> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` N ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1370   T. wtru 1371   e. wcel 1758   =/= wne 2645   class class class wbr 4395   |-> cmpt 4453   dom cdm 4943   ` cfv 5521  (class class class)co 6195   CCcc 9386   RRcr 9387   0cc0 9388   1c1 9389   + caddc 9391   x. cmul 9393   < clt 9524   <_ cle 9525   - cmin 9701   / cdiv 10099   NNcn 10428   2c2 10477   4c4 10479   ZZcz 10752   ZZ>=cuz 10967   RR+crp 11097   ...cfz 11549  ..^cfzo 11660   seqcseq 11918   ^cexp 11977   !cfa 12163   sqrcsqr 12835   ~~> cli 13075   sum_csu 13276   _eceu 13461   logclog 22134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4573  ax-pr 4634  ax-un 6477  ax-inf2 7953  ax-cnex 9444  ax-resscn 9445  ax-1cn 9446  ax-icn 9447  ax-addcl 9448  ax-addrcl 9449  ax-mulcl 9450  ax-mulrcl 9451  ax-mulcom 9452  ax-addass 9453  ax-mulass 9454  ax-distr 9455  ax-i2m1 9456  ax-1ne0 9457  ax-1rid 9458  ax-rnegex 9459  ax-rrecex 9460  ax-cnre 9461  ax-pre-lttri 9462  ax-pre-lttrn 9463  ax-pre-ltadd 9464  ax-pre-mulgt0 9465  ax-pre-sup 9466  ax-addf 9467  ax-mulf 9468

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-nel 2648  df-ral 2801  df-rex 2802  df-reu 2803  df-rmo 2804  df-rab 2805  df-v 3074  df-sbc 3289  df-csb 3391  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-pss 3447  df-nul 3741  df-if 3895  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4195  df-int 4232  df-iun 4276  df-iin 4277  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4489  df-eprel 4735  df-id 4739  df-po 4744  df-so 4745  df-fr 4782  df-se 4783  df-we 4784  df-ord 4825  df-on 4826  df-lim 4827  df-suc 4828  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-rn 4954  df-res 4955  df-ima 4956  df-iota 5484  df-fun 5523  df-fn 5524  df-f 5525  df-f1 5526  df-fo 5527  df-f1o 5528  df-fv 5529  df-isom 5530  df-riota 6156  df-ov 6198  df-oprab 6199  df-mpt2 6200  df-of 6425  df-om 6582  df-1st 6682  df-2nd 6683  df-supp 6796  df-recs 6937  df-rdg 6971  df-1o 7025  df-2o 7026  df-oadd 7029  df-er 7206  df-map 7321  df-pm 7322  df-ixp 7369  df-en 7416  df-dom 7417  df-sdom 7418  df-fin 7419  df-fsupp 7727  df-fi 7767  df-sup 7797  df-oi 7830  df-card 8215  df-cda 8443  df-pnf 9526  df-mnf 9527  df-xr 9528  df-ltxr 9529  df-le 9530  df-sub 9703  df-neg 9704  df-div 10100  df-nn 10429  df-2 10486  df-3 10487  df-4 10488  df-5 10489  df-6 10490  df-7 10491  df-8 10492  df-9 10493  df-10 10494  df-n0 10686  df-z 10753  df-dec 10862  df-uz 10968  df-q 11060  df-rp 11098  df-xneg 11195  df-xadd 11196  df-xmul 11197  df-ioo 11410  df-ioc 11411  df-ico 11412  df-icc 11413  df-fz 11550  df-fzo 11661  df-fl 11754  df-mod 11821  df-seq 11919  df-exp 11978  df-fac 12164  df-bc 12191  df-hash 12216  df-shft 12669  df-cj 12701  df-re 12702  df-im 12703  df-sqr 12837  df-abs 12838  df-limsup 13062  df-clim 13079  df-rlim 13080  df-sum 13277  df-ef 13466  df-e 13467  df-sin 13468  df-cos 13469  df-tan 13470  df-pi 13471  df-dvds 13649  df-struct 14289  df-ndx 14290  df-slot 14291  df-base 14292  df-sets 14293  df-ress 14294  df-plusg 14365  df-mulr 14366  df-starv 14367  df-sca 14368  df-vsca 14369  df-ip 14370  df-tset 14371  df-ple 14372  df-ds 14374  df-unif 14375  df-hom 14376  df-cco 14377  df-rest 14475  df-topn 14476  df-0g 14494  df-gsum 14495  df-topgen 14496  df-pt 14497  df-prds 14500  df-xrs 14554  df-qtop 14559  df-imas 14560  df-xps 14562  df-mre 14638  df-mrc 14639  df-acs 14641  df-mnd 15529  df-submnd 15579  df-mulg 15662  df-cntz 15949  df-cmn 16395  df-psmet 17929  df-xmet 17930  df-met 17931  df-bl 17932  df-mopn 17933  df-fbas 17934  df-fg 17935  df-cnfld 17939  df-top 18630  df-bases 18632  df-topon 18633  df-topsp 18634  df-cld 18750  df-ntr 18751  df-cls 18752  df-nei 18829  df-lp 18867  df-perf 18868  df-cn 18958  df-cnp 18959  df-haus 19046  df-cmp 19117  df-tx 19262  df-hmeo 19455  df-fil 19546  df-fm 19638  df-flim 19639  df-flf 19640  df-xms 20022  df-ms 20023  df-tms 20024  df-cncf 20581  df-limc 21469  df-dv 21470  df-ulm 21970  df-log 22136  df-cxp 22137

This theorem is referenced by:  stirlinglem13  30024