This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )