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 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → ( 𝐵𝑁 ) ∈ ( 0 [,) 1 ) )

Proof

Step Hyp Ref Expression
1 eluzelre ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℝ )
2 1 adantr ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝐵 ∈ ℝ )
3 eluz2nn ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℕ )
4 3 nnne0d ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ≠ 0 )
5 4 adantr ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝐵 ≠ 0 )
6 simpr ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
7 2 5 6 3jca ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ∧ 𝑁 ∈ ℤ ) )
8 7 3adant3 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ∧ 𝑁 ∈ ℤ ) )
9 reexpclz ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐵𝑁 ) ∈ ℝ )
10 8 9 syl ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → ( 𝐵𝑁 ) ∈ ℝ )
11 0red ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 0 ∈ ℝ )
12 1 3ad2ant1 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 𝐵 ∈ ℝ )
13 4 3ad2ant1 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 𝐵 ≠ 0 )
14 simp2 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 𝑁 ∈ ℤ )
15 12 13 14 reexpclzd ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → ( 𝐵𝑁 ) ∈ ℝ )
16 3 nngt0d ( 𝐵 ∈ ( ℤ ‘ 2 ) → 0 < 𝐵 )
17 16 3ad2ant1 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 0 < 𝐵 )
18 expgt0 ( ( 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < 𝐵 ) → 0 < ( 𝐵𝑁 ) )
19 12 14 17 18 syl3anc ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 0 < ( 𝐵𝑁 ) )
20 11 15 19 ltled ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 0 ≤ ( 𝐵𝑁 ) )
21 0zd ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 0 ∈ ℤ )
22 eluz2gt1 ( 𝐵 ∈ ( ℤ ‘ 2 ) → 1 < 𝐵 )
23 22 3ad2ant1 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 1 < 𝐵 )
24 simp3 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 𝑁 < 0 )
25 ltexp2a ( ( ( 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 1 < 𝐵𝑁 < 0 ) ) → ( 𝐵𝑁 ) < ( 𝐵 ↑ 0 ) )
26 12 14 21 23 24 25 syl32anc ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → ( 𝐵𝑁 ) < ( 𝐵 ↑ 0 ) )
27 eluzelcn ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℂ )
28 27 exp0d ( 𝐵 ∈ ( ℤ ‘ 2 ) → ( 𝐵 ↑ 0 ) = 1 )
29 28 eqcomd ( 𝐵 ∈ ( ℤ ‘ 2 ) → 1 = ( 𝐵 ↑ 0 ) )
30 29 3ad2ant1 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → 1 = ( 𝐵 ↑ 0 ) )
31 26 30 breqtrrd ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → ( 𝐵𝑁 ) < 1 )
32 0re 0 ∈ ℝ
33 1xr 1 ∈ ℝ*
34 32 33 pm3.2i ( 0 ∈ ℝ ∧ 1 ∈ ℝ* )
35 elico2 ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( ( 𝐵𝑁 ) ∈ ( 0 [,) 1 ) ↔ ( ( 𝐵𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝐵𝑁 ) ∧ ( 𝐵𝑁 ) < 1 ) ) )
36 34 35 mp1i ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → ( ( 𝐵𝑁 ) ∈ ( 0 [,) 1 ) ↔ ( ( 𝐵𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝐵𝑁 ) ∧ ( 𝐵𝑁 ) < 1 ) ) )
37 10 20 31 36 mpbir3and ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0 ) → ( 𝐵𝑁 ) ∈ ( 0 [,) 1 ) )