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 m = 1 n 1 m log n
emcl.2 G = n m = 1 n 1 m log n + 1
emcl.3 H = n log 1 + 1 n
emcl.4 T = n 1 n log 1 + 1 n
Assertion emcllem7 γ 1 log 2 1 F : γ 1 G : 1 log 2 γ

Proof

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