# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in ℝ\wedge 1<{B}\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\frac{1}{{{B}}^{{k}}}<{A}$

### Proof

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