Metamath Proof Explorer


Theorem egt2lt3

Description: Euler's constant _e = 2.71828... is strictly bounded below by 2 and above by 3. (Contributed by NM, 28-Nov-2008) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Assertion egt2lt3
|- ( 2 < _e /\ _e < 3 )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( n e. NN |-> ( 2 x. ( ( 1 / 2 ) ^ n ) ) ) = ( n e. NN |-> ( 2 x. ( ( 1 / 2 ) ^ n ) ) )
2 eqid
 |-  ( n e. NN0 |-> ( 1 / ( ! ` n ) ) ) = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
3 1 2 ege2le3
 |-  ( 2 <_ _e /\ _e <_ 3 )
4 3 simpli
 |-  2 <_ _e
5 eirr
 |-  _e e/ QQ
6 5 neli
 |-  -. _e e. QQ
7 nnq
 |-  ( _e e. NN -> _e e. QQ )
8 6 7 mto
 |-  -. _e e. NN
9 2nn
 |-  2 e. NN
10 eleq1
 |-  ( _e = 2 -> ( _e e. NN <-> 2 e. NN ) )
11 9 10 mpbiri
 |-  ( _e = 2 -> _e e. NN )
12 11 necon3bi
 |-  ( -. _e e. NN -> _e =/= 2 )
13 8 12 ax-mp
 |-  _e =/= 2
14 2re
 |-  2 e. RR
15 ere
 |-  _e e. RR
16 14 15 ltleni
 |-  ( 2 < _e <-> ( 2 <_ _e /\ _e =/= 2 ) )
17 4 13 16 mpbir2an
 |-  2 < _e
18 3 simpri
 |-  _e <_ 3
19 3nn
 |-  3 e. NN
20 eleq1
 |-  ( 3 = _e -> ( 3 e. NN <-> _e e. NN ) )
21 19 20 mpbii
 |-  ( 3 = _e -> _e e. NN )
22 21 necon3bi
 |-  ( -. _e e. NN -> 3 =/= _e )
23 8 22 ax-mp
 |-  3 =/= _e
24 3re
 |-  3 e. RR
25 15 24 ltleni
 |-  ( _e < 3 <-> ( _e <_ 3 /\ 3 =/= _e ) )
26 18 23 25 mpbir2an
 |-  _e < 3
27 17 26 pm3.2i
 |-  ( 2 < _e /\ _e < 3 )