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 ) |