Metamath Proof Explorer

Theorem ege2le3

Description: Lemma for egt2lt3 . (Contributed by NM, 20-Mar-2005) (Proof shortened by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypotheses erelem1.1 
|- F = ( n e. NN |-> ( 2 x. ( ( 1 / 2 ) ^ n ) ) )
erelem1.2 
|- G = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
Assertion ege2le3 
|- ( 2 <_ _e /\ _e <_ 3 )

Proof

Step Hyp Ref Expression
1 erelem1.1 
 |-  F = ( n e. NN |-> ( 2 x. ( ( 1 / 2 ) ^ n ) ) )
2 erelem1.2 
 |-  G = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
3 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
4 0nn0 
 |-  0 e. NN0
5 4 a1i 
 |-  ( T. -> 0 e. NN0 )
6 1e0p1 
 |-  1 = ( 0 + 1 )
7 0z 
 |-  0 e. ZZ
8 fveq2 
 |-  ( n = 0 -> ( ! ` n ) = ( ! ` 0 ) )
9 fac0 
 |-  ( ! ` 0 ) = 1
10 8 9 eqtrdi 
 |-  ( n = 0 -> ( ! ` n ) = 1 )
11 10 oveq2d 
 |-  ( n = 0 -> ( 1 / ( ! ` n ) ) = ( 1 / 1 ) )
12 ax-1cn 
 |-  1 e. CC
13 12 div1i 
 |-  ( 1 / 1 ) = 1
14 11 13 eqtrdi 
 |-  ( n = 0 -> ( 1 / ( ! ` n ) ) = 1 )
15 1ex 
 |-  1 e. _V
16 14 2 15 fvmpt 
 |-  ( 0 e. NN0 -> ( G ` 0 ) = 1 )
17 4 16 mp1i 
 |-  ( T. -> ( G ` 0 ) = 1 )
18 7 17 seq1i 
 |-  ( T. -> ( seq 0 ( + , G ) ` 0 ) = 1 )
19 1nn0 
 |-  1 e. NN0
20 fveq2 
 |-  ( n = 1 -> ( ! ` n ) = ( ! ` 1 ) )
21 fac1 
 |-  ( ! ` 1 ) = 1
22 20 21 eqtrdi 
 |-  ( n = 1 -> ( ! ` n ) = 1 )
23 22 oveq2d 
 |-  ( n = 1 -> ( 1 / ( ! ` n ) ) = ( 1 / 1 ) )
24 23 13 eqtrdi 
 |-  ( n = 1 -> ( 1 / ( ! ` n ) ) = 1 )
25 24 2 15 fvmpt 
 |-  ( 1 e. NN0 -> ( G ` 1 ) = 1 )
26 19 25 mp1i 
 |-  ( T. -> ( G ` 1 ) = 1 )
27 3 5 6 18 26 seqp1d 
 |-  ( T. -> ( seq 0 ( + , G ) ` 1 ) = ( 1 + 1 ) )
28 df-2 
 |-  2 = ( 1 + 1 )
29 27 28 eqtr4di 
 |-  ( T. -> ( seq 0 ( + , G ) ` 1 ) = 2 )
30 19 a1i 
 |-  ( T. -> 1 e. NN0 )
31 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
32 1exp 
 |-  ( n e. ZZ -> ( 1 ^ n ) = 1 )
33 31 32 syl 
 |-  ( n e. NN0 -> ( 1 ^ n ) = 1 )
34 33 oveq1d 
 |-  ( n e. NN0 -> ( ( 1 ^ n ) / ( ! ` n ) ) = ( 1 / ( ! ` n ) ) )
35 34 mpteq2ia 
 |-  ( n e. NN0 |-> ( ( 1 ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
36 2 35 eqtr4i 
 |-  G = ( n e. NN0 |-> ( ( 1 ^ n ) / ( ! ` n ) ) )
37 36 efcvg 
 |-  ( 1 e. CC -> seq 0 ( + , G ) ~~> ( exp ` 1 ) )
38 12 37 mp1i 
 |-  ( T. -> seq 0 ( + , G ) ~~> ( exp ` 1 ) )
39 df-e 
 |-  _e = ( exp ` 1 )
40 38 39 breqtrrdi 
 |-  ( T. -> seq 0 ( + , G ) ~~> _e )
41 fveq2 
 |-  ( n = k -> ( ! ` n ) = ( ! ` k ) )
42 41 oveq2d 
 |-  ( n = k -> ( 1 / ( ! ` n ) ) = ( 1 / ( ! ` k ) ) )
43 ovex 
 |-  ( 1 / ( ! ` k ) ) e. _V
44 42 2 43 fvmpt 
 |-  ( k e. NN0 -> ( G ` k ) = ( 1 / ( ! ` k ) ) )
45 44 adantl 
 |-  ( ( T. /\ k e. NN0 ) -> ( G ` k ) = ( 1 / ( ! ` k ) ) )
46 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
47 46 adantl 
 |-  ( ( T. /\ k e. NN0 ) -> ( ! ` k ) e. NN )
48 47 nnrecred 
 |-  ( ( T. /\ k e. NN0 ) -> ( 1 / ( ! ` k ) ) e. RR )
49 45 48 eqeltrd 
 |-  ( ( T. /\ k e. NN0 ) -> ( G ` k ) e. RR )
50 47 nnred 
 |-  ( ( T. /\ k e. NN0 ) -> ( ! ` k ) e. RR )
51 47 nngt0d 
 |-  ( ( T. /\ k e. NN0 ) -> 0 < ( ! ` k ) )
52 1re 
 |-  1 e. RR
53 0le1 
 |-  0 <_ 1
54 divge0 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( ! ` k ) e. RR /\ 0 < ( ! ` k ) ) ) -> 0 <_ ( 1 / ( ! ` k ) ) )
55 52 53 54 mpanl12 
 |-  ( ( ( ! ` k ) e. RR /\ 0 < ( ! ` k ) ) -> 0 <_ ( 1 / ( ! ` k ) ) )
56 50 51 55 syl2anc 
 |-  ( ( T. /\ k e. NN0 ) -> 0 <_ ( 1 / ( ! ` k ) ) )
57 56 45 breqtrrd 
 |-  ( ( T. /\ k e. NN0 ) -> 0 <_ ( G ` k ) )
58 3 30 40 49 57 climserle 
 |-  ( T. -> ( seq 0 ( + , G ) ` 1 ) <_ _e )
59 29 58 eqbrtrrd 
 |-  ( T. -> 2 <_ _e )
60 59 mptru 
 |-  2 <_ _e
61 nnuz 
 |-  NN = ( ZZ>= ` 1 )
62 1zzd 
 |-  ( T. -> 1 e. ZZ )
63 49 recnd 
 |-  ( ( T. /\ k e. NN0 ) -> ( G ` k ) e. CC )
64 3 5 63 40 clim2ser 
 |-  ( T. -> seq ( 0 + 1 ) ( + , G ) ~~> ( _e - ( seq 0 ( + , G ) ` 0 ) ) )
65 0p1e1 
 |-  ( 0 + 1 ) = 1
66 seqeq1 
 |-  ( ( 0 + 1 ) = 1 -> seq ( 0 + 1 ) ( + , G ) = seq 1 ( + , G ) )
67 65 66 ax-mp 
 |-  seq ( 0 + 1 ) ( + , G ) = seq 1 ( + , G )
68 18 mptru 
 |-  ( seq 0 ( + , G ) ` 0 ) = 1
69 68 oveq2i 
 |-  ( _e - ( seq 0 ( + , G ) ` 0 ) ) = ( _e - 1 )
70 64 67 69 3brtr3g 
 |-  ( T. -> seq 1 ( + , G ) ~~> ( _e - 1 ) )
71 2cnd 
 |-  ( T. -> 2 e. CC )
72 oveq2 
 |-  ( n = k -> ( ( 1 / 2 ) ^ n ) = ( ( 1 / 2 ) ^ k ) )
73 eqid 
 |-  ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) = ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) )
74 ovex 
 |-  ( ( 1 / 2 ) ^ k ) e. _V
75 72 73 74 fvmpt 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` k ) = ( ( 1 / 2 ) ^ k ) )
76 75 adantl 
 |-  ( ( T. /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` k ) = ( ( 1 / 2 ) ^ k ) )
77 halfre 
 |-  ( 1 / 2 ) e. RR
78 simpr 
 |-  ( ( T. /\ k e. NN0 ) -> k e. NN0 )
79 reexpcl 
 |-  ( ( ( 1 / 2 ) e. RR /\ k e. NN0 ) -> ( ( 1 / 2 ) ^ k ) e. RR )
80 77 78 79 sylancr 
 |-  ( ( T. /\ k e. NN0 ) -> ( ( 1 / 2 ) ^ k ) e. RR )
81 80 recnd 
 |-  ( ( T. /\ k e. NN0 ) -> ( ( 1 / 2 ) ^ k ) e. CC )
82 76 81 eqeltrd 
 |-  ( ( T. /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` k ) e. CC )
83 1lt2 
 |-  1 < 2
84 2re 
 |-  2 e. RR
85 0le2 
 |-  0 <_ 2
86 absid 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 )
87 84 85 86 mp2an 
 |-  ( abs ` 2 ) = 2
88 83 87 breqtrri 
 |-  1 < ( abs ` 2 )
89 88 a1i 
 |-  ( T. -> 1 < ( abs ` 2 ) )
90 71 89 76 georeclim 
 |-  ( T. -> seq 0 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) ~~> ( 2 / ( 2 - 1 ) ) )
91 2m1e1 
 |-  ( 2 - 1 ) = 1
92 91 oveq2i 
 |-  ( 2 / ( 2 - 1 ) ) = ( 2 / 1 )
93 2cn 
 |-  2 e. CC
94 93 div1i 
 |-  ( 2 / 1 ) = 2
95 92 94 eqtri 
 |-  ( 2 / ( 2 - 1 ) ) = 2
96 90 95 breqtrdi 
 |-  ( T. -> seq 0 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) ~~> 2 )
97 3 5 82 96 clim2ser 
 |-  ( T. -> seq ( 0 + 1 ) ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) ~~> ( 2 - ( seq 0 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) ` 0 ) ) )
98 seqeq1 
 |-  ( ( 0 + 1 ) = 1 -> seq ( 0 + 1 ) ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) = seq 1 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) )
99 65 98 ax-mp 
 |-  seq ( 0 + 1 ) ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) = seq 1 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) )
100 oveq2 
 |-  ( n = 0 -> ( ( 1 / 2 ) ^ n ) = ( ( 1 / 2 ) ^ 0 ) )
101 ovex 
 |-  ( ( 1 / 2 ) ^ 0 ) e. _V
102 100 73 101 fvmpt 
 |-  ( 0 e. NN0 -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` 0 ) = ( ( 1 / 2 ) ^ 0 ) )
103 4 102 ax-mp 
 |-  ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` 0 ) = ( ( 1 / 2 ) ^ 0 )
104 halfcn 
 |-  ( 1 / 2 ) e. CC
105 exp0 
 |-  ( ( 1 / 2 ) e. CC -> ( ( 1 / 2 ) ^ 0 ) = 1 )
106 104 105 ax-mp 
 |-  ( ( 1 / 2 ) ^ 0 ) = 1
107 103 106 eqtri 
 |-  ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` 0 ) = 1
108 107 a1i 
 |-  ( T. -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` 0 ) = 1 )
109 7 108 seq1i 
 |-  ( T. -> ( seq 0 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) ` 0 ) = 1 )
110 109 mptru 
 |-  ( seq 0 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) ` 0 ) = 1
111 110 oveq2i 
 |-  ( 2 - ( seq 0 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) ` 0 ) ) = ( 2 - 1 )
112 111 91 eqtri 
 |-  ( 2 - ( seq 0 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) ` 0 ) ) = 1
113 97 99 112 3brtr3g 
 |-  ( T. -> seq 1 ( + , ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ) ~~> 1 )
114 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
115 114 82 sylan2 
 |-  ( ( T. /\ k e. NN ) -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` k ) e. CC )
116 72 oveq2d 
 |-  ( n = k -> ( 2 x. ( ( 1 / 2 ) ^ n ) ) = ( 2 x. ( ( 1 / 2 ) ^ k ) ) )
117 ovex 
 |-  ( 2 x. ( ( 1 / 2 ) ^ k ) ) e. _V
118 116 1 117 fvmpt 
 |-  ( k e. NN -> ( F ` k ) = ( 2 x. ( ( 1 / 2 ) ^ k ) ) )
119 118 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) = ( 2 x. ( ( 1 / 2 ) ^ k ) ) )
120 114 76 sylan2 
 |-  ( ( T. /\ k e. NN ) -> ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` k ) = ( ( 1 / 2 ) ^ k ) )
121 120 oveq2d 
 |-  ( ( T. /\ k e. NN ) -> ( 2 x. ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` k ) ) = ( 2 x. ( ( 1 / 2 ) ^ k ) ) )
122 119 121 eqtr4d 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) = ( 2 x. ( ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ` k ) ) )
123 61 62 71 113 115 122 isermulc2 
 |-  ( T. -> seq 1 ( + , F ) ~~> ( 2 x. 1 ) )
124 2t1e2 
 |-  ( 2 x. 1 ) = 2
125 123 124 breqtrdi 
 |-  ( T. -> seq 1 ( + , F ) ~~> 2 )
126 114 49 sylan2 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. RR )
127 remulcl 
 |-  ( ( 2 e. RR /\ ( ( 1 / 2 ) ^ k ) e. RR ) -> ( 2 x. ( ( 1 / 2 ) ^ k ) ) e. RR )
128 84 80 127 sylancr 
 |-  ( ( T. /\ k e. NN0 ) -> ( 2 x. ( ( 1 / 2 ) ^ k ) ) e. RR )
129 114 128 sylan2 
 |-  ( ( T. /\ k e. NN ) -> ( 2 x. ( ( 1 / 2 ) ^ k ) ) e. RR )
130 119 129 eqeltrd 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) e. RR )
131 faclbnd2 
 |-  ( k e. NN0 -> ( ( 2 ^ k ) / 2 ) <_ ( ! ` k ) )
132 131 adantl 
 |-  ( ( T. /\ k e. NN0 ) -> ( ( 2 ^ k ) / 2 ) <_ ( ! ` k ) )
133 2nn 
 |-  2 e. NN
134 nnexpcl 
 |-  ( ( 2 e. NN /\ k e. NN0 ) -> ( 2 ^ k ) e. NN )
135 133 78 134 sylancr 
 |-  ( ( T. /\ k e. NN0 ) -> ( 2 ^ k ) e. NN )
136 135 nnrpd 
 |-  ( ( T. /\ k e. NN0 ) -> ( 2 ^ k ) e. RR+ )
137 136 rphalfcld 
 |-  ( ( T. /\ k e. NN0 ) -> ( ( 2 ^ k ) / 2 ) e. RR+ )
138 47 nnrpd 
 |-  ( ( T. /\ k e. NN0 ) -> ( ! ` k ) e. RR+ )
139 137 138 lerecd 
 |-  ( ( T. /\ k e. NN0 ) -> ( ( ( 2 ^ k ) / 2 ) <_ ( ! ` k ) <-> ( 1 / ( ! ` k ) ) <_ ( 1 / ( ( 2 ^ k ) / 2 ) ) ) )
140 132 139 mpbid 
 |-  ( ( T. /\ k e. NN0 ) -> ( 1 / ( ! ` k ) ) <_ ( 1 / ( ( 2 ^ k ) / 2 ) ) )
141 2cnd 
 |-  ( ( T. /\ k e. NN0 ) -> 2 e. CC )
142 135 nncnd 
 |-  ( ( T. /\ k e. NN0 ) -> ( 2 ^ k ) e. CC )
143 135 nnne0d 
 |-  ( ( T. /\ k e. NN0 ) -> ( 2 ^ k ) =/= 0 )
144 141 142 143 divrecd 
 |-  ( ( T. /\ k e. NN0 ) -> ( 2 / ( 2 ^ k ) ) = ( 2 x. ( 1 / ( 2 ^ k ) ) ) )
145 2ne0 
 |-  2 =/= 0
146 recdiv 
 |-  ( ( ( ( 2 ^ k ) e. CC /\ ( 2 ^ k ) =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( 1 / ( ( 2 ^ k ) / 2 ) ) = ( 2 / ( 2 ^ k ) ) )
147 93 145 146 mpanr12 
 |-  ( ( ( 2 ^ k ) e. CC /\ ( 2 ^ k ) =/= 0 ) -> ( 1 / ( ( 2 ^ k ) / 2 ) ) = ( 2 / ( 2 ^ k ) ) )
148 142 143 147 syl2anc 
 |-  ( ( T. /\ k e. NN0 ) -> ( 1 / ( ( 2 ^ k ) / 2 ) ) = ( 2 / ( 2 ^ k ) ) )
149 145 a1i 
 |-  ( ( T. /\ k e. NN0 ) -> 2 =/= 0 )
150 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
151 150 adantl 
 |-  ( ( T. /\ k e. NN0 ) -> k e. ZZ )
152 141 149 151 exprecd 
 |-  ( ( T. /\ k e. NN0 ) -> ( ( 1 / 2 ) ^ k ) = ( 1 / ( 2 ^ k ) ) )
153 152 oveq2d 
 |-  ( ( T. /\ k e. NN0 ) -> ( 2 x. ( ( 1 / 2 ) ^ k ) ) = ( 2 x. ( 1 / ( 2 ^ k ) ) ) )
154 144 148 153 3eqtr4rd 
 |-  ( ( T. /\ k e. NN0 ) -> ( 2 x. ( ( 1 / 2 ) ^ k ) ) = ( 1 / ( ( 2 ^ k ) / 2 ) ) )
155 140 154 breqtrrd 
 |-  ( ( T. /\ k e. NN0 ) -> ( 1 / ( ! ` k ) ) <_ ( 2 x. ( ( 1 / 2 ) ^ k ) ) )
156 114 155 sylan2 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / ( ! ` k ) ) <_ ( 2 x. ( ( 1 / 2 ) ^ k ) ) )
157 114 45 sylan2 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) = ( 1 / ( ! ` k ) ) )
158 156 157 119 3brtr4d 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) <_ ( F ` k ) )
159 61 62 70 125 126 130 158 iserle 
 |-  ( T. -> ( _e - 1 ) <_ 2 )
160 159 mptru 
 |-  ( _e - 1 ) <_ 2
161 ere 
 |-  _e e. RR
162 161 52 84 lesubaddi 
 |-  ( ( _e - 1 ) <_ 2 <-> _e <_ ( 2 + 1 ) )
163 160 162 mpbi 
 |-  _e <_ ( 2 + 1 )
164 df-3 
 |-  3 = ( 2 + 1 )
165 163 164 breqtrri 
 |-  _e <_ 3
166 60 165 pm3.2i 
 |-  ( 2 <_ _e /\ _e <_ 3 )