Proof of Theorem expnlbnd2
Step | Hyp | Ref
| Expression |
1 | | expnlbnd 9026 |
. 2
⊢
((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) → ∃𝑗 ∈ ℕ
(1 / (B↑𝑗)) < A) |
2 | | simpl2 907 |
. . . . . . . 8
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → B ∈
ℝ) |
3 | | simpl3 908 |
. . . . . . . . 9
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 1 < B) |
4 | | 1re 6824 |
. . . . . . . . . 10
⊢ 1 ∈ ℝ |
5 | | ltle 6902 |
. . . . . . . . . 10
⊢ ((1 ∈ ℝ ∧
B ∈
ℝ) → (1 < B → 1 ≤
B)) |
6 | 4, 2, 5 | sylancr 393 |
. . . . . . . . 9
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (1 < B → 1 ≤ B)) |
7 | 3, 6 | mpd 13 |
. . . . . . . 8
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 1 ≤ B) |
8 | | simprr 484 |
. . . . . . . 8
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝑘 ∈
(ℤ≥‘𝑗)) |
9 | | leexp2a 8961 |
. . . . . . . 8
⊢
((B ∈ ℝ ∧ 1 ≤
B ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (B↑𝑗) ≤ (B↑𝑘)) |
10 | 2, 7, 8, 9 | syl3anc 1134 |
. . . . . . 7
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (B↑𝑗) ≤ (B↑𝑘)) |
11 | | 0red 6826 |
. . . . . . . . . . 11
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 0 ∈ ℝ) |
12 | | 1red 6840 |
. . . . . . . . . . 11
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 1 ∈ ℝ) |
13 | | 0lt1 6938 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
14 | 13 | a1i 9 |
. . . . . . . . . . 11
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 0 < 1) |
15 | 11, 12, 2, 14, 3 | lttrd 6937 |
. . . . . . . . . 10
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 0 < B) |
16 | 2, 15 | elrpd 8395 |
. . . . . . . . 9
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → B ∈
ℝ+) |
17 | | nnz 8040 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
18 | 17 | ad2antrl 459 |
. . . . . . . . 9
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝑗 ∈
ℤ) |
19 | | rpexpcl 8928 |
. . . . . . . . 9
⊢
((B ∈ ℝ+ ∧ 𝑗
∈ ℤ) → (B↑𝑗) ∈
ℝ+) |
20 | 16, 18, 19 | syl2anc 391 |
. . . . . . . 8
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (B↑𝑗) ∈
ℝ+) |
21 | | eluzelz 8258 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ℤ≥‘𝑗) → 𝑘 ∈
ℤ) |
22 | 21 | ad2antll 460 |
. . . . . . . . 9
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝑘 ∈
ℤ) |
23 | | rpexpcl 8928 |
. . . . . . . . 9
⊢
((B ∈ ℝ+ ∧ 𝑘
∈ ℤ) → (B↑𝑘) ∈
ℝ+) |
24 | 16, 22, 23 | syl2anc 391 |
. . . . . . . 8
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (B↑𝑘) ∈
ℝ+) |
25 | 20, 24 | lerecd 8416 |
. . . . . . 7
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((B↑𝑗) ≤ (B↑𝑘) ↔ (1 / (B↑𝑘)) ≤ (1 / (B↑𝑗)))) |
26 | 10, 25 | mpbid 135 |
. . . . . 6
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (1 / (B↑𝑘)) ≤ (1 / (B↑𝑗))) |
27 | 24 | rprecred 8408 |
. . . . . . 7
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (1 / (B↑𝑘)) ∈
ℝ) |
28 | 20 | rprecred 8408 |
. . . . . . 7
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (1 / (B↑𝑗)) ∈
ℝ) |
29 | | simpl1 906 |
. . . . . . . 8
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → A ∈
ℝ+) |
30 | 29 | rpred 8397 |
. . . . . . 7
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → A ∈
ℝ) |
31 | | lelttr 6903 |
. . . . . . 7
⊢ (((1 /
(B↑𝑘)) ∈
ℝ ∧ (1 / (B↑𝑗)) ∈
ℝ ∧ A ∈ ℝ)
→ (((1 / (B↑𝑘)) ≤ (1 / (B↑𝑗)) ∧ (1 /
(B↑𝑗)) < A) → (1 / (B↑𝑘)) < A)) |
32 | 27, 28, 30, 31 | syl3anc 1134 |
. . . . . 6
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (((1 / (B↑𝑘)) ≤ (1 / (B↑𝑗)) ∧ (1 /
(B↑𝑗)) < A) → (1 / (B↑𝑘)) < A)) |
33 | 26, 32 | mpand 405 |
. . . . 5
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧
(𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((1 / (B↑𝑗)) < A
→ (1 / (B↑𝑘)) < A)) |
34 | 33 | anassrs 380 |
. . . 4
⊢
((((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((1 / (B↑𝑗)) < A
→ (1 / (B↑𝑘)) < A)) |
35 | 34 | ralrimdva 2393 |
. . 3
⊢
(((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) ∧ 𝑗 ∈ ℕ) → ((1 / (B↑𝑗)) < A
→ ∀𝑘 ∈
(ℤ≥‘𝑗)(1 / (B↑𝑘)) < A)) |
36 | 35 | reximdva 2415 |
. 2
⊢
((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) → (∃𝑗 ∈ ℕ
(1 / (B↑𝑗)) < A
→ ∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(1 / (B↑𝑘)) < A)) |
37 | 1, 36 | mpd 13 |
1
⊢
((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 <
B) → ∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(1 / (B↑𝑘)) < A) |