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

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 )