| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2re 12340 | . . . . 5
⊢ 2 ∈
ℝ | 
| 2 |  | simp1 1137 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐴 ∈ ℝ) | 
| 3 |  | remulcl 11240 | . . . . 5
⊢ ((2
∈ ℝ ∧ 𝐴
∈ ℝ) → (2 · 𝐴) ∈ ℝ) | 
| 4 | 1, 2, 3 | sylancr 587 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (2 · 𝐴) ∈
ℝ) | 
| 5 |  | simp3 1139 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 1 < 𝐵) | 
| 6 |  | 1re 11261 | . . . . . 6
⊢ 1 ∈
ℝ | 
| 7 |  | simp2 1138 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐵 ∈ ℝ) | 
| 8 |  | difrp 13073 | . . . . . 6
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ) → (1 < 𝐵 ↔ (𝐵 − 1) ∈
ℝ+)) | 
| 9 | 6, 7, 8 | sylancr 587 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (1 < 𝐵 ↔ (𝐵 − 1) ∈
ℝ+)) | 
| 10 | 5, 9 | mpbid 232 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵 − 1) ∈
ℝ+) | 
| 11 | 4, 10 | rerpdivcld 13108 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ((2 ·
𝐴) / (𝐵 − 1)) ∈
ℝ) | 
| 12 |  | expnbnd 14271 | . . 3
⊢ ((((2
· 𝐴) / (𝐵 − 1)) ∈ ℝ
∧ 𝐵 ∈ ℝ
∧ 1 < 𝐵) →
∃𝑛 ∈ ℕ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛)) | 
| 13 | 11, 7, 5, 12 | syl3anc 1373 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ∃𝑛 ∈ ℕ ((2 ·
𝐴) / (𝐵 − 1)) < (𝐵↑𝑛)) | 
| 14 |  | 2nn0 12543 | . . . 4
⊢ 2 ∈
ℕ0 | 
| 15 |  | nnnn0 12533 | . . . . 5
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) | 
| 16 | 15 | ad2antrl 728 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ0) | 
| 17 |  | nn0mulcl 12562 | . . . 4
⊢ ((2
∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℕ0) | 
| 18 | 14, 16, 17 | sylancr 587 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈
ℕ0) | 
| 19 | 2 | ad2antrr 726 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐴 ∈
ℝ) | 
| 20 |  | 2nn 12339 | . . . . . . . . 9
⊢ 2 ∈
ℕ | 
| 21 |  | simprl 771 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ) | 
| 22 |  | nnmulcl 12290 | . . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ) → (2 · 𝑛) ∈ ℕ) | 
| 23 | 20, 21, 22 | sylancr 587 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ) | 
| 24 |  | eluznn 12960 | . . . . . . . 8
⊢ (((2
· 𝑛) ∈ ℕ
∧ 𝑘 ∈
(ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ) | 
| 25 | 23, 24 | sylan 580 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℕ) | 
| 26 | 25 | nnred 12281 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℝ) | 
| 27 | 19, 26 | remulcld 11291 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐴 · 𝑘) ∈ ℝ) | 
| 28 |  | 0re 11263 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 29 |  | ifcl 4571 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ) | 
| 30 | 19, 28, 29 | sylancl 586 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → if(0
≤ 𝐴, 𝐴, 0) ∈ ℝ) | 
| 31 |  | remulcl 11240 | . . . . . . 7
⊢ ((2
∈ ℝ ∧ if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ) → (2 · if(0
≤ 𝐴, 𝐴, 0)) ∈ ℝ) | 
| 32 | 1, 30, 31 | sylancr 587 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· if(0 ≤ 𝐴, 𝐴, 0)) ∈
ℝ) | 
| 33 |  | simplrl 777 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑛 ∈
ℕ) | 
| 34 | 33 | nnred 12281 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑛 ∈
ℝ) | 
| 35 | 26, 34 | resubcld 11691 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈ ℝ) | 
| 36 | 32, 35 | remulcld 11291 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) ∈ ℝ) | 
| 37 | 7 | ad2antrr 726 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐵 ∈
ℝ) | 
| 38 | 25 | nnnn0d 12587 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℕ0) | 
| 39 |  | reexpcl 14119 | . . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑𝑘) ∈
ℝ) | 
| 40 | 37, 38, 39 | syl2anc 584 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑𝑘) ∈ ℝ) | 
| 41 |  | remulcl 11240 | . . . . . . . 8
⊢ ((2
∈ ℝ ∧ (𝑘
− 𝑛) ∈ ℝ)
→ (2 · (𝑘
− 𝑛)) ∈
ℝ) | 
| 42 | 1, 35, 41 | sylancr 587 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· (𝑘 − 𝑛)) ∈
ℝ) | 
| 43 | 38 | nn0ge0d 12590 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 ≤
𝑘) | 
| 44 |  | max1 13227 | . . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0)) | 
| 45 | 28, 19, 44 | sylancr 587 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 ≤
if(0 ≤ 𝐴, 𝐴, 0)) | 
| 46 |  | remulcl 11240 | . . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 𝑛
∈ ℝ) → (2 · 𝑛) ∈ ℝ) | 
| 47 | 1, 34, 46 | sylancr 587 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑛) ∈
ℝ) | 
| 48 |  | eluzle 12891 | . . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘(2 · 𝑛)) → (2 · 𝑛) ≤ 𝑘) | 
| 49 | 48 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑛) ≤ 𝑘) | 
| 50 | 47, 26, 26, 49 | leadd2dd 11878 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (𝑘 + 𝑘)) | 
| 51 | 26 | recnd 11289 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℂ) | 
| 52 | 51 | 2timesd 12509 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑘) = (𝑘 + 𝑘)) | 
| 53 | 50, 52 | breqtrrd 5171 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘)) | 
| 54 |  | remulcl 11240 | . . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 𝑘
∈ ℝ) → (2 · 𝑘) ∈ ℝ) | 
| 55 | 1, 26, 54 | sylancr 587 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑘) ∈
ℝ) | 
| 56 |  | leaddsub 11739 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧ (2
· 𝑛) ∈ ℝ
∧ (2 · 𝑘) ∈
ℝ) → ((𝑘 + (2
· 𝑛)) ≤ (2
· 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛)))) | 
| 57 | 26, 47, 55, 56 | syl3anc 1373 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛)))) | 
| 58 | 53, 57 | mpbid 232 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))) | 
| 59 |  | 2cnd 12344 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 2
∈ ℂ) | 
| 60 | 34 | recnd 11289 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑛 ∈
ℂ) | 
| 61 | 59, 51, 60 | subdid 11719 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛))) | 
| 62 | 58, 61 | breqtrrd 5171 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ≤ (2 · (𝑘 − 𝑛))) | 
| 63 |  | max2 13229 | . . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → 𝐴
≤ if(0 ≤ 𝐴, 𝐴, 0)) | 
| 64 | 28, 19, 63 | sylancr 587 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐴 ≤ if(0 ≤ 𝐴, 𝐴, 0)) | 
| 65 | 26, 42, 19, 30, 43, 45, 62, 64 | lemul12bd 12211 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 · 𝐴) ≤ ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0))) | 
| 66 | 19 | recnd 11289 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐴 ∈
ℂ) | 
| 67 | 66, 51 | mulcomd 11282 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐴 · 𝑘) = (𝑘 · 𝐴)) | 
| 68 | 30 | recnd 11289 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → if(0
≤ 𝐴, 𝐴, 0) ∈ ℂ) | 
| 69 | 35 | recnd 11289 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈ ℂ) | 
| 70 | 59, 68, 69 | mul32d 11471 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) = ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0))) | 
| 71 | 65, 67, 70 | 3brtr4d 5175 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐴 · 𝑘) ≤ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛))) | 
| 72 | 10 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵 − 1) ∈
ℝ+) | 
| 73 | 72 | rpred 13077 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵 − 1) ∈
ℝ) | 
| 74 | 73, 35 | remulcld 11291 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝑘 − 𝑛)) ∈
ℝ) | 
| 75 | 33 | nnnn0d 12587 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑛 ∈
ℕ0) | 
| 76 |  | reexpcl 14119 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℕ0)
→ (𝐵↑𝑛) ∈
ℝ) | 
| 77 | 37, 75, 76 | syl2anc 584 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑𝑛) ∈ ℝ) | 
| 78 | 74, 77 | remulcld 11291 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝑘 − 𝑛)) · (𝐵↑𝑛)) ∈ ℝ) | 
| 79 |  | simplrr 778 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛)) | 
| 80 | 1, 19, 3 | sylancr 587 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝐴) ∈
ℝ) | 
| 81 | 80, 77, 72 | ltdivmuld 13128 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛) ↔ (2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)))) | 
| 82 | 79, 81 | mpbid 232 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛))) | 
| 83 | 5 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 1 <
𝐵) | 
| 84 |  | posdif 11756 | . . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1))) | 
| 85 | 6, 37, 84 | sylancr 587 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (1
< 𝐵 ↔ 0 < (𝐵 − 1))) | 
| 86 | 83, 85 | mpbid 232 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
(𝐵 −
1)) | 
| 87 | 33 | nnzd 12640 | . . . . . . . . . . 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 11785 | . . . . . . . . . . . . 13
⊢ 0 <
1 | 
| 91 | 90 | a1i 11 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
1) | 
| 92 | 88, 89, 37, 91, 83 | lttrd 11422 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
𝐵) | 
| 93 |  | expgt0 14136 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 0 <
𝐵) → 0 < (𝐵↑𝑛)) | 
| 94 | 37, 87, 92, 93 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
(𝐵↑𝑛)) | 
| 95 | 73, 77, 86, 94 | mulgt0d 11416 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
((𝐵 − 1) ·
(𝐵↑𝑛))) | 
| 96 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 𝐴) = (2 · if(0 ≤ 𝐴, 𝐴, 0))) | 
| 97 | 96 | breq1d 5153 | . . . . . . . . . 10
⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → ((2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)))) | 
| 98 |  | 2t0e0 12435 | . . . . . . . . . . . 12
⊢ (2
· 0) = 0 | 
| 99 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (0 = if(0
≤ 𝐴, 𝐴, 0) → (2 · 0) = (2 ·
if(0 ≤ 𝐴, 𝐴, 0))) | 
| 100 | 98, 99 | eqtr3id 2791 | . . . . . . . . . . 11
⊢ (0 = if(0
≤ 𝐴, 𝐴, 0) → 0 = (2 · if(0 ≤ 𝐴, 𝐴, 0))) | 
| 101 | 100 | breq1d 5153 | . . . . . . . . . 10
⊢ (0 = if(0
≤ 𝐴, 𝐴, 0) → (0 < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)))) | 
| 102 | 97, 101 | ifboth 4565 | . . . . . . . . 9
⊢ (((2
· 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ∧ 0 < ((𝐵 − 1) · (𝐵↑𝑛))) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))) | 
| 103 | 82, 95, 102 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))) | 
| 104 | 73, 77 | remulcld 11291 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝐵↑𝑛)) ∈ ℝ) | 
| 105 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
(ℤ≥‘(2 · 𝑛))) | 
| 106 | 60 | 2timesd 12509 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (2
· 𝑛) = (𝑛 + 𝑛)) | 
| 107 | 106 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(ℤ≥‘(2 · 𝑛)) = (ℤ≥‘(𝑛 + 𝑛))) | 
| 108 | 105, 107 | eleqtrd 2843 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
(ℤ≥‘(𝑛 + 𝑛))) | 
| 109 |  | eluzsub 12908 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘(𝑛 + 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ≥‘𝑛)) | 
| 110 | 87, 87, 108, 109 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ≥‘𝑛)) | 
| 111 |  | eluznn 12960 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ (𝑘 − 𝑛) ∈ (ℤ≥‘𝑛)) → (𝑘 − 𝑛) ∈ ℕ) | 
| 112 | 33, 110, 111 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈ ℕ) | 
| 113 | 112 | nngt0d 12315 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 <
(𝑘 − 𝑛)) | 
| 114 |  | ltmul1 12117 | . . . . . . . . 9
⊢ (((2
· if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ ∧
((𝐵 − 1) ·
(𝐵↑𝑛)) ∈ ℝ ∧ ((𝑘 − 𝑛) ∈ ℝ ∧ 0 < (𝑘 − 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)))) | 
| 115 | 32, 104, 35, 113, 114 | syl112anc 1376 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)))) | 
| 116 | 103, 115 | mpbid 232 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛))) | 
| 117 | 73 | recnd 11289 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵 − 1) ∈
ℂ) | 
| 118 | 77 | recnd 11289 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑𝑛) ∈ ℂ) | 
| 119 | 117, 118,
69 | mul32d 11471 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝐵↑𝑛)) · (𝑘 − 𝑛)) = (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛))) | 
| 120 | 116, 119 | breqtrd 5169 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛))) | 
| 121 |  | peano2re 11434 | . . . . . . . . . 10
⊢ (((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ) | 
| 122 | 74, 121 | syl 17 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝑘 − 𝑛)) + 1) ∈
ℝ) | 
| 123 | 112 | nnnn0d 12587 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝑘 − 𝑛) ∈
ℕ0) | 
| 124 |  | reexpcl 14119 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ0) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ) | 
| 125 | 37, 123, 124 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ) | 
| 126 | 74 | ltp1d 12198 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) + 1)) | 
| 127 | 88, 37, 92 | ltled 11409 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 0 ≤
𝐵) | 
| 128 |  | bernneq2 14269 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ0 ∧ 0 ≤
𝐵) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛))) | 
| 129 | 37, 123, 127, 128 | syl3anc 1373 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛))) | 
| 130 | 74, 122, 125, 126, 129 | ltletrd 11421 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝑘 − 𝑛)) < (𝐵↑(𝑘 − 𝑛))) | 
| 131 | 37 | recnd 11289 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐵 ∈
ℂ) | 
| 132 | 92 | gt0ne0d 11827 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝐵 ≠ 0) | 
| 133 |  | eluzelz 12888 | . . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘(2 · 𝑛)) → 𝑘 ∈ ℤ) | 
| 134 | 133 | adantl 481 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → 𝑘 ∈
ℤ) | 
| 135 |  | expsub 14151 | . . . . . . . . 9
⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛))) | 
| 136 | 131, 132,
134, 87, 135 | syl22anc 839 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛))) | 
| 137 | 130, 136 | breqtrd 5169 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((𝐵 − 1) ·
(𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛))) | 
| 138 |  | ltmuldiv 12141 | . . . . . . . 8
⊢ ((((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ ∧ (𝐵↑𝑘) ∈ ℝ ∧ ((𝐵↑𝑛) ∈ ℝ ∧ 0 < (𝐵↑𝑛))) → ((((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛)))) | 
| 139 | 74, 40, 77, 94, 138 | syl112anc 1376 | . . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
((((𝐵 − 1) ·
(𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛)))) | 
| 140 | 137, 139 | mpbird 257 | . . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) →
(((𝐵 − 1) ·
(𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘)) | 
| 141 | 36, 78, 40, 120, 140 | lttrd 11422 | . . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → ((2
· if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (𝐵↑𝑘)) | 
| 142 | 27, 36, 40, 71, 141 | lelttrd 11419 | . . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2
· 𝑛))) → (𝐴 · 𝑘) < (𝐵↑𝑘)) | 
| 143 | 142 | ralrimiva 3146 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∀𝑘 ∈ (ℤ≥‘(2
· 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)) | 
| 144 |  | fveq2 6906 | . . . . 5
⊢ (𝑗 = (2 · 𝑛) →
(ℤ≥‘𝑗) = (ℤ≥‘(2 ·
𝑛))) | 
| 145 | 144 | raleqdv 3326 | . . . 4
⊢ (𝑗 = (2 · 𝑛) → (∀𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘) ↔ ∀𝑘 ∈ (ℤ≥‘(2
· 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘))) | 
| 146 | 145 | rspcev 3622 | . . 3
⊢ (((2
· 𝑛) ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘(2
· 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) | 
| 147 | 18, 143, 146 | syl2anc 584 | . 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2
· 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) | 
| 148 | 13, 147 | rexlimddv 3161 | 1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ∃𝑗 ∈ ℕ0
∀𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) |