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 ) )