Description: An integer greater than 1 to the power of a negative integer is in the closed-below, open-above interval between 0 and 1. (Contributed by AV, 24-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | expnegico01 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluzelre | |
|
2 | 1 | adantr | |
3 | eluz2nn | |
|
4 | 3 | nnne0d | |
5 | 4 | adantr | |
6 | simpr | |
|
7 | 2 5 6 | 3jca | |
8 | 7 | 3adant3 | |
9 | reexpclz | |
|
10 | 8 9 | syl | |
11 | 0red | |
|
12 | 1 | 3ad2ant1 | |
13 | 4 | 3ad2ant1 | |
14 | simp2 | |
|
15 | 12 13 14 | reexpclzd | |
16 | 3 | nngt0d | |
17 | 16 | 3ad2ant1 | |
18 | expgt0 | |
|
19 | 12 14 17 18 | syl3anc | |
20 | 11 15 19 | ltled | |
21 | 0zd | |
|
22 | eluz2gt1 | |
|
23 | 22 | 3ad2ant1 | |
24 | simp3 | |
|
25 | ltexp2a | |
|
26 | 12 14 21 23 24 25 | syl32anc | |
27 | eluzelcn | |
|
28 | 27 | exp0d | |
29 | 28 | eqcomd | |
30 | 29 | 3ad2ant1 | |
31 | 26 30 | breqtrrd | |
32 | 0re | |
|
33 | 1xr | |
|
34 | 32 33 | pm3.2i | |
35 | elico2 | |
|
36 | 34 35 | mp1i | |
37 | 10 20 31 36 | mpbir3and | |