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 
|- ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> ( B ^ N ) e. ( 0 [,) 1 ) )

Proof

Step Hyp Ref Expression
1 eluzelre 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. RR )
2 1 adantr 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> B e. RR )
3 eluz2nn 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. NN )
4 3 nnne0d 
 |-  ( B e. ( ZZ>= ` 2 ) -> B =/= 0 )
5 4 adantr 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> B =/= 0 )
6 simpr 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> N e. ZZ )
7 2 5 6 3jca 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( B e. RR /\ B =/= 0 /\ N e. ZZ ) )
8 7 3adant3 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> ( B e. RR /\ B =/= 0 /\ N e. ZZ ) )
9 reexpclz 
 |-  ( ( B e. RR /\ B =/= 0 /\ N e. ZZ ) -> ( B ^ N ) e. RR )
10 8 9 syl 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> ( B ^ N ) e. RR )
11 0red 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> 0 e. RR )
12 1 3ad2ant1 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> B e. RR )
13 4 3ad2ant1 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> B =/= 0 )
14 simp2 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> N e. ZZ )
15 12 13 14 reexpclzd 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> ( B ^ N ) e. RR )
16 3 nngt0d 
 |-  ( B e. ( ZZ>= ` 2 ) -> 0 < B )
17 16 3ad2ant1 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> 0 < B )
18 expgt0 
 |-  ( ( B e. RR /\ N e. ZZ /\ 0 < B ) -> 0 < ( B ^ N ) )
19 12 14 17 18 syl3anc 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> 0 < ( B ^ N ) )
20 11 15 19 ltled 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> 0 <_ ( B ^ N ) )
21 0zd 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> 0 e. ZZ )
22 eluz2gt1 
 |-  ( B e. ( ZZ>= ` 2 ) -> 1 < B )
23 22 3ad2ant1 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> 1 < B )
24 simp3 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> N < 0 )
25 ltexp2a 
 |-  ( ( ( B e. RR /\ N e. ZZ /\ 0 e. ZZ ) /\ ( 1 < B /\ N < 0 ) ) -> ( B ^ N ) < ( B ^ 0 ) )
26 12 14 21 23 24 25 syl32anc 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> ( B ^ N ) < ( B ^ 0 ) )
27 eluzelcn 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. CC )
28 27 exp0d 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( B ^ 0 ) = 1 )
29 28 eqcomd 
 |-  ( B e. ( ZZ>= ` 2 ) -> 1 = ( B ^ 0 ) )
30 29 3ad2ant1 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> 1 = ( B ^ 0 ) )
31 26 30 breqtrrd 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> ( B ^ N ) < 1 )
32 0re 
 |-  0 e. RR
33 1xr 
 |-  1 e. RR*
34 32 33 pm3.2i 
 |-  ( 0 e. RR /\ 1 e. RR* )
35 elico2 
 |-  ( ( 0 e. RR /\ 1 e. RR* ) -> ( ( B ^ N ) e. ( 0 [,) 1 ) <-> ( ( B ^ N ) e. RR /\ 0 <_ ( B ^ N ) /\ ( B ^ N ) < 1 ) ) )
36 34 35 mp1i 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> ( ( B ^ N ) e. ( 0 [,) 1 ) <-> ( ( B ^ N ) e. RR /\ 0 <_ ( B ^ N ) /\ ( B ^ N ) < 1 ) ) )
37 10 20 31 36 mpbir3and 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> ( B ^ N ) e. ( 0 [,) 1 ) )