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 / ( 𝐵 ↑ 𝑘 ) ) < 𝐴 )