Metamath Proof Explorer


Theorem expnlbnd2

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

Ref Expression
Assertion expnlbnd2 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 1 / ( 𝐵𝑘 ) ) < 𝐴 )

Proof

Step Hyp Ref Expression
1 expnlbnd ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑗 ∈ ℕ ( 1 / ( 𝐵𝑗 ) ) < 𝐴 )
2 simpl2 ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 𝐵 ∈ ℝ )
3 simpl3 ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 1 < 𝐵 )
4 1re 1 ∈ ℝ
5 ltle ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < 𝐵 → 1 ≤ 𝐵 ) )
6 4 2 5 sylancr ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( 1 < 𝐵 → 1 ≤ 𝐵 ) )
7 3 6 mpd ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 1 ≤ 𝐵 )
8 simprr ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 𝑘 ∈ ( ℤ𝑗 ) )
9 leexp2a ( ( 𝐵 ∈ ℝ ∧ 1 ≤ 𝐵𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐵𝑗 ) ≤ ( 𝐵𝑘 ) )
10 2 7 8 9 syl3anc ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( 𝐵𝑗 ) ≤ ( 𝐵𝑘 ) )
11 0red ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 0 ∈ ℝ )
12 1red ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 1 ∈ ℝ )
13 0lt1 0 < 1
14 13 a1i ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 0 < 1 )
15 11 12 2 14 3 lttrd ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 0 < 𝐵 )
16 2 15 elrpd ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 𝐵 ∈ ℝ+ )
17 nnz ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
18 17 ad2antrl ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 𝑗 ∈ ℤ )
19 rpexpcl ( ( 𝐵 ∈ ℝ+𝑗 ∈ ℤ ) → ( 𝐵𝑗 ) ∈ ℝ+ )
20 16 18 19 syl2anc ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( 𝐵𝑗 ) ∈ ℝ+ )
21 eluzelz ( 𝑘 ∈ ( ℤ𝑗 ) → 𝑘 ∈ ℤ )
22 21 ad2antll ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 𝑘 ∈ ℤ )
23 rpexpcl ( ( 𝐵 ∈ ℝ+𝑘 ∈ ℤ ) → ( 𝐵𝑘 ) ∈ ℝ+ )
24 16 22 23 syl2anc ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( 𝐵𝑘 ) ∈ ℝ+ )
25 20 24 lerecd ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐵𝑗 ) ≤ ( 𝐵𝑘 ) ↔ ( 1 / ( 𝐵𝑘 ) ) ≤ ( 1 / ( 𝐵𝑗 ) ) ) )
26 10 25 mpbid ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( 1 / ( 𝐵𝑘 ) ) ≤ ( 1 / ( 𝐵𝑗 ) ) )
27 24 rprecred ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( 1 / ( 𝐵𝑘 ) ) ∈ ℝ )
28 20 rprecred ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( 1 / ( 𝐵𝑗 ) ) ∈ ℝ )
29 simpl1 ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 𝐴 ∈ ℝ+ )
30 29 rpred ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → 𝐴 ∈ ℝ )
31 lelttr ( ( ( 1 / ( 𝐵𝑘 ) ) ∈ ℝ ∧ ( 1 / ( 𝐵𝑗 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( ( 1 / ( 𝐵𝑘 ) ) ≤ ( 1 / ( 𝐵𝑗 ) ) ∧ ( 1 / ( 𝐵𝑗 ) ) < 𝐴 ) → ( 1 / ( 𝐵𝑘 ) ) < 𝐴 ) )
32 27 28 30 31 syl3anc ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( ( ( 1 / ( 𝐵𝑘 ) ) ≤ ( 1 / ( 𝐵𝑗 ) ) ∧ ( 1 / ( 𝐵𝑗 ) ) < 𝐴 ) → ( 1 / ( 𝐵𝑘 ) ) < 𝐴 ) )
33 26 32 mpand ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ) → ( ( 1 / ( 𝐵𝑗 ) ) < 𝐴 → ( 1 / ( 𝐵𝑘 ) ) < 𝐴 ) )
34 33 anassrs ( ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( 1 / ( 𝐵𝑗 ) ) < 𝐴 → ( 1 / ( 𝐵𝑘 ) ) < 𝐴 ) )
35 34 ralrimdva ( ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑗 ∈ ℕ ) → ( ( 1 / ( 𝐵𝑗 ) ) < 𝐴 → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 1 / ( 𝐵𝑘 ) ) < 𝐴 ) )
36 35 reximdva ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( ∃ 𝑗 ∈ ℕ ( 1 / ( 𝐵𝑗 ) ) < 𝐴 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 1 / ( 𝐵𝑘 ) ) < 𝐴 ) )
37 1 36 mpd ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 1 / ( 𝐵𝑘 ) ) < 𝐴 )