Metamath Proof Explorer

Theorem expnlbnd

Description: The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008)

Ref Expression
Assertion expnlbnd ⊢A∈ℝ+∧B∈ℝ∧1<B→∃k∈ℕ1Bk<A

Proof

Step Hyp Ref Expression
1 rpre ⊢A∈ℝ+→A∈ℝ
2 rpne0 ⊢A∈ℝ+→A≠0
3 1 2 rereccld ⊢A∈ℝ+→1A∈ℝ
4 expnbnd ⊢1A∈ℝ∧B∈ℝ∧1<B→∃k∈ℕ1A<Bk
5 3 4 syl3an1 ⊢A∈ℝ+∧B∈ℝ∧1<B→∃k∈ℕ1A<Bk
6 rpregt0 ⊢A∈ℝ+→A∈ℝ∧0<A
7 6 3ad2ant1 ⊢A∈ℝ+∧B∈ℝ∧1<B→A∈ℝ∧0<A
8 nnnn0 ⊢k∈ℕ→k∈ℕ0
9 reexpcl ⊢B∈ℝ∧k∈ℕ0→Bk∈ℝ
10 8 9 sylan2 ⊢B∈ℝ∧k∈ℕ→Bk∈ℝ
11 10 adantlr ⊢B∈ℝ∧1<B∧k∈ℕ→Bk∈ℝ
12 simpll ⊢B∈ℝ∧1<B∧k∈ℕ→B∈ℝ
13 nnz ⊢k∈ℕ→k∈ℤ
14 13 adantl ⊢B∈ℝ∧1<B∧k∈ℕ→k∈ℤ
15 0lt1 ⊢0<1
16 0re ⊢0∈ℝ
17 1re ⊢1∈ℝ
18 lttr ⊢0∈ℝ∧1∈ℝ∧B∈ℝ→0<1∧1<B→0<B
19 16 17 18 mp3an12 ⊢B∈ℝ→0<1∧1<B→0<B
20 15 19 mpani ⊢B∈ℝ→1<B→0<B
21 20 imp ⊢B∈ℝ∧1<B→0<B
22 21 adantr ⊢B∈ℝ∧1<B∧k∈ℕ→0<B
23 expgt0 ⊢B∈ℝ∧k∈ℤ∧0<B→0<Bk
24 12 14 22 23 syl3anc ⊢B∈ℝ∧1<B∧k∈ℕ→0<Bk
25 11 24 jca ⊢B∈ℝ∧1<B∧k∈ℕ→Bk∈ℝ∧0<Bk
26 25 3adantl1 ⊢A∈ℝ+∧B∈ℝ∧1<B∧k∈ℕ→Bk∈ℝ∧0<Bk
27 ltrec1 ⊢A∈ℝ∧0<A∧Bk∈ℝ∧0<Bk→1A<Bk↔1Bk<A
28 7 26 27 syl2an2r ⊢A∈ℝ+∧B∈ℝ∧1<B∧k∈ℕ→1A<Bk↔1Bk<A
29 28 rexbidva ⊢A∈ℝ+∧B∈ℝ∧1<B→∃k∈ℕ1A<Bk↔∃k∈ℕ1Bk<A
30 5 29 mpbid ⊢A∈ℝ+∧B∈ℝ∧1<B→∃k∈ℕ1Bk<A