expnlbnd2

Description: The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008) (Proof shortened by Mario Carneiro, 5-Jun-2014)

		Ref	Expression
	Assertion	expnlbnd2	$⊢ (A \in ℝ^{+} \land B \in ℝ \land 1 < B) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \frac{1}{B^{k}} < A$

Proof

Step	Hyp	Ref	Expression
1		expnlbnd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land 1 < B) \to \exists j \in ℕ \frac{1}{B^{j}} < A$
2		simpl2	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to B \in ℝ$
3		simpl3	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to 1 < B$
4		1re	$⊢ 1 \in ℝ$
5		ltle	$⊢ (1 \in ℝ \land B \in ℝ) \to (1 < B \to 1 \leq B)$
6	4 2 5	sylancr	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to (1 < B \to 1 \leq B)$
7	3 6	mpd	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to 1 \leq B$
8		simprr	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to k \in ℤ_{\geq j}$
9		leexp2a	$⊢ (B \in ℝ \land 1 \leq B \land k \in ℤ_{\geq j}) \to B^{j} \leq B^{k}$
10	2 7 8 9	syl3anc	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to B^{j} \leq B^{k}$
11		0red	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to 0 \in ℝ$
12		1red	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to 1 \in ℝ$
13		0lt1	$⊢ 0 < 1$
14	13	a1i	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to 0 < 1$
15	11 12 2 14 3	lttrd	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to 0 < B$
16	2 15	elrpd	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to B \in ℝ^{+}$
17		nnz	$⊢ j \in ℕ \to j \in ℤ$
18	17	ad2antrl	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to j \in ℤ$
19		rpexpcl	$⊢ (B \in ℝ^{+} \land j \in ℤ) \to B^{j} \in ℝ^{+}$
20	16 18 19	syl2anc	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to B^{j} \in ℝ^{+}$
21		eluzelz	$⊢ k \in ℤ_{\geq j} \to k \in ℤ$
22	21	ad2antll	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to k \in ℤ$
23		rpexpcl	$⊢ (B \in ℝ^{+} \land k \in ℤ) \to B^{k} \in ℝ^{+}$
24	16 22 23	syl2anc	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to B^{k} \in ℝ^{+}$
25	20 24	lerecd	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to (B^{j} \leq B^{k} \leftrightarrow \frac{1}{B^{k}} \leq \frac{1}{B^{j}})$
26	10 25	mpbid	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to \frac{1}{B^{k}} \leq \frac{1}{B^{j}}$
27	24	rprecred	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to \frac{1}{B^{k}} \in ℝ$
28	20	rprecred	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to \frac{1}{B^{j}} \in ℝ$
29		simpl1	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to A \in ℝ^{+}$
30	29	rpred	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to A \in ℝ$
31		lelttr	$⊢ (\frac{1}{B^{k}} \in ℝ \land \frac{1}{B^{j}} \in ℝ \land A \in ℝ) \to ((\frac{1}{B^{k}} \leq \frac{1}{B^{j}} \land \frac{1}{B^{j}} < A) \to \frac{1}{B^{k}} < A)$
32	27 28 30 31	syl3anc	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to ((\frac{1}{B^{k}} \leq \frac{1}{B^{j}} \land \frac{1}{B^{j}} < A) \to \frac{1}{B^{k}} < A)$
33	26 32	mpand	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to (\frac{1}{B^{j}} < A \to \frac{1}{B^{k}} < A)$
34	33	anassrs	$⊢ (((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (\frac{1}{B^{j}} < A \to \frac{1}{B^{k}} < A)$
35	34	ralrimdva	$⊢ ((A \in ℝ^{+} \land B \in ℝ \land 1 < B) \land j \in ℕ) \to (\frac{1}{B^{j}} < A \to \forall k \in ℤ_{\geq j} \frac{1}{B^{k}} < A)$
36	35	reximdva	$⊢ (A \in ℝ^{+} \land B \in ℝ \land 1 < B) \to (\exists j \in ℕ \frac{1}{B^{j}} < A \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \frac{1}{B^{k}} < A)$
37	1 36	mpd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land 1 < B) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \frac{1}{B^{k}} < A$

Metamath Proof Explorer

Theorem expnlbnd2

Proof