Metamath Proof Explorer


Theorem expnegico01

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 B2NN<0BN01

Proof

Step Hyp Ref Expression
1 eluzelre B2B
2 1 adantr B2NB
3 eluz2nn B2B
4 3 nnne0d B2B0
5 4 adantr B2NB0
6 simpr B2NN
7 2 5 6 3jca B2NBB0N
8 7 3adant3 B2NN<0BB0N
9 reexpclz BB0NBN
10 8 9 syl B2NN<0BN
11 0red B2NN<00
12 1 3ad2ant1 B2NN<0B
13 4 3ad2ant1 B2NN<0B0
14 simp2 B2NN<0N
15 12 13 14 reexpclzd B2NN<0BN
16 3 nngt0d B20<B
17 16 3ad2ant1 B2NN<00<B
18 expgt0 BN0<B0<BN
19 12 14 17 18 syl3anc B2NN<00<BN
20 11 15 19 ltled B2NN<00BN
21 0zd B2NN<00
22 eluz2gt1 B21<B
23 22 3ad2ant1 B2NN<01<B
24 simp3 B2NN<0N<0
25 ltexp2a BN01<BN<0BN<B0
26 12 14 21 23 24 25 syl32anc B2NN<0BN<B0
27 eluzelcn B2B
28 27 exp0d B2B0=1
29 28 eqcomd B21=B0
30 29 3ad2ant1 B2NN<01=B0
31 26 30 breqtrrd B2NN<0BN<1
32 0re 0
33 1xr 1*
34 32 33 pm3.2i 01*
35 elico2 01*BN01BN0BNBN<1
36 34 35 mp1i B2NN<0BN01BN0BNBN<1
37 10 20 31 36 mpbir3and B2NN<0BN01