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 ∈ ℕ 1 B k < A

Proof

Step Hyp Ref Expression
1 rpre ⊢ A ∈ ℝ + → A ∈ ℝ
2 rpne0 ⊢ A ∈ ℝ + → A ≠ 0
3 1 2 rereccld ⊢ A ∈ ℝ + → 1 A ∈ ℝ
4 expnbnd ⊢ 1 A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < B → ∃ k ∈ ℕ 1 A < B k
5 3 4 syl3an1 ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ 1 < B → ∃ k ∈ ℕ 1 A < B k
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 → B k ∈ ℝ
10 8 9 sylan2 ⊢ B ∈ ℝ ∧ k ∈ ℕ → B k ∈ ℝ
11 10 adantlr ⊢ B ∈ ℝ ∧ 1 < B ∧ k ∈ ℕ → B k ∈ ℝ
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 < B k
24 12 14 22 23 syl3anc ⊢ B ∈ ℝ ∧ 1 < B ∧ k ∈ ℕ → 0 < B k
25 11 24 jca ⊢ B ∈ ℝ ∧ 1 < B ∧ k ∈ ℕ → B k ∈ ℝ ∧ 0 < B k
26 25 3adantl1 ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ 1 < B ∧ k ∈ ℕ → B k ∈ ℝ ∧ 0 < B k
27 ltrec1 ⊢ A ∈ ℝ ∧ 0 < A ∧ B k ∈ ℝ ∧ 0 < B k → 1 A < B k ↔ 1 B k < A
28 7 26 27 syl2an2r ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ 1 < B ∧ k ∈ ℕ → 1 A < B k ↔ 1 B k < A
29 28 rexbidva ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ 1 < B → ∃ k ∈ ℕ 1 A < B k ↔ ∃ k ∈ ℕ 1 B k < A
30 5 29 mpbid ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ 1 < B → ∃ k ∈ ℕ 1 B k < A