Theorem emcllem7

Description: Lemma for emcl and harmonicbnd . Derive bounds on gamma as F ( 1 ) and G ( 1 ) . (Contributed by Mario Carneiro, 11-Jul-2014) (Revised by Mario Carneiro, 9-Apr-2016)

	Ref	Expression
Hypotheses	emcl.1	|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )
	emcl.2	|- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )
	emcl.3	|- H = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )
	emcl.4	|- T = ( n e. NN |-> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )
Assertion	emcllem7	|- ( gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 ) /\ F : NN --> ( gamma [,] 1 ) /\ G : NN --> ( ( 1 - ( log ` 2 ) ) [,] gamma ) )

Proof

Step	Hyp	Ref	Expression
1		emcl.1	|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )
2		emcl.2	|- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )
3		emcl.3	|- H = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )
4		emcl.4	|- T = ( n e. NN |-> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )
5		nnuz	|- NN = ( ZZ>= ` 1 )
6		1zzd	|- ( T. -> 1 e. ZZ )
7	1 2 3 4	emcllem6	|- ( F ~~> gamma /\ G ~~> gamma )
8	7	simpri	|- G ~~> gamma
9	8	a1i	|- ( T. -> G ~~> gamma )
10	1 2	emcllem1	|- ( F : NN --> RR /\ G : NN --> RR )
11	10	simpri	|- G : NN --> RR
12	11	ffvelcdmi	|- ( k e. NN -> ( G ` k ) e. RR )
13	12	adantl	|- ( ( T. /\ k e. NN ) -> ( G ` k ) e. RR )
14	5 6 9 13	climrecl	|- ( T. -> gamma e. RR )
15		1nn	|- 1 e. NN
16		simpr	|- ( ( T. /\ i e. NN ) -> i e. NN )
17	8	a1i	|- ( ( T. /\ i e. NN ) -> G ~~> gamma )
18	12	adantl	|- ( ( ( T. /\ i e. NN ) /\ k e. NN ) -> ( G ` k ) e. RR )
19	1 2	emcllem2	|- ( k e. NN -> ( ( F ` ( k + 1 ) ) <_ ( F ` k ) /\ ( G ` k ) <_ ( G ` ( k + 1 ) ) ) )
20	19	simprd	|- ( k e. NN -> ( G ` k ) <_ ( G ` ( k + 1 ) ) )
21	20	adantl	|- ( ( ( T. /\ i e. NN ) /\ k e. NN ) -> ( G ` k ) <_ ( G ` ( k + 1 ) ) )
22	5 16 17 18 21	climub	|- ( ( T. /\ i e. NN ) -> ( G ` i ) <_ gamma )
23	22	ralrimiva	|- ( T. -> A. i e. NN ( G ` i ) <_ gamma )
24		fveq2	|- ( i = 1 -> ( G ` i ) = ( G ` 1 ) )
25		oveq2	|- ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
26	25	sumeq1d	|- ( n = 1 -> sum_ m e. ( 1 ... n ) ( 1 / m ) = sum_ m e. ( 1 ... 1 ) ( 1 / m ) )
27		1z	|- 1 e. ZZ
28		ax-1cn	|- 1 e. CC
29		oveq2	|- ( m = 1 -> ( 1 / m ) = ( 1 / 1 ) )
30		1div1e1	|- ( 1 / 1 ) = 1
31	29 30	eqtrdi	|- ( m = 1 -> ( 1 / m ) = 1 )
32	31	fsum1	|- ( ( 1 e. ZZ /\ 1 e. CC ) -> sum_ m e. ( 1 ... 1 ) ( 1 / m ) = 1 )
33	27 28 32	mp2an	|- sum_ m e. ( 1 ... 1 ) ( 1 / m ) = 1
34	26 33	eqtrdi	|- ( n = 1 -> sum_ m e. ( 1 ... n ) ( 1 / m ) = 1 )
35		oveq1	|- ( n = 1 -> ( n + 1 ) = ( 1 + 1 ) )
36		df-2	|- 2 = ( 1 + 1 )
37	35 36	eqtr4di	|- ( n = 1 -> ( n + 1 ) = 2 )
38	37	fveq2d	|- ( n = 1 -> ( log ` ( n + 1 ) ) = ( log ` 2 ) )
39	34 38	oveq12d	|- ( n = 1 -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) = ( 1 - ( log ` 2 ) ) )
40		1re	|- 1 e. RR
41		2rp	|- 2 e. RR+
42		relogcl	|- ( 2 e. RR+ -> ( log ` 2 ) e. RR )
43	41 42	ax-mp	|- ( log ` 2 ) e. RR
44	40 43	resubcli	|- ( 1 - ( log ` 2 ) ) e. RR
45	44	elexi	|- ( 1 - ( log ` 2 ) ) e. _V
46	39 2 45	fvmpt	|- ( 1 e. NN -> ( G ` 1 ) = ( 1 - ( log ` 2 ) ) )
47	15 46	ax-mp	|- ( G ` 1 ) = ( 1 - ( log ` 2 ) )
48	24 47	eqtrdi	|- ( i = 1 -> ( G ` i ) = ( 1 - ( log ` 2 ) ) )
49	48	breq1d	|- ( i = 1 -> ( ( G ` i ) <_ gamma <-> ( 1 - ( log ` 2 ) ) <_ gamma ) )
50	49	rspcva	|- ( ( 1 e. NN /\ A. i e. NN ( G ` i ) <_ gamma ) -> ( 1 - ( log ` 2 ) ) <_ gamma )
51	15 23 50	sylancr	|- ( T. -> ( 1 - ( log ` 2 ) ) <_ gamma )
52		fveq2	|- ( x = i -> ( F ` x ) = ( F ` i ) )
53	52	negeqd	|- ( x = i -> -u ( F ` x ) = -u ( F ` i ) )
54		eqid	|- ( x e. NN |-> -u ( F ` x ) ) = ( x e. NN |-> -u ( F ` x ) )
55		negex	|- -u ( F ` i ) e. _V
56	53 54 55	fvmpt	|- ( i e. NN -> ( ( x e. NN |-> -u ( F ` x ) ) ` i ) = -u ( F ` i ) )
57	56	adantl	|- ( ( T. /\ i e. NN ) -> ( ( x e. NN |-> -u ( F ` x ) ) ` i ) = -u ( F ` i ) )
58	7	simpli	|- F ~~> gamma
59	58	a1i	|- ( T. -> F ~~> gamma )
60		0cnd	|- ( T. -> 0 e. CC )
61		nnex	|- NN e. _V
62	61	mptex	|- ( x e. NN |-> -u ( F ` x ) ) e. _V
63	62	a1i	|- ( T. -> ( x e. NN |-> -u ( F ` x ) ) e. _V )
64	10	simpli	|- F : NN --> RR
65	64	ffvelcdmi	|- ( k e. NN -> ( F ` k ) e. RR )
66	65	adantl	|- ( ( T. /\ k e. NN ) -> ( F ` k ) e. RR )
67	66	recnd	|- ( ( T. /\ k e. NN ) -> ( F ` k ) e. CC )
68		fveq2	|- ( x = k -> ( F ` x ) = ( F ` k ) )
69	68	negeqd	|- ( x = k -> -u ( F ` x ) = -u ( F ` k ) )
70		negex	|- -u ( F ` k ) e. _V
71	69 54 70	fvmpt	|- ( k e. NN -> ( ( x e. NN |-> -u ( F ` x ) ) ` k ) = -u ( F ` k ) )
72	71	adantl	|- ( ( T. /\ k e. NN ) -> ( ( x e. NN |-> -u ( F ` x ) ) ` k ) = -u ( F ` k ) )
73		df-neg	|- -u ( F ` k ) = ( 0 - ( F ` k ) )
74	72 73	eqtrdi	|- ( ( T. /\ k e. NN ) -> ( ( x e. NN |-> -u ( F ` x ) ) ` k ) = ( 0 - ( F ` k ) ) )
75	5 6 59 60 63 67 74	climsubc2	|- ( T. -> ( x e. NN |-> -u ( F ` x ) ) ~~> ( 0 - gamma ) )
76	75	adantr	|- ( ( T. /\ i e. NN ) -> ( x e. NN |-> -u ( F ` x ) ) ~~> ( 0 - gamma ) )
77	66	renegcld	|- ( ( T. /\ k e. NN ) -> -u ( F ` k ) e. RR )
78	72 77	eqeltrd	|- ( ( T. /\ k e. NN ) -> ( ( x e. NN |-> -u ( F ` x ) ) ` k ) e. RR )
79	78	adantlr	|- ( ( ( T. /\ i e. NN ) /\ k e. NN ) -> ( ( x e. NN |-> -u ( F ` x ) ) ` k ) e. RR )
80	19	simpld	|- ( k e. NN -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
81	80	adantl	|- ( ( T. /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
82		peano2nn	|- ( k e. NN -> ( k + 1 ) e. NN )
83	82	adantl	|- ( ( T. /\ k e. NN ) -> ( k + 1 ) e. NN )
84	64	ffvelcdmi	|- ( ( k + 1 ) e. NN -> ( F ` ( k + 1 ) ) e. RR )
85	83 84	syl	|- ( ( T. /\ k e. NN ) -> ( F ` ( k + 1 ) ) e. RR )
86	85 66	lenegd	|- ( ( T. /\ k e. NN ) -> ( ( F ` ( k + 1 ) ) <_ ( F ` k ) <-> -u ( F ` k ) <_ -u ( F ` ( k + 1 ) ) ) )
87	81 86	mpbid	|- ( ( T. /\ k e. NN ) -> -u ( F ` k ) <_ -u ( F ` ( k + 1 ) ) )
88		fveq2	|- ( x = ( k + 1 ) -> ( F ` x ) = ( F ` ( k + 1 ) ) )
89	88	negeqd	|- ( x = ( k + 1 ) -> -u ( F ` x ) = -u ( F ` ( k + 1 ) ) )
90		negex	|- -u ( F ` ( k + 1 ) ) e. _V
91	89 54 90	fvmpt	|- ( ( k + 1 ) e. NN -> ( ( x e. NN |-> -u ( F ` x ) ) ` ( k + 1 ) ) = -u ( F ` ( k + 1 ) ) )
92	83 91	syl	|- ( ( T. /\ k e. NN ) -> ( ( x e. NN |-> -u ( F ` x ) ) ` ( k + 1 ) ) = -u ( F ` ( k + 1 ) ) )
93	87 72 92	3brtr4d	|- ( ( T. /\ k e. NN ) -> ( ( x e. NN |-> -u ( F ` x ) ) ` k ) <_ ( ( x e. NN |-> -u ( F ` x ) ) ` ( k + 1 ) ) )
94	93	adantlr	|- ( ( ( T. /\ i e. NN ) /\ k e. NN ) -> ( ( x e. NN |-> -u ( F ` x ) ) ` k ) <_ ( ( x e. NN |-> -u ( F ` x ) ) ` ( k + 1 ) ) )
95	5 16 76 79 94	climub	|- ( ( T. /\ i e. NN ) -> ( ( x e. NN |-> -u ( F ` x ) ) ` i ) <_ ( 0 - gamma ) )
96	57 95	eqbrtrrd	|- ( ( T. /\ i e. NN ) -> -u ( F ` i ) <_ ( 0 - gamma ) )
97		df-neg	|- -u gamma = ( 0 - gamma )
98	96 97	breqtrrdi	|- ( ( T. /\ i e. NN ) -> -u ( F ` i ) <_ -u gamma )
99	14	mptru	|- gamma e. RR
100	64	ffvelcdmi	|- ( i e. NN -> ( F ` i ) e. RR )
101	100	adantl	|- ( ( T. /\ i e. NN ) -> ( F ` i ) e. RR )
102		leneg	|- ( ( gamma e. RR /\ ( F ` i ) e. RR ) -> ( gamma <_ ( F ` i ) <-> -u ( F ` i ) <_ -u gamma ) )
103	99 101 102	sylancr	|- ( ( T. /\ i e. NN ) -> ( gamma <_ ( F ` i ) <-> -u ( F ` i ) <_ -u gamma ) )
104	98 103	mpbird	|- ( ( T. /\ i e. NN ) -> gamma <_ ( F ` i ) )
105	104	ralrimiva	|- ( T. -> A. i e. NN gamma <_ ( F ` i ) )
106		fveq2	|- ( i = 1 -> ( F ` i ) = ( F ` 1 ) )
107		fveq2	|- ( n = 1 -> ( log ` n ) = ( log ` 1 ) )
108		log1	|- ( log ` 1 ) = 0
109	107 108	eqtrdi	|- ( n = 1 -> ( log ` n ) = 0 )
110	34 109	oveq12d	|- ( n = 1 -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) = ( 1 - 0 ) )
111		1m0e1	|- ( 1 - 0 ) = 1
112	110 111	eqtrdi	|- ( n = 1 -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) = 1 )
113	40	elexi	|- 1 e. _V
114	112 1 113	fvmpt	|- ( 1 e. NN -> ( F ` 1 ) = 1 )
115	15 114	ax-mp	|- ( F ` 1 ) = 1
116	106 115	eqtrdi	|- ( i = 1 -> ( F ` i ) = 1 )
117	116	breq2d	|- ( i = 1 -> ( gamma <_ ( F ` i ) <-> gamma <_ 1 ) )
118	117	rspcva	|- ( ( 1 e. NN /\ A. i e. NN gamma <_ ( F ` i ) ) -> gamma <_ 1 )
119	15 105 118	sylancr	|- ( T. -> gamma <_ 1 )
120	44 40	elicc2i	|- ( gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 ) <-> ( gamma e. RR /\ ( 1 - ( log ` 2 ) ) <_ gamma /\ gamma <_ 1 ) )
121	14 51 119 120	syl3anbrc	|- ( T. -> gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 ) )
122		ffn	|- ( F : NN --> RR -> F Fn NN )
123	64 122	mp1i	|- ( T. -> F Fn NN )
124	16 5	eleqtrdi	|- ( ( T. /\ i e. NN ) -> i e. ( ZZ>= ` 1 ) )
125		elfznn	|- ( k e. ( 1 ... i ) -> k e. NN )
126	125	adantl	|- ( ( ( T. /\ i e. NN ) /\ k e. ( 1 ... i ) ) -> k e. NN )
127	126 65	syl	|- ( ( ( T. /\ i e. NN ) /\ k e. ( 1 ... i ) ) -> ( F ` k ) e. RR )
128		elfznn	|- ( k e. ( 1 ... ( i - 1 ) ) -> k e. NN )
129	128	adantl	|- ( ( ( T. /\ i e. NN ) /\ k e. ( 1 ... ( i - 1 ) ) ) -> k e. NN )
130	129 80	syl	|- ( ( ( T. /\ i e. NN ) /\ k e. ( 1 ... ( i - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
131	124 127 130	monoord2	|- ( ( T. /\ i e. NN ) -> ( F ` i ) <_ ( F ` 1 ) )
132	131 115	breqtrdi	|- ( ( T. /\ i e. NN ) -> ( F ` i ) <_ 1 )
133	99 40	elicc2i	|- ( ( F ` i ) e. ( gamma [,] 1 ) <-> ( ( F ` i ) e. RR /\ gamma <_ ( F ` i ) /\ ( F ` i ) <_ 1 ) )
134	101 104 132 133	syl3anbrc	|- ( ( T. /\ i e. NN ) -> ( F ` i ) e. ( gamma [,] 1 ) )
135	134	ralrimiva	|- ( T. -> A. i e. NN ( F ` i ) e. ( gamma [,] 1 ) )
136		ffnfv	|- ( F : NN --> ( gamma [,] 1 ) <-> ( F Fn NN /\ A. i e. NN ( F ` i ) e. ( gamma [,] 1 ) ) )
137	123 135 136	sylanbrc	|- ( T. -> F : NN --> ( gamma [,] 1 ) )
138		ffn	|- ( G : NN --> RR -> G Fn NN )
139	11 138	mp1i	|- ( T. -> G Fn NN )
140	11	ffvelcdmi	|- ( i e. NN -> ( G ` i ) e. RR )
141	140	adantl	|- ( ( T. /\ i e. NN ) -> ( G ` i ) e. RR )
142	126 12	syl	|- ( ( ( T. /\ i e. NN ) /\ k e. ( 1 ... i ) ) -> ( G ` k ) e. RR )
143	129 20	syl	|- ( ( ( T. /\ i e. NN ) /\ k e. ( 1 ... ( i - 1 ) ) ) -> ( G ` k ) <_ ( G ` ( k + 1 ) ) )
144	124 142 143	monoord	|- ( ( T. /\ i e. NN ) -> ( G ` 1 ) <_ ( G ` i ) )
145	47 144	eqbrtrrid	|- ( ( T. /\ i e. NN ) -> ( 1 - ( log ` 2 ) ) <_ ( G ` i ) )
146	44 99	elicc2i	|- ( ( G ` i ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) <-> ( ( G ` i ) e. RR /\ ( 1 - ( log ` 2 ) ) <_ ( G ` i ) /\ ( G ` i ) <_ gamma ) )
147	141 145 22 146	syl3anbrc	|- ( ( T. /\ i e. NN ) -> ( G ` i ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) )
148	147	ralrimiva	|- ( T. -> A. i e. NN ( G ` i ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) )
149		ffnfv	|- ( G : NN --> ( ( 1 - ( log ` 2 ) ) [,] gamma ) <-> ( G Fn NN /\ A. i e. NN ( G ` i ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) ) )
150	139 148 149	sylanbrc	|- ( T. -> G : NN --> ( ( 1 - ( log ` 2 ) ) [,] gamma ) )
151	121 137 150	3jca	|- ( T. -> ( gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 ) /\ F : NN --> ( gamma [,] 1 ) /\ G : NN --> ( ( 1 - ( log ` 2 ) ) [,] gamma ) ) )
152	151	mptru	|- ( gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 ) /\ F : NN --> ( gamma [,] 1 ) /\ G : NN --> ( ( 1 - ( log ` 2 ) ) [,] gamma ) )