| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cvgdvgrat.w | . . . . . . . . 9
⊢ 𝑊 =
(ℤ≥‘𝑁) | 
| 2 |  | eqid 2737 | . . . . . . . . 9
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) | 
| 3 |  | elioore 13417 | . . . . . . . . . 10
⊢ (𝑟 ∈ (𝐿(,)1) → 𝑟 ∈ ℝ) | 
| 4 | 3 | ad3antlr 731 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑟 ∈ ℝ) | 
| 5 |  | cvgdvgrat.n | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ 𝑍) | 
| 6 |  | cvgdvgrat.z | . . . . . . . . . . . . . . . . 17
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 7 | 5, 6 | eleqtrdi 2851 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 8 |  | eluzelz 12888 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | 
| 9 | 7, 8 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 10 |  | cvgdvgrat.cvg | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ⇝ 𝐿) | 
| 11 |  | cvgdvgrat.r | . . . . . . . . . . . . . . . . . 18
⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) | 
| 12 | 11 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))) | 
| 13 | 1 | peano2uzs 12944 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑊 → (𝑘 + 1) ∈ 𝑊) | 
| 14 |  | ovex 7464 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 + 1) ∈ V | 
| 15 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = (𝑘 + 1) → (𝑖 ∈ 𝑊 ↔ (𝑘 + 1) ∈ 𝑊)) | 
| 16 | 15 | anbi2d 630 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = (𝑘 + 1) → ((𝜑 ∧ 𝑖 ∈ 𝑊) ↔ (𝜑 ∧ (𝑘 + 1) ∈ 𝑊))) | 
| 17 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = (𝑘 + 1) → (𝐹‘𝑖) = (𝐹‘(𝑘 + 1))) | 
| 18 | 17 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝑖) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ)) | 
| 19 | 16, 18 | imbi12d 344 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = (𝑘 + 1) → (((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ))) | 
| 20 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝑊 ↔ 𝑖 ∈ 𝑊)) | 
| 21 | 20 | anbi2d 630 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ 𝑊) ↔ (𝜑 ∧ 𝑖 ∈ 𝑊))) | 
| 22 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖)) | 
| 23 | 22 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑖) ∈ ℂ)) | 
| 24 | 21, 23 | imbi12d 344 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ))) | 
| 25 | 1 | eleq2i 2833 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ 𝑊 ↔ 𝑘 ∈ (ℤ≥‘𝑁)) | 
| 26 | 6 | uztrn2 12897 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → 𝑘 ∈ 𝑍) | 
| 27 | 5, 26 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → 𝑘 ∈ 𝑍) | 
| 28 | 25, 27 | sylan2b 594 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑍) | 
| 29 |  | cvgdvgrat.c | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) | 
| 30 | 28, 29 | syldan 591 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ) | 
| 31 | 24, 30 | chvarvv 1998 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ) | 
| 32 | 14, 19, 31 | vtocl 3558 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ) | 
| 33 | 13, 32 | sylan2 593 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ) | 
| 34 |  | cvgdvgrat.n0 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) | 
| 35 | 33, 30, 34 | divcld 12043 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ) | 
| 36 | 35 | abscld 15475 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ) | 
| 37 | 12, 36 | fvmpt2d 7029 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) | 
| 38 | 37, 36 | eqeltrd 2841 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) ∈ ℝ) | 
| 39 | 1, 9, 10, 38 | climrecl 15619 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ ℝ) | 
| 40 | 39 | rexrd 11311 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈
ℝ*) | 
| 41 |  | 1xr 11320 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℝ* | 
| 42 |  | elioo2 13428 | . . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℝ*
∧ 1 ∈ ℝ*) → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1))) | 
| 43 | 40, 41, 42 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1))) | 
| 44 | 43 | biimpa 476 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟 ∧ 𝑟 < 1)) | 
| 45 | 44 | simp3d 1145 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑟 < 1) | 
| 46 | 45 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑟 < 1) | 
| 47 |  | simplr 769 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → 𝑛 ∈ 𝑊) | 
| 48 | 31 | ex 412 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ)) | 
| 49 | 48 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ)) | 
| 50 | 49 | imp 406 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ) | 
| 51 |  | fvoveq1 7454 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑖 + 1))) | 
| 52 | 51 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘(𝐹‘(𝑖 + 1)))) | 
| 53 | 22 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (abs‘(𝐹‘𝑘)) = (abs‘(𝐹‘𝑖))) | 
| 54 | 53 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (𝑟 · (abs‘(𝐹‘𝑘))) = (𝑟 · (abs‘(𝐹‘𝑖)))) | 
| 55 | 52, 54 | breq12d 5156 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → ((abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))) ↔ (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖))))) | 
| 56 | 55 | rspccva 3621 | . . . . . . . . . 10
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖)))) | 
| 57 | 56 | adantll 714 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑖)))) | 
| 58 | 1, 2, 4, 46, 47, 50, 57 | cvgrat 15919 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) | 
| 59 | 9 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑁 ∈ ℤ) | 
| 60 | 44 | simp2d 1144 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝐿 < 𝑟) | 
| 61 |  | difrp 13073 | . . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐿 < 𝑟 ↔ (𝑟 − 𝐿) ∈
ℝ+)) | 
| 62 | 39, 3, 61 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝐿 < 𝑟 ↔ (𝑟 − 𝐿) ∈
ℝ+)) | 
| 63 | 60, 62 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (𝑟 − 𝐿) ∈
ℝ+) | 
| 64 | 37 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) | 
| 65 | 10 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → 𝑅 ⇝ 𝐿) | 
| 66 | 1, 59, 63, 64, 65 | climi2 15547 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) | 
| 67 | 1 | uztrn2 12897 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ 𝑊) | 
| 68 | 67, 33 | sylan2 593 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ≥‘𝑛))) → (𝐹‘(𝑘 + 1)) ∈ ℂ) | 
| 69 | 68 | anassrs 467 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ) | 
| 70 | 69 | adantllr 719 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ) | 
| 71 | 70 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘(𝑘 + 1)) ∈ ℂ) | 
| 72 | 71 | abscld 15475 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ) | 
| 73 | 3 | ad4antlr 733 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝑟 ∈ ℝ) | 
| 74 | 67, 30 | sylan2 593 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ≥‘𝑛))) → (𝐹‘𝑘) ∈ ℂ) | 
| 75 | 74 | anassrs 467 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ) | 
| 76 | 75 | adantllr 719 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ) | 
| 77 | 76 | adantr 480 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘𝑘) ∈ ℂ) | 
| 78 | 77 | abscld 15475 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℝ) | 
| 79 | 73, 78 | remulcld 11291 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝑟 · (abs‘(𝐹‘𝑘))) ∈ ℝ) | 
| 80 | 67, 34 | sylan2 593 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑘 ∈ (ℤ≥‘𝑛))) → (𝐹‘𝑘) ≠ 0) | 
| 81 | 80 | anassrs 467 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ≠ 0) | 
| 82 | 81 | adantllr 719 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ≠ 0) | 
| 83 | 82 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (𝐹‘𝑘) ≠ 0) | 
| 84 | 71, 77, 83 | absdivd 15494 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘)))) | 
| 85 | 70, 76, 82 | divcld 12043 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ) | 
| 86 | 85 | abscld 15475 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ) | 
| 87 | 39 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐿 ∈ ℝ) | 
| 88 | 86, 87 | resubcld 11691 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∈ ℝ) | 
| 89 | 3 | ad3antlr 731 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ ℝ) | 
| 90 | 89, 87 | resubcld 11691 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝑟 − 𝐿) ∈ ℝ) | 
| 91 | 88, 90 | absltd 15468 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) →
((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) ↔ (-(𝑟 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿)))) | 
| 92 | 91 | simplbda 499 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿)) | 
| 93 | 71, 77, 83 | divcld 12043 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ) | 
| 94 | 93 | abscld 15475 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ) | 
| 95 | 39 | ad4antr 732 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝐿 ∈ ℝ) | 
| 96 | 94, 73, 95 | ltsub1d 11872 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) < 𝑟 ↔ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝑟 − 𝐿))) | 
| 97 | 92, 96 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) < 𝑟) | 
| 98 | 84, 97 | eqbrtrrd 5167 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))) < 𝑟) | 
| 99 | 77, 83 | absrpcld 15487 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈
ℝ+) | 
| 100 | 72, 73, 99 | ltdivmuld 13128 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))) < 𝑟 ↔ (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹‘𝑘)) · 𝑟))) | 
| 101 | 98, 100 | mpbid 232 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹‘𝑘)) · 𝑟)) | 
| 102 | 99 | rpcnd 13079 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘𝑘)) ∈ ℂ) | 
| 103 | 73 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → 𝑟 ∈ ℂ) | 
| 104 | 102, 103 | mulcomd 11282 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → ((abs‘(𝐹‘𝑘)) · 𝑟) = (𝑟 · (abs‘(𝐹‘𝑘)))) | 
| 105 | 101, 104 | breqtrd 5169 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < (𝑟 · (abs‘(𝐹‘𝑘)))) | 
| 106 | 72, 79, 105 | ltled 11409 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) | 
| 107 | 106 | ex 412 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) →
((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))) | 
| 108 | 107 | ralimdva 3167 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))) | 
| 109 | 108 | reximdva 3168 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝑟 − 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘))))) | 
| 110 | 66, 109 | mpd 15 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹‘𝑘)))) | 
| 111 | 58, 110 | r19.29a 3162 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐿(,)1)) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) | 
| 112 | 111 | ralrimiva 3146 | . . . . . 6
⊢ (𝜑 → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ) | 
| 113 | 112 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐿 < 1) → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ) | 
| 114 |  | ioon0 13413 | . . . . . . . 8
⊢ ((𝐿 ∈ ℝ*
∧ 1 ∈ ℝ*) → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1)) | 
| 115 | 40, 41, 114 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1)) | 
| 116 | 115 | biimpar 477 | . . . . . 6
⊢ ((𝜑 ∧ 𝐿 < 1) → (𝐿(,)1) ≠ ∅) | 
| 117 |  | r19.3rzv 4499 | . . . . . 6
⊢ ((𝐿(,)1) ≠ ∅ →
(seq𝑁( + , 𝐹) ∈ dom ⇝ ↔
∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )) | 
| 118 | 116, 117 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝐿 < 1) → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )) | 
| 119 | 113, 118 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ 𝐿 < 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) | 
| 120 | 6, 5, 29 | iserex 15693 | . . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) | 
| 121 | 120 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐿 < 1) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) | 
| 122 | 119, 121 | mpbird 257 | . . 3
⊢ ((𝜑 ∧ 𝐿 < 1) → seq𝑀( + , 𝐹) ∈ dom ⇝ ) | 
| 123 | 122 | ex 412 | . 2
⊢ (𝜑 → (𝐿 < 1 → seq𝑀( + , 𝐹) ∈ dom ⇝ )) | 
| 124 |  | cvgdvgrat.n1 | . . . . . 6
⊢ (𝜑 → 𝐿 ≠ 1) | 
| 125 |  | 1red 11262 | . . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) | 
| 126 | 39, 125 | lttri2d 11400 | . . . . . 6
⊢ (𝜑 → (𝐿 ≠ 1 ↔ (𝐿 < 1 ∨ 1 < 𝐿))) | 
| 127 | 124, 126 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝐿 < 1 ∨ 1 < 𝐿)) | 
| 128 | 127 | orcanai 1005 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 < 1) → 1 < 𝐿) | 
| 129 |  | simplr 769 | . . . . . . . 8
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝑛 ∈ 𝑊) | 
| 130 |  | cvgdvgrat.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑉) | 
| 131 | 130 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝐹 ∈ 𝑉) | 
| 132 | 48 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → (𝑖 ∈ 𝑊 → (𝐹‘𝑖) ∈ ℂ)) | 
| 133 | 132 | imp 406 | . . . . . . . 8
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ∈ ℂ) | 
| 134 | 1 | uztrn2 12897 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ 𝑊 ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝑖 ∈ 𝑊) | 
| 135 | 22 | neeq1d 3000 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ≠ 0 ↔ (𝐹‘𝑖) ≠ 0)) | 
| 136 | 21, 135 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ≠ 0))) | 
| 137 | 136, 34 | chvarvv 1998 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑊) → (𝐹‘𝑖) ≠ 0) | 
| 138 | 134, 137 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ 𝑊 ∧ 𝑖 ∈ (ℤ≥‘𝑛))) → (𝐹‘𝑖) ≠ 0) | 
| 139 | 138 | anassrs 467 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑊) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑖) ≠ 0) | 
| 140 | 139 | adantllr 719 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑖) ≠ 0) | 
| 141 | 140 | adantlr 715 | . . . . . . . 8
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑖) ≠ 0) | 
| 142 | 53, 52 | breq12d 5156 | . . . . . . . . . 10
⊢ (𝑘 = 𝑖 → ((abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ↔ (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))) | 
| 143 | 142 | rspccva 3621 | . . . . . . . . 9
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1)))) | 
| 144 | 143 | adantll 714 | . . . . . . . 8
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐹‘𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1)))) | 
| 145 | 1, 2, 129, 131, 133, 141, 144 | dvgrat 44331 | . . . . . . 7
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → seq𝑁( + , 𝐹) ∉ dom ⇝ ) | 
| 146 | 9 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 1 < 𝐿) → 𝑁 ∈ ℤ) | 
| 147 |  | 1re 11261 | . . . . . . . . . . 11
⊢ 1 ∈
ℝ | 
| 148 |  | difrp 13073 | . . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 𝐿
∈ ℝ) → (1 < 𝐿 ↔ (𝐿 − 1) ∈
ℝ+)) | 
| 149 | 147, 39, 148 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (1 < 𝐿 ↔ (𝐿 − 1) ∈
ℝ+)) | 
| 150 | 149 | biimpa 476 | . . . . . . . . 9
⊢ ((𝜑 ∧ 1 < 𝐿) → (𝐿 − 1) ∈
ℝ+) | 
| 151 | 37 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐿) ∧ 𝑘 ∈ 𝑊) → (𝑅‘𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) | 
| 152 | 10 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 1 < 𝐿) → 𝑅 ⇝ 𝐿) | 
| 153 | 1, 146, 150, 151, 152 | climi2 15547 | . . . . . . . 8
⊢ ((𝜑 ∧ 1 < 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) | 
| 154 | 75 | adantllr 719 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ) | 
| 155 | 154 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘𝑘) ∈ ℂ) | 
| 156 | 155 | abscld 15475 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℝ) | 
| 157 | 69 | adantllr 719 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ) | 
| 158 | 157 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘(𝑘 + 1)) ∈ ℂ) | 
| 159 | 158 | abscld 15475 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ) | 
| 160 | 81 | adantllr 719 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ≠ 0) | 
| 161 | 160 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘𝑘) ≠ 0) | 
| 162 | 155, 161 | absrpcld 15487 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈
ℝ+) | 
| 163 | 162 | rpcnd 13079 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ∈ ℂ) | 
| 164 | 163 | mullidd 11279 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 ·
(abs‘(𝐹‘𝑘))) = (abs‘(𝐹‘𝑘))) | 
| 165 | 39 | ad4antr 732 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℝ) | 
| 166 | 165 | recnd 11289 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℂ) | 
| 167 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈
ℂ) | 
| 168 | 166, 167 | negsubdi2d 11636 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) = (1 − 𝐿)) | 
| 169 | 157, 154,
160 | divcld 12043 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ) | 
| 170 | 169 | abscld 15475 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ) | 
| 171 | 39 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐿 ∈ ℝ) | 
| 172 | 170, 171 | resubcld 11691 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∈ ℝ) | 
| 173 |  | 1red 11262 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 1 ∈
ℝ) | 
| 174 | 171, 173 | resubcld 11691 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐿 − 1) ∈ ℝ) | 
| 175 | 172, 174 | absltd 15468 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) →
((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) ↔ (-(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿) < (𝐿 − 1)))) | 
| 176 | 175 | simprbda 498 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) | 
| 177 | 168, 176 | eqbrtrrd 5167 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) | 
| 178 |  | 1red 11262 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈
ℝ) | 
| 179 | 158, 155,
161 | divcld 12043 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) ∈ ℂ) | 
| 180 | 179 | abscld 15475 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ∈ ℝ) | 
| 181 | 178, 180,
165 | ltsub1d 11872 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 <
(abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) ↔ (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿))) | 
| 182 | 177, 181 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 <
(abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) | 
| 183 | 158, 155,
161 | absdivd 15494 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘)))) | 
| 184 | 182, 183 | breqtrd 5169 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 <
((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘)))) | 
| 185 | 178, 159,
162 | ltmuldivd 13124 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → ((1 ·
(abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘(𝑘 + 1))) ↔ 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹‘𝑘))))) | 
| 186 | 184, 185 | mpbird 257 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 ·
(abs‘(𝐹‘𝑘))) < (abs‘(𝐹‘(𝑘 + 1)))) | 
| 187 | 164, 186 | eqbrtrrd 5167 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) < (abs‘(𝐹‘(𝑘 + 1)))) | 
| 188 | 156, 159,
187 | ltled 11409 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 1 <
𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) ∧
(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) | 
| 189 | 188 | ex 412 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) →
((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))) | 
| 190 | 189 | ralimdva 3167 | . . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐿) ∧ 𝑛 ∈ 𝑊) → (∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))) | 
| 191 | 190 | reximdva 3168 | . . . . . . . 8
⊢ ((𝜑 ∧ 1 < 𝐿) → (∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) − 𝐿)) < (𝐿 − 1) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))) | 
| 192 | 153, 191 | mpd 15 | . . . . . . 7
⊢ ((𝜑 ∧ 1 < 𝐿) → ∃𝑛 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) | 
| 193 | 145, 192 | r19.29a 3162 | . . . . . 6
⊢ ((𝜑 ∧ 1 < 𝐿) → seq𝑁( + , 𝐹) ∉ dom ⇝ ) | 
| 194 |  | df-nel 3047 | . . . . . 6
⊢ (seq𝑁( + , 𝐹) ∉ dom ⇝ ↔ ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ ) | 
| 195 | 193, 194 | sylib 218 | . . . . 5
⊢ ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ ) | 
| 196 | 120 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 1 < 𝐿) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) | 
| 197 | 195, 196 | mtbird 325 | . . . 4
⊢ ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ ) | 
| 198 | 128, 197 | syldan 591 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐿 < 1) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ ) | 
| 199 | 198 | ex 412 | . 2
⊢ (𝜑 → (¬ 𝐿 < 1 → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )) | 
| 200 | 123, 199 | impcon4bid 227 | 1
⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ )) |