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 \in ℤ_{\geq 2} \land N \in ℤ \land N < 0) \to B^{N} \in [0, 1)$

Proof

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

Metamath Proof Explorer

Theorem expnegico01

Proof