# 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 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {{B}}^{{N}}\in \left[0,1\right)$

### Proof

Step Hyp Ref Expression
1 eluzelre ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℝ$
2 1 adantr ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {B}\in ℝ$
3 eluz2nn ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℕ$
4 3 nnne0d ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\ne 0$
5 4 adantr ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {B}\ne 0$
6 simpr ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {N}\in ℤ$
7 2 5 6 3jca ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left({B}\in ℝ\wedge {B}\ne 0\wedge {N}\in ℤ\right)$
8 7 3adant3 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to \left({B}\in ℝ\wedge {B}\ne 0\wedge {N}\in ℤ\right)$
9 reexpclz ${⊢}\left({B}\in ℝ\wedge {B}\ne 0\wedge {N}\in ℤ\right)\to {{B}}^{{N}}\in ℝ$
10 8 9 syl ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {{B}}^{{N}}\in ℝ$
11 0red ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to 0\in ℝ$
12 1 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {B}\in ℝ$
13 4 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {B}\ne 0$
14 simp2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {N}\in ℤ$
15 12 13 14 reexpclzd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {{B}}^{{N}}\in ℝ$
16 3 nngt0d ${⊢}{B}\in {ℤ}_{\ge 2}\to 0<{B}$
17 16 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to 0<{B}$
18 expgt0 ${⊢}\left({B}\in ℝ\wedge {N}\in ℤ\wedge 0<{B}\right)\to 0<{{B}}^{{N}}$
19 12 14 17 18 syl3anc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to 0<{{B}}^{{N}}$
20 11 15 19 ltled ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to 0\le {{B}}^{{N}}$
21 0zd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to 0\in ℤ$
22 eluz2gt1 ${⊢}{B}\in {ℤ}_{\ge 2}\to 1<{B}$
23 22 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to 1<{B}$
24 simp3 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {N}<0$
25 ltexp2a ${⊢}\left(\left({B}\in ℝ\wedge {N}\in ℤ\wedge 0\in ℤ\right)\wedge \left(1<{B}\wedge {N}<0\right)\right)\to {{B}}^{{N}}<{{B}}^{0}$
26 12 14 21 23 24 25 syl32anc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {{B}}^{{N}}<{{B}}^{0}$
27 eluzelcn ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℂ$
28 27 exp0d ${⊢}{B}\in {ℤ}_{\ge 2}\to {{B}}^{0}=1$
29 28 eqcomd ${⊢}{B}\in {ℤ}_{\ge 2}\to 1={{B}}^{0}$
30 29 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to 1={{B}}^{0}$
31 26 30 breqtrrd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {{B}}^{{N}}<1$
32 0re ${⊢}0\in ℝ$
33 1xr ${⊢}1\in {ℝ}^{*}$
34 32 33 pm3.2i ${⊢}\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)$
35 elico2 ${⊢}\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)\to \left({{B}}^{{N}}\in \left[0,1\right)↔\left({{B}}^{{N}}\in ℝ\wedge 0\le {{B}}^{{N}}\wedge {{B}}^{{N}}<1\right)\right)$
36 34 35 mp1i ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to \left({{B}}^{{N}}\in \left[0,1\right)↔\left({{B}}^{{N}}\in ℝ\wedge 0\le {{B}}^{{N}}\wedge {{B}}^{{N}}<1\right)\right)$
37 10 20 31 36 mpbir3and ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\wedge {N}<0\right)\to {{B}}^{{N}}\in \left[0,1\right)$