Theorem egt2lt3

Description: Euler's constant _e = 2.71828... is bounded by 2 and 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 )