Step | Hyp | Ref
| Expression |
1 | | 2re 11790 |
. . . . 5
⊢ 2 ∈
ℝ |
2 | | simp1 1137 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐴 ∈ ℝ) |
3 | | remulcl 10700 |
. . . . 5
⊢ ((2
∈ ℝ ∧ 𝐴
∈ ℝ) → (2 · 𝐴) ∈ ℝ) |
4 | 1, 2, 3 | sylancr 590 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (2 · 𝐴) ∈
ℝ) |
5 | | simp3 1139 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 1 < 𝐵) |
6 | | 1re 10719 |
. . . . . 6
⊢ 1 ∈
ℝ |
7 | | simp2 1138 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐵 ∈ ℝ) |
8 | | difrp 12510 |
. . . . . 6
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ) → (1 < 𝐵 ↔ (𝐵 − 1) ∈
ℝ+)) |
9 | 6, 7, 8 | sylancr 590 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (1 < 𝐵 ↔ (𝐵 − 1) ∈
ℝ+)) |
10 | 5, 9 | mpbid 235 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵 − 1) ∈
ℝ+) |
11 | 4, 10 | rerpdivcld 12545 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ((2 ·
𝐴) / (𝐵 − 1)) ∈
ℝ) |
12 | | expnbnd 13685 |
. . 3
⊢ ((((2
· 𝐴) / (𝐵 − 1)) ∈ ℝ
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) →
∃𝑛 ∈ ℕ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛)) |
13 | 11, 7, 5, 12 | syl3anc 1372 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ∃𝑛 ∈ ℕ ((2 ·
𝐴) / (𝐵 − 1)) < (𝐵↑𝑛)) |
14 | | 2nn0 11993 |
. . . 4
⊢ 2 ∈
ℕ0 |
15 | | nnnn0 11983 |
. . . . 5
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
16 | 15 | ad2antrl 728 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ0) |
17 | | nn0mulcl 12012 |
. . . 4
⊢ ((2
∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℕ0) |
18 | 14, 16, 17 | sylancr 590 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈
ℕ0) |
19 | 2 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐴 ∈
ℝ) |
20 | | 2nn 11789 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
21 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ) |
22 | | nnmulcl 11740 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ) → (2 · 𝑛) ∈ ℕ) |
23 | 20, 21, 22 | sylancr 590 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ) |
24 | | eluznn 12400 |
. . . . . . . 8
⊢ (((2
· 𝑛) ∈ ℕ
∧ 𝑘 ∈
(ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ) |
25 | 23, 24 | sylan 583 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℕ) |
26 | 25 | nnred 11731 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℝ) |
27 | 19, 26 | remulcld 10749 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐴 · 𝑘) ∈ ℝ) |
28 | | 0re 10721 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
29 | | ifcl 4459 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ) |
30 | 19, 28, 29 | sylancl 589 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → if(0
≤ 𝐴, 𝐴, 0) ∈ ℝ) |
31 | | remulcl 10700 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ) → (2 · if(0
≤ 𝐴, 𝐴, 0)) ∈ ℝ) |
32 | 1, 30, 31 | sylancr 590 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· if(0 ≤ 𝐴, 𝐴, 0)) ∈
ℝ) |
33 | | simplrl 777 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑛 ∈
ℕ) |
34 | 33 | nnred 11731 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑛 ∈
ℝ) |
35 | 26, 34 | resubcld 11146 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈ ℝ) |
36 | 32, 35 | remulcld 10749 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) ∈ ℝ) |
37 | 7 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐵 ∈
ℝ) |
38 | 25 | nnnn0d 12036 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℕ0) |
39 | | reexpcl 13538 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑𝑘) ∈
ℝ) |
40 | 37, 38, 39 | syl2anc 587 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑𝑘) ∈ ℝ) |
41 | | remulcl 10700 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ (𝑘
− 𝑛) ∈ ℝ)
→ (2 · (𝑘
− 𝑛)) ∈
ℝ) |
42 | 1, 35, 41 | sylancr 590 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· (𝑘 − 𝑛)) ∈
ℝ) |
43 | 38 | nn0ge0d 12039 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 ≤
𝑘) |
44 | | max1 12661 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0)) |
45 | 28, 19, 44 | sylancr 590 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 ≤
if(0 ≤ 𝐴, 𝐴, 0)) |
46 | | remulcl 10700 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 𝑛
∈ ℝ) → (2 · 𝑛) ∈ ℝ) |
47 | 1, 34, 46 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑛) ∈
ℝ) |
48 | | eluzle 12337 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘(2 · 𝑛)) → (2 · 𝑛) ≤ 𝑘) |
49 | 48 | adantl 485 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑛) ≤ 𝑘) |
50 | 47, 26, 26, 49 | leadd2dd 11333 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (𝑘 + 𝑘)) |
51 | 26 | recnd 10747 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℂ) |
52 | 51 | 2timesd 11959 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑘) = (𝑘 + 𝑘)) |
53 | 50, 52 | breqtrrd 5058 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘)) |
54 | | remulcl 10700 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 𝑘
∈ ℝ) → (2 · 𝑘) ∈ ℝ) |
55 | 1, 26, 54 | sylancr 590 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑘) ∈
ℝ) |
56 | | leaddsub 11194 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧ (2
· 𝑛) ∈ ℝ
∧ (2 · 𝑘) ∈
ℝ) → ((𝑘 + (2
· 𝑛)) ≤ (2
· 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛)))) |
57 | 26, 47, 55, 56 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛)))) |
58 | 53, 57 | mpbid 235 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))) |
59 | | 2cnd 11794 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 2
∈ ℂ) |
60 | 34 | recnd 10747 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑛 ∈
ℂ) |
61 | 59, 51, 60 | subdid 11174 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛))) |
62 | 58, 61 | breqtrrd 5058 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ≤ (2 · (𝑘 − 𝑛))) |
63 | | max2 12663 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → 𝐴
≤ if(0 ≤ 𝐴, 𝐴, 0)) |
64 | 28, 19, 63 | sylancr 590 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐴 ≤ if(0 ≤ 𝐴, 𝐴, 0)) |
65 | 26, 42, 19, 30, 43, 45, 62, 64 | lemul12bd 11661 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 · 𝐴) ≤ ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0))) |
66 | 19 | recnd 10747 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐴 ∈
ℂ) |
67 | 66, 51 | mulcomd 10740 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐴 · 𝑘) = (𝑘 · 𝐴)) |
68 | 30 | recnd 10747 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → if(0
≤ 𝐴, 𝐴, 0) ∈ ℂ) |
69 | 35 | recnd 10747 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈ ℂ) |
70 | 59, 68, 69 | mul32d 10928 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) = ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0))) |
71 | 65, 67, 70 | 3brtr4d 5062 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐴 · 𝑘) ≤ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛))) |
72 | 10 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵 − 1) ∈
ℝ+) |
73 | 72 | rpred 12514 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵 − 1) ∈
ℝ) |
74 | 73, 35 | remulcld 10749 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝑘 − 𝑛)) ∈
ℝ) |
75 | 33 | nnnn0d 12036 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑛 ∈
ℕ0) |
76 | | reexpcl 13538 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℕ0)
→ (𝐵↑𝑛) ∈
ℝ) |
77 | 37, 75, 76 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑𝑛) ∈ ℝ) |
78 | 74, 77 | remulcld 10749 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝑘 − 𝑛)) · (𝐵↑𝑛)) ∈ ℝ) |
79 | | simplrr 778 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛)) |
80 | 1, 19, 3 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝐴) ∈
ℝ) |
81 | 80, 77, 72 | ltdivmuld 12565 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛) ↔ (2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)))) |
82 | 79, 81 | mpbid 235 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛))) |
83 | 5 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 1 <
𝐵) |
84 | | posdif 11211 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1))) |
85 | 6, 37, 84 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (1
< 𝐵 ↔ 0 < (𝐵 − 1))) |
86 | 83, 85 | mpbid 235 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
(𝐵 −
1)) |
87 | 33 | nnzd 12167 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑛 ∈
ℤ) |
88 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0
∈ ℝ) |
89 | 6 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 1
∈ ℝ) |
90 | | 0lt1 11240 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
91 | 90 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
1) |
92 | 88, 89, 37, 91, 83 | lttrd 10879 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
𝐵) |
93 | | expgt0 13554 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 0 <
𝐵) → 0 < (𝐵↑𝑛)) |
94 | 37, 87, 92, 93 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
(𝐵↑𝑛)) |
95 | 73, 77, 86, 94 | mulgt0d 10873 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
((𝐵 − 1) ·
(𝐵↑𝑛))) |
96 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 𝐴) = (2 · if(0 ≤ 𝐴, 𝐴, 0))) |
97 | 96 | breq1d 5040 |
. . . . . . . . . 10
⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → ((2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)))) |
98 | | 2t0e0 11885 |
. . . . . . . . . . . 12
⊢ (2
· 0) = 0 |
99 | | oveq2 7178 |
. . . . . . . . . . . 12
⊢ (0 = if(0
≤ 𝐴, 𝐴, 0) → (2 · 0) = (2 ·
if(0 ≤ 𝐴, 𝐴, 0))) |
100 | 98, 99 | eqtr3id 2787 |
. . . . . . . . . . 11
⊢ (0 = if(0
≤ 𝐴, 𝐴, 0) → 0 = (2 · if(0 ≤ 𝐴, 𝐴, 0))) |
101 | 100 | breq1d 5040 |
. . . . . . . . . 10
⊢ (0 = if(0
≤ 𝐴, 𝐴, 0) → (0 < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)))) |
102 | 97, 101 | ifboth 4453 |
. . . . . . . . 9
⊢ (((2
· 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ∧ 0 < ((𝐵 − 1) · (𝐵↑𝑛))) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))) |
103 | 82, 95, 102 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))) |
104 | 73, 77 | remulcld 10749 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝐵↑𝑛)) ∈ ℝ) |
105 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
(ℤ≥‘(2 · 𝑛))) |
106 | 60 | 2timesd 11959 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑛) = (𝑛 + 𝑛)) |
107 | 106 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(ℤ≥‘(2 · 𝑛)) = (ℤ≥‘(𝑛 + 𝑛))) |
108 | 105, 107 | eleqtrd 2835 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
(ℤ≥‘(𝑛 + 𝑛))) |
109 | | eluzsub 12356 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘(𝑛 + 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ≥‘𝑛)) |
110 | 87, 87, 108, 109 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ≥‘𝑛)) |
111 | | eluznn 12400 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ (𝑘 − 𝑛) ∈ (ℤ≥‘𝑛)) → (𝑘 − 𝑛) ∈ ℕ) |
112 | 33, 110, 111 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈ ℕ) |
113 | 112 | nngt0d 11765 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
(𝑘 − 𝑛)) |
114 | | ltmul1 11568 |
. . . . . . . . 9
⊢ (((2
· if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ ∧
((𝐵 − 1) ·
(𝐵↑𝑛)) ∈ ℝ ∧ ((𝑘 − 𝑛) ∈ ℝ ∧ 0 < (𝑘 − 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)))) |
115 | 32, 104, 35, 113, 114 | syl112anc 1375 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)))) |
116 | 103, 115 | mpbid 235 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛))) |
117 | 73 | recnd 10747 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵 − 1) ∈
ℂ) |
118 | 77 | recnd 10747 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑𝑛) ∈ ℂ) |
119 | 117, 118,
69 | mul32d 10928 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝐵↑𝑛)) · (𝑘 − 𝑛)) = (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛))) |
120 | 116, 119 | breqtrd 5056 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛))) |
121 | | peano2re 10891 |
. . . . . . . . . 10
⊢ (((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ) |
122 | 74, 121 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝑘 − 𝑛)) + 1) ∈
ℝ) |
123 | 112 | nnnn0d 12036 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈
ℕ0) |
124 | | reexpcl 13538 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ0) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ) |
125 | 37, 123, 124 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ) |
126 | 74 | ltp1d 11648 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) + 1)) |
127 | 88, 37, 92 | ltled 10866 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 ≤
𝐵) |
128 | | bernneq2 13683 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ0 ∧ 0 ≤
𝐵) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛))) |
129 | 37, 123, 127, 128 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛))) |
130 | 74, 122, 125, 126, 129 | ltletrd 10878 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝑘 − 𝑛)) < (𝐵↑(𝑘 − 𝑛))) |
131 | 37 | recnd 10747 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐵 ∈
ℂ) |
132 | 92 | gt0ne0d 11282 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐵 ≠ 0) |
133 | | eluzelz 12334 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘(2 · 𝑛)) → 𝑘 ∈ ℤ) |
134 | 133 | adantl 485 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℤ) |
135 | | expsub 13569 |
. . . . . . . . 9
⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛))) |
136 | 131, 132,
134, 87, 135 | syl22anc 838 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛))) |
137 | 130, 136 | breqtrd 5056 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛))) |
138 | | ltmuldiv 11591 |
. . . . . . . 8
⊢ ((((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ ∧ (𝐵↑𝑘) ∈ ℝ ∧ ((𝐵↑𝑛) ∈ ℝ ∧ 0 < (𝐵↑𝑛))) → ((((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛)))) |
139 | 74, 40, 77, 94, 138 | syl112anc 1375 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((((𝐵 − 1) ·
(𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛)))) |
140 | 137, 139 | mpbird 260 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘)) |
141 | 36, 78, 40, 120, 140 | lttrd 10879 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (𝐵↑𝑘)) |
142 | 27, 36, 40, 71, 141 | lelttrd 10876 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐴 · 𝑘) < (𝐵↑𝑘)) |
143 | 142 | ralrimiva 3096 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∀𝑘 ∈ (ℤ≥‘(2
· 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)) |
144 | | fveq2 6674 |
. . . . 5
⊢ (𝑗 = (2 · 𝑛) →
(ℤ≥‘𝑗) = (ℤ≥‘(2 ·
𝑛))) |
145 | 144 | raleqdv 3316 |
. . . 4
⊢ (𝑗 = (2 · 𝑛) → (∀𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘) ↔ ∀𝑘 ∈ (ℤ≥‘(2
· 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘))) |
146 | 145 | rspcev 3526 |
. . 3
⊢ (((2
· 𝑛) ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘(2
· 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) |
147 | 18, 143, 146 | syl2anc 587 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) |
148 | 13, 147 | rexlimddv 3201 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ∃𝑗 ∈ ℕ0
∀𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) |