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 ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑘 ∈ ℕ ( 1 / ( 𝐵 ↑ 𝑘 ) ) < 𝐴 )

Proof

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