logfaclbnd

Description: A lower bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016)

		Ref	Expression
	Assertion	logfaclbnd	\|- ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) <_ ( log ` ( ! ` ( \|_ ` A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	\|- ( A e. RR+ -> A e. CC )
2	1	times2d	\|- ( A e. RR+ -> ( A x. 2 ) = ( A + A ) )
3	2	oveq2d	\|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - ( A x. 2 ) ) = ( ( A x. ( log ` A ) ) - ( A + A ) ) )
4		relogcl	\|- ( A e. RR+ -> ( log ` A ) e. RR )
5	4	recnd	\|- ( A e. RR+ -> ( log ` A ) e. CC )
6		2cnd	\|- ( A e. RR+ -> 2 e. CC )
7	1 5 6	subdid	\|- ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) = ( ( A x. ( log ` A ) ) - ( A x. 2 ) ) )
8		rpre	\|- ( A e. RR+ -> A e. RR )
9	8 4	remulcld	\|- ( A e. RR+ -> ( A x. ( log ` A ) ) e. RR )
10	9	recnd	\|- ( A e. RR+ -> ( A x. ( log ` A ) ) e. CC )
11	10 1 1	subsub4d	\|- ( A e. RR+ -> ( ( ( A x. ( log ` A ) ) - A ) - A ) = ( ( A x. ( log ` A ) ) - ( A + A ) ) )
12	3 7 11	3eqtr4d	\|- ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) = ( ( ( A x. ( log ` A ) ) - A ) - A ) )
13	9 8	resubcld	\|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) e. RR )
14		fzfid	\|- ( A e. RR+ -> ( 1 ... ( \|_ ` A ) ) e. Fin )
15		fzfid	\|- ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) -> ( 1 ... n ) e. Fin )
16		elfznn	\|- ( d e. ( 1 ... n ) -> d e. NN )
17	16	adantl	\|- ( ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) /\ d e. ( 1 ... n ) ) -> d e. NN )
18	17	nnrecred	\|- ( ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) /\ d e. ( 1 ... n ) ) -> ( 1 / d ) e. RR )
19	15 18	fsumrecl	\|- ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) -> sum_ d e. ( 1 ... n ) ( 1 / d ) e. RR )
20	14 19	fsumrecl	\|- ( A e. RR+ -> sum_ n e. ( 1 ... ( \|_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) e. RR )
21		rprege0	\|- ( A e. RR+ -> ( A e. RR /\ 0 <_ A ) )
22		flge0nn0	\|- ( ( A e. RR /\ 0 <_ A ) -> ( \|_ ` A ) e. NN0 )
23	21 22	syl	\|- ( A e. RR+ -> ( \|_ ` A ) e. NN0 )
24	23	faccld	\|- ( A e. RR+ -> ( ! ` ( \|_ ` A ) ) e. NN )
25	24	nnrpd	\|- ( A e. RR+ -> ( ! ` ( \|_ ` A ) ) e. RR+ )
26	25	relogcld	\|- ( A e. RR+ -> ( log ` ( ! ` ( \|_ ` A ) ) ) e. RR )
27	26 8	readdcld	\|- ( A e. RR+ -> ( ( log ` ( ! ` ( \|_ ` A ) ) ) + A ) e. RR )
28		elfznn	\|- ( d e. ( 1 ... ( \|_ ` A ) ) -> d e. NN )
29	28	adantl	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> d e. NN )
30	29	nnrecred	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( 1 / d ) e. RR )
31	14 30	fsumrecl	\|- ( A e. RR+ -> sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) e. RR )
32	8 31	remulcld	\|- ( A e. RR+ -> ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) e. RR )
33		reflcl	\|- ( A e. RR -> ( \|_ ` A ) e. RR )
34	8 33	syl	\|- ( A e. RR+ -> ( \|_ ` A ) e. RR )
35	32 34	resubcld	\|- ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) - ( \|_ ` A ) ) e. RR )
36		harmoniclbnd	\|- ( A e. RR+ -> ( log ` A ) <_ sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) )
37		rpregt0	\|- ( A e. RR+ -> ( A e. RR /\ 0 < A ) )
38		lemul2	\|- ( ( ( log ` A ) e. RR /\ sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( log ` A ) <_ sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) <-> ( A x. ( log ` A ) ) <_ ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) ) )
39	4 31 37 38	syl3anc	\|- ( A e. RR+ -> ( ( log ` A ) <_ sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) <-> ( A x. ( log ` A ) ) <_ ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) ) )
40	36 39	mpbid	\|- ( A e. RR+ -> ( A x. ( log ` A ) ) <_ ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) )
41		flle	\|- ( A e. RR -> ( \|_ ` A ) <_ A )
42	8 41	syl	\|- ( A e. RR+ -> ( \|_ ` A ) <_ A )
43	9 34 32 8 40 42	le2subd	\|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) <_ ( ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) - ( \|_ ` A ) ) )
44	28	nnrecred	\|- ( d e. ( 1 ... ( \|_ ` A ) ) -> ( 1 / d ) e. RR )
45		remulcl	\|- ( ( A e. RR /\ ( 1 / d ) e. RR ) -> ( A x. ( 1 / d ) ) e. RR )
46	8 44 45	syl2an	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( A x. ( 1 / d ) ) e. RR )
47		peano2rem	\|- ( ( A x. ( 1 / d ) ) e. RR -> ( ( A x. ( 1 / d ) ) - 1 ) e. RR )
48	46 47	syl	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - 1 ) e. RR )
49		fzfid	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( d ... ( \|_ ` A ) ) e. Fin )
50	30	adantr	\|- ( ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) /\ n e. ( d ... ( \|_ ` A ) ) ) -> ( 1 / d ) e. RR )
51	49 50	fsumrecl	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> sum_ n e. ( d ... ( \|_ ` A ) ) ( 1 / d ) e. RR )
52	8	adantr	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> A e. RR )
53	52 33	syl	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( \|_ ` A ) e. RR )
54		peano2re	\|- ( ( \|_ ` A ) e. RR -> ( ( \|_ ` A ) + 1 ) e. RR )
55	53 54	syl	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( \|_ ` A ) + 1 ) e. RR )
56	29	nnred	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> d e. RR )
57		fllep1	\|- ( A e. RR -> A <_ ( ( \|_ ` A ) + 1 ) )
58	8 57	syl	\|- ( A e. RR+ -> A <_ ( ( \|_ ` A ) + 1 ) )
59	58	adantr	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> A <_ ( ( \|_ ` A ) + 1 ) )
60	52 55 56 59	lesub1dd	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( A - d ) <_ ( ( ( \|_ ` A ) + 1 ) - d ) )
61	52 56	resubcld	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( A - d ) e. RR )
62	55 56	resubcld	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( ( \|_ ` A ) + 1 ) - d ) e. RR )
63	29	nnrpd	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> d e. RR+ )
64	63	rpreccld	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( 1 / d ) e. RR+ )
65	61 62 64	lemul1d	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( A - d ) <_ ( ( ( \|_ ` A ) + 1 ) - d ) <-> ( ( A - d ) x. ( 1 / d ) ) <_ ( ( ( ( \|_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) ) )
66	60 65	mpbid	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( A - d ) x. ( 1 / d ) ) <_ ( ( ( ( \|_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) )
67	1	adantr	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> A e. CC )
68	29	nncnd	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> d e. CC )
69	30	recnd	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( 1 / d ) e. CC )
70	67 68 69	subdird	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( A - d ) x. ( 1 / d ) ) = ( ( A x. ( 1 / d ) ) - ( d x. ( 1 / d ) ) ) )
71	29	nnne0d	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> d =/= 0 )
72	68 71	recidd	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( d x. ( 1 / d ) ) = 1 )
73	72	oveq2d	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - ( d x. ( 1 / d ) ) ) = ( ( A x. ( 1 / d ) ) - 1 ) )
74	70 73	eqtr2d	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - 1 ) = ( ( A - d ) x. ( 1 / d ) ) )
75		fsumconst	\|- ( ( ( d ... ( \|_ ` A ) ) e. Fin /\ ( 1 / d ) e. CC ) -> sum_ n e. ( d ... ( \|_ ` A ) ) ( 1 / d ) = ( ( # ` ( d ... ( \|_ ` A ) ) ) x. ( 1 / d ) ) )
76	49 69 75	syl2anc	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> sum_ n e. ( d ... ( \|_ ` A ) ) ( 1 / d ) = ( ( # ` ( d ... ( \|_ ` A ) ) ) x. ( 1 / d ) ) )
77		elfzuz3	\|- ( d e. ( 1 ... ( \|_ ` A ) ) -> ( \|_ ` A ) e. ( ZZ>= ` d ) )
78	77	adantl	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( \|_ ` A ) e. ( ZZ>= ` d ) )
79		hashfz	\|- ( ( \|_ ` A ) e. ( ZZ>= ` d ) -> ( # ` ( d ... ( \|_ ` A ) ) ) = ( ( ( \|_ ` A ) - d ) + 1 ) )
80	78 79	syl	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( # ` ( d ... ( \|_ ` A ) ) ) = ( ( ( \|_ ` A ) - d ) + 1 ) )
81	34	recnd	\|- ( A e. RR+ -> ( \|_ ` A ) e. CC )
82	81	adantr	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( \|_ ` A ) e. CC )
83		1cnd	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> 1 e. CC )
84	82 83 68	addsubd	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( ( \|_ ` A ) + 1 ) - d ) = ( ( ( \|_ ` A ) - d ) + 1 ) )
85	80 84	eqtr4d	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( # ` ( d ... ( \|_ ` A ) ) ) = ( ( ( \|_ ` A ) + 1 ) - d ) )
86	85	oveq1d	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( # ` ( d ... ( \|_ ` A ) ) ) x. ( 1 / d ) ) = ( ( ( ( \|_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) )
87	76 86	eqtrd	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> sum_ n e. ( d ... ( \|_ ` A ) ) ( 1 / d ) = ( ( ( ( \|_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) )
88	66 74 87	3brtr4d	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - 1 ) <_ sum_ n e. ( d ... ( \|_ ` A ) ) ( 1 / d ) )
89	14 48 51 88	fsumle	\|- ( A e. RR+ -> sum_ d e. ( 1 ... ( \|_ ` A ) ) ( ( A x. ( 1 / d ) ) - 1 ) <_ sum_ d e. ( 1 ... ( \|_ ` A ) ) sum_ n e. ( d ... ( \|_ ` A ) ) ( 1 / d ) )
90	14 1 69	fsummulc2	\|- ( A e. RR+ -> ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) = sum_ d e. ( 1 ... ( \|_ ` A ) ) ( A x. ( 1 / d ) ) )
91		ax-1cn	\|- 1 e. CC
92		fsumconst	\|- ( ( ( 1 ... ( \|_ ` A ) ) e. Fin /\ 1 e. CC ) -> sum_ d e. ( 1 ... ( \|_ ` A ) ) 1 = ( ( # ` ( 1 ... ( \|_ ` A ) ) ) x. 1 ) )
93	14 91 92	sylancl	\|- ( A e. RR+ -> sum_ d e. ( 1 ... ( \|_ ` A ) ) 1 = ( ( # ` ( 1 ... ( \|_ ` A ) ) ) x. 1 ) )
94		hashfz1	\|- ( ( \|_ ` A ) e. NN0 -> ( # ` ( 1 ... ( \|_ ` A ) ) ) = ( \|_ ` A ) )
95	23 94	syl	\|- ( A e. RR+ -> ( # ` ( 1 ... ( \|_ ` A ) ) ) = ( \|_ ` A ) )
96	95	oveq1d	\|- ( A e. RR+ -> ( ( # ` ( 1 ... ( \|_ ` A ) ) ) x. 1 ) = ( ( \|_ ` A ) x. 1 ) )
97	81	mulridd	\|- ( A e. RR+ -> ( ( \|_ ` A ) x. 1 ) = ( \|_ ` A ) )
98	93 96 97	3eqtrrd	\|- ( A e. RR+ -> ( \|_ ` A ) = sum_ d e. ( 1 ... ( \|_ ` A ) ) 1 )
99	90 98	oveq12d	\|- ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) - ( \|_ ` A ) ) = ( sum_ d e. ( 1 ... ( \|_ ` A ) ) ( A x. ( 1 / d ) ) - sum_ d e. ( 1 ... ( \|_ ` A ) ) 1 ) )
100	46	recnd	\|- ( ( A e. RR+ /\ d e. ( 1 ... ( \|_ ` A ) ) ) -> ( A x. ( 1 / d ) ) e. CC )
101	14 100 83	fsumsub	\|- ( A e. RR+ -> sum_ d e. ( 1 ... ( \|_ ` A ) ) ( ( A x. ( 1 / d ) ) - 1 ) = ( sum_ d e. ( 1 ... ( \|_ ` A ) ) ( A x. ( 1 / d ) ) - sum_ d e. ( 1 ... ( \|_ ` A ) ) 1 ) )
102	99 101	eqtr4d	\|- ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) - ( \|_ ` A ) ) = sum_ d e. ( 1 ... ( \|_ ` A ) ) ( ( A x. ( 1 / d ) ) - 1 ) )
103		eqid	\|- ( ZZ>= ` 1 ) = ( ZZ>= ` 1 )
104	103	uztrn2	\|- ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) -> n e. ( ZZ>= ` 1 ) )
105	104	adantl	\|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> n e. ( ZZ>= ` 1 ) )
106	105	biantrurd	\|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( \|_ ` A ) e. ( ZZ>= ` n ) <-> ( n e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) )
107		uzss	\|- ( n e. ( ZZ>= ` d ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` d ) )
108	107	ad2antll	\|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` d ) )
109	108	sseld	\|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( \|_ ` A ) e. ( ZZ>= ` n ) -> ( \|_ ` A ) e. ( ZZ>= ` d ) ) )
110	109	pm4.71rd	\|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( \|_ ` A ) e. ( ZZ>= ` n ) <-> ( ( \|_ ` A ) e. ( ZZ>= ` d ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) )
111	106 110	bitr3d	\|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( n e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) <-> ( ( \|_ ` A ) e. ( ZZ>= ` d ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) )
112	111	pm5.32da	\|- ( A e. RR+ -> ( ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( ( \|_ ` A ) e. ( ZZ>= ` d ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) ) )
113		ancom	\|- ( ( ( n e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) )
114		an4	\|- ( ( ( d e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` d ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( ( \|_ ` A ) e. ( ZZ>= ` d ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) )
115	112 113 114	3bitr4g	\|- ( A e. RR+ -> ( ( ( n e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` d ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) ) )
116		elfzuzb	\|- ( n e. ( 1 ... ( \|_ ` A ) ) <-> ( n e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) )
117		elfzuzb	\|- ( d e. ( 1 ... n ) <-> ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) )
118	116 117	anbi12i	\|- ( ( n e. ( 1 ... ( \|_ ` A ) ) /\ d e. ( 1 ... n ) ) <-> ( ( n e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) )
119		elfzuzb	\|- ( d e. ( 1 ... ( \|_ ` A ) ) <-> ( d e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` d ) ) )
120		elfzuzb	\|- ( n e. ( d ... ( \|_ ` A ) ) <-> ( n e. ( ZZ>= ` d ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) )
121	119 120	anbi12i	\|- ( ( d e. ( 1 ... ( \|_ ` A ) ) /\ n e. ( d ... ( \|_ ` A ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ ( \|_ ` A ) e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` d ) /\ ( \|_ ` A ) e. ( ZZ>= ` n ) ) ) )
122	115 118 121	3bitr4g	\|- ( A e. RR+ -> ( ( n e. ( 1 ... ( \|_ ` A ) ) /\ d e. ( 1 ... n ) ) <-> ( d e. ( 1 ... ( \|_ ` A ) ) /\ n e. ( d ... ( \|_ ` A ) ) ) ) )
123	18	recnd	\|- ( ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) /\ d e. ( 1 ... n ) ) -> ( 1 / d ) e. CC )
124	123	anasss	\|- ( ( A e. RR+ /\ ( n e. ( 1 ... ( \|_ ` A ) ) /\ d e. ( 1 ... n ) ) ) -> ( 1 / d ) e. CC )
125	14 14 15 122 124	fsumcom2	\|- ( A e. RR+ -> sum_ n e. ( 1 ... ( \|_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) = sum_ d e. ( 1 ... ( \|_ ` A ) ) sum_ n e. ( d ... ( \|_ ` A ) ) ( 1 / d ) )
126	89 102 125	3brtr4d	\|- ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( \|_ ` A ) ) ( 1 / d ) ) - ( \|_ ` A ) ) <_ sum_ n e. ( 1 ... ( \|_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) )
127	13 35 20 43 126	letrd	\|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) <_ sum_ n e. ( 1 ... ( \|_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) )
128	26 34	readdcld	\|- ( A e. RR+ -> ( ( log ` ( ! ` ( \|_ ` A ) ) ) + ( \|_ ` A ) ) e. RR )
129		elfznn	\|- ( n e. ( 1 ... ( \|_ ` A ) ) -> n e. NN )
130	129	adantl	\|- ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) -> n e. NN )
131	130	nnrpd	\|- ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) -> n e. RR+ )
132	131	relogcld	\|- ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) -> ( log ` n ) e. RR )
133		peano2re	\|- ( ( log ` n ) e. RR -> ( ( log ` n ) + 1 ) e. RR )
134	132 133	syl	\|- ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) -> ( ( log ` n ) + 1 ) e. RR )
135		nnz	\|- ( n e. NN -> n e. ZZ )
136		flid	\|- ( n e. ZZ -> ( \|_ ` n ) = n )
137	135 136	syl	\|- ( n e. NN -> ( \|_ ` n ) = n )
138	137	oveq2d	\|- ( n e. NN -> ( 1 ... ( \|_ ` n ) ) = ( 1 ... n ) )
139	138	sumeq1d	\|- ( n e. NN -> sum_ d e. ( 1 ... ( \|_ ` n ) ) ( 1 / d ) = sum_ d e. ( 1 ... n ) ( 1 / d ) )
140		nnre	\|- ( n e. NN -> n e. RR )
141		nnge1	\|- ( n e. NN -> 1 <_ n )
142		harmonicubnd	\|- ( ( n e. RR /\ 1 <_ n ) -> sum_ d e. ( 1 ... ( \|_ ` n ) ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) )
143	140 141 142	syl2anc	\|- ( n e. NN -> sum_ d e. ( 1 ... ( \|_ ` n ) ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) )
144	139 143	eqbrtrrd	\|- ( n e. NN -> sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) )
145	130 144	syl	\|- ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) -> sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) )
146	14 19 134 145	fsumle	\|- ( A e. RR+ -> sum_ n e. ( 1 ... ( \|_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) <_ sum_ n e. ( 1 ... ( \|_ ` A ) ) ( ( log ` n ) + 1 ) )
147	132	recnd	\|- ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) -> ( log ` n ) e. CC )
148		1cnd	\|- ( ( A e. RR+ /\ n e. ( 1 ... ( \|_ ` A ) ) ) -> 1 e. CC )
149	14 147 148	fsumadd	\|- ( A e. RR+ -> sum_ n e. ( 1 ... ( \|_ ` A ) ) ( ( log ` n ) + 1 ) = ( sum_ n e. ( 1 ... ( \|_ ` A ) ) ( log ` n ) + sum_ n e. ( 1 ... ( \|_ ` A ) ) 1 ) )
150		logfac	\|- ( ( \|_ ` A ) e. NN0 -> ( log ` ( ! ` ( \|_ ` A ) ) ) = sum_ n e. ( 1 ... ( \|_ ` A ) ) ( log ` n ) )
151	23 150	syl	\|- ( A e. RR+ -> ( log ` ( ! ` ( \|_ ` A ) ) ) = sum_ n e. ( 1 ... ( \|_ ` A ) ) ( log ` n ) )
152		fsumconst	\|- ( ( ( 1 ... ( \|_ ` A ) ) e. Fin /\ 1 e. CC ) -> sum_ n e. ( 1 ... ( \|_ ` A ) ) 1 = ( ( # ` ( 1 ... ( \|_ ` A ) ) ) x. 1 ) )
153	14 91 152	sylancl	\|- ( A e. RR+ -> sum_ n e. ( 1 ... ( \|_ ` A ) ) 1 = ( ( # ` ( 1 ... ( \|_ ` A ) ) ) x. 1 ) )
154	153 96 97	3eqtrrd	\|- ( A e. RR+ -> ( \|_ ` A ) = sum_ n e. ( 1 ... ( \|_ ` A ) ) 1 )
155	151 154	oveq12d	\|- ( A e. RR+ -> ( ( log ` ( ! ` ( \|_ ` A ) ) ) + ( \|_ ` A ) ) = ( sum_ n e. ( 1 ... ( \|_ ` A ) ) ( log ` n ) + sum_ n e. ( 1 ... ( \|_ ` A ) ) 1 ) )
156	149 155	eqtr4d	\|- ( A e. RR+ -> sum_ n e. ( 1 ... ( \|_ ` A ) ) ( ( log ` n ) + 1 ) = ( ( log ` ( ! ` ( \|_ ` A ) ) ) + ( \|_ ` A ) ) )
157	146 156	breqtrd	\|- ( A e. RR+ -> sum_ n e. ( 1 ... ( \|_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` ( ! ` ( \|_ ` A ) ) ) + ( \|_ ` A ) ) )
158	34 8 26 42	leadd2dd	\|- ( A e. RR+ -> ( ( log ` ( ! ` ( \|_ ` A ) ) ) + ( \|_ ` A ) ) <_ ( ( log ` ( ! ` ( \|_ ` A ) ) ) + A ) )
159	20 128 27 157 158	letrd	\|- ( A e. RR+ -> sum_ n e. ( 1 ... ( \|_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` ( ! ` ( \|_ ` A ) ) ) + A ) )
160	13 20 27 127 159	letrd	\|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) <_ ( ( log ` ( ! ` ( \|_ ` A ) ) ) + A ) )
161	13 8 26	lesubaddd	\|- ( A e. RR+ -> ( ( ( ( A x. ( log ` A ) ) - A ) - A ) <_ ( log ` ( ! ` ( \|_ ` A ) ) ) <-> ( ( A x. ( log ` A ) ) - A ) <_ ( ( log ` ( ! ` ( \|_ ` A ) ) ) + A ) ) )
162	160 161	mpbird	\|- ( A e. RR+ -> ( ( ( A x. ( log ` A ) ) - A ) - A ) <_ ( log ` ( ! ` ( \|_ ` A ) ) ) )
163	12 162	eqbrtrd	\|- ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) <_ ( log ` ( ! ` ( \|_ ` A ) ) ) )

Metamath Proof Explorer

Theorem logfaclbnd

Proof