Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvgdvgrat Structured version   Visualization version   GIF version

Theorem cvgdvgrat 44332
Description: Ratio test for convergence and divergence of a complex infinite series. If the ratio 𝑅 of the absolute values of successive terms in an infinite sequence 𝐹 converges to less than one, then the infinite sum of the terms of 𝐹 converges to a complex number; and if 𝑅 converges greater then the sum diverges. This combined form of cvgrat 15919 and dvgrat 44331 directly uses the limit of the ratio.

(It also demonstrates how to use climi2 15547 and absltd 15468 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15468, and how to use r19.29a 3162 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3155 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3155.) (Contributed by Steve Rodriguez, 28-Feb-2020.)

Hypotheses
Ref Expression
cvgdvgrat.z 𝑍 = (ℤ𝑀)
cvgdvgrat.w 𝑊 = (ℤ𝑁)
cvgdvgrat.n (𝜑𝑁𝑍)
cvgdvgrat.f (𝜑𝐹𝑉)
cvgdvgrat.c ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
cvgdvgrat.n0 ((𝜑𝑘𝑊) → (𝐹𝑘) ≠ 0)
cvgdvgrat.r 𝑅 = (𝑘𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
cvgdvgrat.cvg (𝜑𝑅𝐿)
cvgdvgrat.n1 (𝜑𝐿 ≠ 1)
Assertion
Ref Expression
cvgdvgrat (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
Distinct variable groups:   𝜑,𝑘   𝑘,𝐹   𝑘,𝐿   𝑘,𝑁   𝑘,𝑊   𝑅,𝑘   𝑘,𝑀   𝑘,𝑍
Allowed substitution hint:   𝑉(𝑘)

Proof of Theorem cvgdvgrat
Dummy variables 𝑖 𝑛 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvgdvgrat.w . . . . . . . . 9 𝑊 = (ℤ𝑁)
2 eqid 2737 . . . . . . . . 9 (ℤ𝑛) = (ℤ𝑛)
3 elioore 13417 . . . . . . . . . 10 (𝑟 ∈ (𝐿(,)1) → 𝑟 ∈ ℝ)
43ad3antlr 731 . . . . . . . . 9 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → 𝑟 ∈ ℝ)
5 cvgdvgrat.n . . . . . . . . . . . . . . . . 17 (𝜑𝑁𝑍)
6 cvgdvgrat.z . . . . . . . . . . . . . . . . 17 𝑍 = (ℤ𝑀)
75, 6eleqtrdi 2851 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝑀))
8 eluzelz 12888 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
97, 8syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℤ)
10 cvgdvgrat.cvg . . . . . . . . . . . . . . 15 (𝜑𝑅𝐿)
11 cvgdvgrat.r . . . . . . . . . . . . . . . . . 18 𝑅 = (𝑘𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
1211a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑𝑅 = (𝑘𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘)))))
131peano2uzs 12944 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝑊 → (𝑘 + 1) ∈ 𝑊)
14 ovex 7464 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 + 1) ∈ V
15 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝑖𝑊 ↔ (𝑘 + 1) ∈ 𝑊))
1615anbi2d 630 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑘 + 1) → ((𝜑𝑖𝑊) ↔ (𝜑 ∧ (𝑘 + 1) ∈ 𝑊)))
17 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝐹𝑖) = (𝐹‘(𝑘 + 1)))
1817eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑘 + 1) → ((𝐹𝑖) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
1916, 18imbi12d 344 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = (𝑘 + 1) → (((𝜑𝑖𝑊) → (𝐹𝑖) ∈ ℂ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)))
20 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → (𝑘𝑊𝑖𝑊))
2120anbi2d 630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → ((𝜑𝑘𝑊) ↔ (𝜑𝑖𝑊)))
22 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
2322eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑖) ∈ ℂ))
2421, 23imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑖 → (((𝜑𝑘𝑊) → (𝐹𝑘) ∈ ℂ) ↔ ((𝜑𝑖𝑊) → (𝐹𝑖) ∈ ℂ)))
251eleq2i 2833 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑊𝑘 ∈ (ℤ𝑁))
266uztrn2 12897 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁𝑍𝑘 ∈ (ℤ𝑁)) → 𝑘𝑍)
275, 26sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (ℤ𝑁)) → 𝑘𝑍)
2825, 27sylan2b 594 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘𝑊) → 𝑘𝑍)
29 cvgdvgrat.c . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
3028, 29syldan 591 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘𝑊) → (𝐹𝑘) ∈ ℂ)
3124, 30chvarvv 1998 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝑊) → (𝐹𝑖) ∈ ℂ)
3214, 19, 31vtocl 3558 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
3313, 32sylan2 593 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
34 cvgdvgrat.n0 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑊) → (𝐹𝑘) ≠ 0)
3533, 30, 34divcld 12043 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑊) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
3635abscld 15475 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑊) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
3712, 36fvmpt2d 7029 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑊) → (𝑅𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
3837, 36eqeltrd 2841 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑊) → (𝑅𝑘) ∈ ℝ)
391, 9, 10, 38climrecl 15619 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ ℝ)
4039rexrd 11311 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ℝ*)
41 1xr 11320 . . . . . . . . . . . . 13 1 ∈ ℝ*
42 elioo2 13428 . . . . . . . . . . . . 13 ((𝐿 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟𝑟 < 1)))
4340, 41, 42sylancl 586 . . . . . . . . . . . 12 (𝜑 → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟𝑟 < 1)))
4443biimpa 476 . . . . . . . . . . 11 ((𝜑𝑟 ∈ (𝐿(,)1)) → (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟𝑟 < 1))
4544simp3d 1145 . . . . . . . . . 10 ((𝜑𝑟 ∈ (𝐿(,)1)) → 𝑟 < 1)
4645ad2antrr 726 . . . . . . . . 9 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → 𝑟 < 1)
47 simplr 769 . . . . . . . . 9 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → 𝑛𝑊)
4831ex 412 . . . . . . . . . . 11 (𝜑 → (𝑖𝑊 → (𝐹𝑖) ∈ ℂ))
4948ad3antrrr 730 . . . . . . . . . 10 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → (𝑖𝑊 → (𝐹𝑖) ∈ ℂ))
5049imp 406 . . . . . . . . 9 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) ∧ 𝑖𝑊) → (𝐹𝑖) ∈ ℂ)
51 fvoveq1 7454 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑖 + 1)))
5251fveq2d 6910 . . . . . . . . . . . 12 (𝑘 = 𝑖 → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘(𝐹‘(𝑖 + 1))))
5322fveq2d 6910 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (abs‘(𝐹𝑘)) = (abs‘(𝐹𝑖)))
5453oveq2d 7447 . . . . . . . . . . . 12 (𝑘 = 𝑖 → (𝑟 · (abs‘(𝐹𝑘))) = (𝑟 · (abs‘(𝐹𝑖))))
5552, 54breq12d 5156 . . . . . . . . . . 11 (𝑘 = 𝑖 → ((abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘))) ↔ (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑖)))))
5655rspccva 3621 . . . . . . . . . 10 ((∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘))) ∧ 𝑖 ∈ (ℤ𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑖))))
5756adantll 714 . . . . . . . . 9 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) ∧ 𝑖 ∈ (ℤ𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑖))))
581, 2, 4, 46, 47, 50, 57cvgrat 15919 . . . . . . . 8 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
599adantr 480 . . . . . . . . . 10 ((𝜑𝑟 ∈ (𝐿(,)1)) → 𝑁 ∈ ℤ)
6044simp2d 1144 . . . . . . . . . . 11 ((𝜑𝑟 ∈ (𝐿(,)1)) → 𝐿 < 𝑟)
61 difrp 13073 . . . . . . . . . . . 12 ((𝐿 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐿 < 𝑟 ↔ (𝑟𝐿) ∈ ℝ+))
6239, 3, 61syl2an 596 . . . . . . . . . . 11 ((𝜑𝑟 ∈ (𝐿(,)1)) → (𝐿 < 𝑟 ↔ (𝑟𝐿) ∈ ℝ+))
6360, 62mpbid 232 . . . . . . . . . 10 ((𝜑𝑟 ∈ (𝐿(,)1)) → (𝑟𝐿) ∈ ℝ+)
6437adantlr 715 . . . . . . . . . 10 (((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑘𝑊) → (𝑅𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
6510adantr 480 . . . . . . . . . 10 ((𝜑𝑟 ∈ (𝐿(,)1)) → 𝑅𝐿)
661, 59, 63, 64, 65climi2 15547 . . . . . . . . 9 ((𝜑𝑟 ∈ (𝐿(,)1)) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿))
671uztrn2 12897 . . . . . . . . . . . . . . . . . 18 ((𝑛𝑊𝑘 ∈ (ℤ𝑛)) → 𝑘𝑊)
6867, 33sylan2 593 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛𝑊𝑘 ∈ (ℤ𝑛))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
6968anassrs 467 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
7069adantllr 719 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
7170adantr 480 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
7271abscld 15475 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
733ad4antlr 733 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → 𝑟 ∈ ℝ)
7467, 30sylan2 593 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛𝑊𝑘 ∈ (ℤ𝑛))) → (𝐹𝑘) ∈ ℂ)
7574anassrs 467 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ∈ ℂ)
7675adantllr 719 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ∈ ℂ)
7776adantr 480 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (𝐹𝑘) ∈ ℂ)
7877abscld 15475 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹𝑘)) ∈ ℝ)
7973, 78remulcld 11291 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (𝑟 · (abs‘(𝐹𝑘))) ∈ ℝ)
8067, 34sylan2 593 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛𝑊𝑘 ∈ (ℤ𝑛))) → (𝐹𝑘) ≠ 0)
8180anassrs 467 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ≠ 0)
8281adantllr 719 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ≠ 0)
8382adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (𝐹𝑘) ≠ 0)
8471, 77, 83absdivd 15494 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))))
8570, 76, 82divcld 12043 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
8685abscld 15475 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
8739ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝐿 ∈ ℝ)
8886, 87resubcld 11691 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) ∈ ℝ)
893ad3antlr 731 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑟 ∈ ℝ)
9089, 87resubcld 11691 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑟𝐿) ∈ ℝ)
9188, 90absltd 15468 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿) ↔ (-(𝑟𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) < (𝑟𝐿))))
9291simplbda 499 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) < (𝑟𝐿))
9371, 77, 83divcld 12043 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
9493abscld 15475 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
9539ad4antr 732 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → 𝐿 ∈ ℝ)
9694, 73, 95ltsub1d 11872 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) < 𝑟 ↔ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) < (𝑟𝐿)))
9792, 96mpbird 257 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) < 𝑟)
9884, 97eqbrtrrd 5167 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))) < 𝑟)
9977, 83absrpcld 15487 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹𝑘)) ∈ ℝ+)
10072, 73, 99ltdivmuld 13128 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))) < 𝑟 ↔ (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹𝑘)) · 𝑟)))
10198, 100mpbid 232 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹𝑘)) · 𝑟))
10299rpcnd 13079 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹𝑘)) ∈ ℂ)
10373recnd 11289 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → 𝑟 ∈ ℂ)
104102, 103mulcomd 11282 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((abs‘(𝐹𝑘)) · 𝑟) = (𝑟 · (abs‘(𝐹𝑘))))
105101, 104breqtrd 5169 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < (𝑟 · (abs‘(𝐹𝑘))))
10672, 79, 105ltled 11409 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘))))
107106ex 412 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))))
108107ralimdva 3167 . . . . . . . . . 10 (((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) → (∀𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿) → ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))))
109108reximdva 3168 . . . . . . . . 9 ((𝜑𝑟 ∈ (𝐿(,)1)) → (∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))))
11066, 109mpd 15 . . . . . . . 8 ((𝜑𝑟 ∈ (𝐿(,)1)) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘))))
11158, 110r19.29a 3162 . . . . . . 7 ((𝜑𝑟 ∈ (𝐿(,)1)) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
112111ralrimiva 3146 . . . . . 6 (𝜑 → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
113112adantr 480 . . . . 5 ((𝜑𝐿 < 1) → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
114 ioon0 13413 . . . . . . . 8 ((𝐿 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
11540, 41, 114sylancl 586 . . . . . . 7 (𝜑 → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
116115biimpar 477 . . . . . 6 ((𝜑𝐿 < 1) → (𝐿(,)1) ≠ ∅)
117 r19.3rzv 4499 . . . . . 6 ((𝐿(,)1) ≠ ∅ → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
118116, 117syl 17 . . . . 5 ((𝜑𝐿 < 1) → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
119113, 118mpbird 257 . . . 4 ((𝜑𝐿 < 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
1206, 5, 29iserex 15693 . . . . 5 (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
121120adantr 480 . . . 4 ((𝜑𝐿 < 1) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
122119, 121mpbird 257 . . 3 ((𝜑𝐿 < 1) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
123122ex 412 . 2 (𝜑 → (𝐿 < 1 → seq𝑀( + , 𝐹) ∈ dom ⇝ ))
124 cvgdvgrat.n1 . . . . . 6 (𝜑𝐿 ≠ 1)
125 1red 11262 . . . . . . 7 (𝜑 → 1 ∈ ℝ)
12639, 125lttri2d 11400 . . . . . 6 (𝜑 → (𝐿 ≠ 1 ↔ (𝐿 < 1 ∨ 1 < 𝐿)))
127124, 126mpbid 232 . . . . 5 (𝜑 → (𝐿 < 1 ∨ 1 < 𝐿))
128127orcanai 1005 . . . 4 ((𝜑 ∧ ¬ 𝐿 < 1) → 1 < 𝐿)
129 simplr 769 . . . . . . . 8 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝑛𝑊)
130 cvgdvgrat.f . . . . . . . . 9 (𝜑𝐹𝑉)
131130ad3antrrr 730 . . . . . . . 8 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝐹𝑉)
13248ad3antrrr 730 . . . . . . . . 9 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → (𝑖𝑊 → (𝐹𝑖) ∈ ℂ))
133132imp 406 . . . . . . . 8 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖𝑊) → (𝐹𝑖) ∈ ℂ)
1341uztrn2 12897 . . . . . . . . . . . 12 ((𝑛𝑊𝑖 ∈ (ℤ𝑛)) → 𝑖𝑊)
13522neeq1d 3000 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → ((𝐹𝑘) ≠ 0 ↔ (𝐹𝑖) ≠ 0))
13621, 135imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (((𝜑𝑘𝑊) → (𝐹𝑘) ≠ 0) ↔ ((𝜑𝑖𝑊) → (𝐹𝑖) ≠ 0)))
137136, 34chvarvv 1998 . . . . . . . . . . . 12 ((𝜑𝑖𝑊) → (𝐹𝑖) ≠ 0)
138134, 137sylan2 593 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛𝑊𝑖 ∈ (ℤ𝑛))) → (𝐹𝑖) ≠ 0)
139138anassrs 467 . . . . . . . . . 10 (((𝜑𝑛𝑊) ∧ 𝑖 ∈ (ℤ𝑛)) → (𝐹𝑖) ≠ 0)
140139adantllr 719 . . . . . . . . 9 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑖 ∈ (ℤ𝑛)) → (𝐹𝑖) ≠ 0)
141140adantlr 715 . . . . . . . 8 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ𝑛)) → (𝐹𝑖) ≠ 0)
14253, 52breq12d 5156 . . . . . . . . . 10 (𝑘 = 𝑖 → ((abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ↔ (abs‘(𝐹𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1)))))
143142rspccva 3621 . . . . . . . . 9 ((∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ∧ 𝑖 ∈ (ℤ𝑛)) → (abs‘(𝐹𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
144143adantll 714 . . . . . . . 8 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ𝑛)) → (abs‘(𝐹𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
1451, 2, 129, 131, 133, 141, 144dvgrat 44331 . . . . . . 7 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
1469adantr 480 . . . . . . . . 9 ((𝜑 ∧ 1 < 𝐿) → 𝑁 ∈ ℤ)
147 1re 11261 . . . . . . . . . . 11 1 ∈ ℝ
148 difrp 13073 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ+))
149147, 39, 148sylancr 587 . . . . . . . . . 10 (𝜑 → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ+))
150149biimpa 476 . . . . . . . . 9 ((𝜑 ∧ 1 < 𝐿) → (𝐿 − 1) ∈ ℝ+)
15137adantlr 715 . . . . . . . . 9 (((𝜑 ∧ 1 < 𝐿) ∧ 𝑘𝑊) → (𝑅𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
15210adantr 480 . . . . . . . . 9 ((𝜑 ∧ 1 < 𝐿) → 𝑅𝐿)
1531, 146, 150, 151, 152climi2 15547 . . . . . . . 8 ((𝜑 ∧ 1 < 𝐿) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1))
15475adantllr 719 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ∈ ℂ)
155154adantr 480 . . . . . . . . . . . . 13 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹𝑘) ∈ ℂ)
156155abscld 15475 . . . . . . . . . . . 12 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) ∈ ℝ)
15769adantllr 719 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
158157adantr 480 . . . . . . . . . . . . 13 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
159158abscld 15475 . . . . . . . . . . . 12 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
16081adantllr 719 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ≠ 0)
161160adantr 480 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹𝑘) ≠ 0)
162155, 161absrpcld 15487 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) ∈ ℝ+)
163162rpcnd 13079 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) ∈ ℂ)
164163mullidd 11279 . . . . . . . . . . . . 13 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹𝑘))) = (abs‘(𝐹𝑘)))
16539ad4antr 732 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℝ)
166165recnd 11289 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℂ)
167 1cnd 11256 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℂ)
168166, 167negsubdi2d 11636 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) = (1 − 𝐿))
169157, 154, 160divcld 12043 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
170169abscld 15475 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
17139ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝐿 ∈ ℝ)
172170, 171resubcld 11691 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) ∈ ℝ)
173 1red 11262 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → 1 ∈ ℝ)
174171, 173resubcld 11691 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐿 − 1) ∈ ℝ)
175172, 174absltd 15468 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1) ↔ (-(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) < (𝐿 − 1))))
176175simprbda 498 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿))
177168, 176eqbrtrrd 5167 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿))
178 1red 11262 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℝ)
179158, 155, 161divcld 12043 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
180179abscld 15475 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
181178, 180, 165ltsub1d 11872 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ↔ (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)))
182177, 181mpbird 257 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
183158, 155, 161absdivd 15494 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))))
184182, 183breqtrd 5169 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))))
185178, 159, 162ltmuldivd 13124 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → ((1 · (abs‘(𝐹𝑘))) < (abs‘(𝐹‘(𝑘 + 1))) ↔ 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘)))))
186184, 185mpbird 257 . . . . . . . . . . . . 13 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹𝑘))) < (abs‘(𝐹‘(𝑘 + 1))))
187164, 186eqbrtrrd 5167 . . . . . . . . . . . 12 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) < (abs‘(𝐹‘(𝑘 + 1))))
188156, 159, 187ltled 11409 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
189188ex 412 . . . . . . . . . 10 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1) → (abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
190189ralimdva 3167 . . . . . . . . 9 (((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) → (∀𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1) → ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
191190reximdva 3168 . . . . . . . 8 ((𝜑 ∧ 1 < 𝐿) → (∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
192153, 191mpd 15 . . . . . . 7 ((𝜑 ∧ 1 < 𝐿) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
193145, 192r19.29a 3162 . . . . . 6 ((𝜑 ∧ 1 < 𝐿) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
194 df-nel 3047 . . . . . 6 (seq𝑁( + , 𝐹) ∉ dom ⇝ ↔ ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
195193, 194sylib 218 . . . . 5 ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
196120adantr 480 . . . . 5 ((𝜑 ∧ 1 < 𝐿) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
197195, 196mtbird 325 . . . 4 ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
198128, 197syldan 591 . . 3 ((𝜑 ∧ ¬ 𝐿 < 1) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
199198ex 412 . 2 (𝜑 → (¬ 𝐿 < 1 → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
200123, 199impcon4bid 227 1 (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wnel 3046  wral 3061  wrex 3070  c0 4333   class class class wbr 5143  cmpt 5225  dom cdm 5685  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  *cxr 11294   < clt 11295  cle 11296  cmin 11492  -cneg 11493   / cdiv 11920  cz 12613  cuz 12878  +crp 13034  (,)cioo 13387  seqcseq 14042  abscabs 15273  cli 15520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-ioo 13391  df-ico 13393  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723
This theorem is referenced by:  radcnvrat  44333
  Copyright terms: Public domain W3C validator