Proof of Theorem expnlbnd2
Step | Hyp | Ref
| Expression |
1 | | expnlbnd 10542 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) →
∃𝑗 ∈ ℕ (1
/ (𝐵↑𝑗)) < 𝐴) |
2 | | simpl2 986 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 𝐵 ∈ ℝ) |
3 | | simpl3 987 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 1 < 𝐵) |
4 | | 1re 7877 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
5 | | ltle 7964 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ) → (1 < 𝐵 → 1 ≤ 𝐵)) |
6 | 4, 2, 5 | sylancr 411 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (1 < 𝐵 → 1 ≤ 𝐵)) |
7 | 3, 6 | mpd 13 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 1 ≤ 𝐵) |
8 | | simprr 522 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 𝑘 ∈ (ℤ≥‘𝑗)) |
9 | | leexp2a 10472 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 1 ≤
𝐵 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐵↑𝑗) ≤ (𝐵↑𝑘)) |
10 | 2, 7, 8, 9 | syl3anc 1220 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (𝐵↑𝑗) ≤ (𝐵↑𝑘)) |
11 | | 0red 7879 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 0 ∈ ℝ) |
12 | | 1red 7893 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 1 ∈ ℝ) |
13 | | 0lt1 8002 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
14 | 13 | a1i 9 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 0 < 1) |
15 | 11, 12, 2, 14, 3 | lttrd 8001 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 0 < 𝐵) |
16 | 2, 15 | elrpd 9600 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 𝐵 ∈
ℝ+) |
17 | | nnz 9186 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
18 | 17 | ad2antrl 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 𝑗 ∈ ℤ) |
19 | | rpexpcl 10438 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ+
∧ 𝑗 ∈ ℤ)
→ (𝐵↑𝑗) ∈
ℝ+) |
20 | 16, 18, 19 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (𝐵↑𝑗) ∈
ℝ+) |
21 | | eluzelz 9448 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘𝑗) → 𝑘 ∈ ℤ) |
22 | 21 | ad2antll 483 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 𝑘 ∈ ℤ) |
23 | | rpexpcl 10438 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (𝐵↑𝑘) ∈
ℝ+) |
24 | 16, 22, 23 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (𝐵↑𝑘) ∈
ℝ+) |
25 | 20, 24 | lerecd 9623 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → ((𝐵↑𝑗) ≤ (𝐵↑𝑘) ↔ (1 / (𝐵↑𝑘)) ≤ (1 / (𝐵↑𝑗)))) |
26 | 10, 25 | mpbid 146 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (1 / (𝐵↑𝑘)) ≤ (1 / (𝐵↑𝑗))) |
27 | 24 | rprecred 9615 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (1 / (𝐵↑𝑘)) ∈ ℝ) |
28 | 20 | rprecred 9615 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (1 / (𝐵↑𝑗)) ∈ ℝ) |
29 | | simpl1 985 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 𝐴 ∈
ℝ+) |
30 | 29 | rpred 9603 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → 𝐴 ∈ ℝ) |
31 | | lelttr 7965 |
. . . . . . 7
⊢ (((1 /
(𝐵↑𝑘)) ∈ ℝ ∧ (1 / (𝐵↑𝑗)) ∈ ℝ ∧ 𝐴 ∈ ℝ) → (((1 / (𝐵↑𝑘)) ≤ (1 / (𝐵↑𝑗)) ∧ (1 / (𝐵↑𝑗)) < 𝐴) → (1 / (𝐵↑𝑘)) < 𝐴)) |
32 | 27, 28, 30, 31 | syl3anc 1220 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (((1 / (𝐵↑𝑘)) ≤ (1 / (𝐵↑𝑗)) ∧ (1 / (𝐵↑𝑗)) < 𝐴) → (1 / (𝐵↑𝑘)) < 𝐴)) |
33 | 26, 32 | mpand 426 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → ((1 / (𝐵↑𝑗)) < 𝐴 → (1 / (𝐵↑𝑘)) < 𝐴)) |
34 | 33 | anassrs 398 |
. . . 4
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → ((1 / (𝐵↑𝑗)) < 𝐴 → (1 / (𝐵↑𝑘)) < 𝐴)) |
35 | 34 | ralrimdva 2537 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) ∧ 𝑗 ∈ ℕ) → ((1 /
(𝐵↑𝑗)) < 𝐴 → ∀𝑘 ∈ (ℤ≥‘𝑗)(1 / (𝐵↑𝑘)) < 𝐴)) |
36 | 35 | reximdva 2559 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) →
(∃𝑗 ∈ ℕ (1
/ (𝐵↑𝑗)) < 𝐴 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(1 / (𝐵↑𝑘)) < 𝐴)) |
37 | 1, 36 | mpd 13 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(1 / (𝐵↑𝑘)) < 𝐴) |