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 37334
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 14397 and dvgrat 37333 directly uses the limit of the ratio.

(It also demonstrates how to use climi2 14033 and absltd 13959 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191, and how to use r19.29a 3056 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3009 at https://groups.google.com/forum/#!topic/metamath/2RPikOiXLMo.) (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 2606 . . . . . . . . 9 (ℤ𝑛) = (ℤ𝑛)
3 elioore 12029 . . . . . . . . . 10 (𝑟 ∈ (𝐿(,)1) → 𝑟 ∈ ℝ)
43ad3antlr 762 . . . . . . . . 9 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → 𝑟 ∈ ℝ)
5 cvgdvgrat.n . . . . . . . . . . . . . . . . 17 (𝜑𝑁𝑍)
6 cvgdvgrat.z . . . . . . . . . . . . . . . . 17 𝑍 = (ℤ𝑀)
75, 6syl6eleq 2694 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝑀))
8 eluzelz 11526 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
97, 8syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℤ)
10 cvgdvgrat.cvg . . . . . . . . . . . . . . 15 (𝜑𝑅𝐿)
11 cvgdvgrat.r . . . . . . . . . . . . . . . . . 18 𝑅 = (𝑘𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
1211a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑𝑅 = (𝑘𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘)))))
131peano2uzs 11571 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝑊 → (𝑘 + 1) ∈ 𝑊)
14 ovex 6552 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 + 1) ∈ V
15 eleq1 2672 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝑖𝑊 ↔ (𝑘 + 1) ∈ 𝑊))
1615anbi2d 735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑘 + 1) → ((𝜑𝑖𝑊) ↔ (𝜑 ∧ (𝑘 + 1) ∈ 𝑊)))
17 fveq2 6085 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝐹𝑖) = (𝐹‘(𝑘 + 1)))
1817eleq1d 2668 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑘 + 1) → ((𝐹𝑖) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
1916, 18imbi12d 332 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = (𝑘 + 1) → (((𝜑𝑖𝑊) → (𝐹𝑖) ∈ ℂ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)))
20 eleq1 2672 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → (𝑘𝑊𝑖𝑊))
2120anbi2d 735 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → ((𝜑𝑘𝑊) ↔ (𝜑𝑖𝑊)))
22 fveq2 6085 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
2322eleq1d 2668 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑖) ∈ ℂ))
2421, 23imbi12d 332 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑖 → (((𝜑𝑘𝑊) → (𝐹𝑘) ∈ ℂ) ↔ ((𝜑𝑖𝑊) → (𝐹𝑖) ∈ ℂ)))
251eleq2i 2676 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑊𝑘 ∈ (ℤ𝑁))
266uztrn2 11534 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁𝑍𝑘 ∈ (ℤ𝑁)) → 𝑘𝑍)
275, 26sylan 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (ℤ𝑁)) → 𝑘𝑍)
2825, 27sylan2b 490 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘𝑊) → 𝑘𝑍)
29 cvgdvgrat.c . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
3028, 29syldan 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘𝑊) → (𝐹𝑘) ∈ ℂ)
3124, 30chvarv 2246 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝑊) → (𝐹𝑖) ∈ ℂ)
3214, 19, 31vtocl 3228 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
3313, 32sylan2 489 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
34 cvgdvgrat.n0 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑊) → (𝐹𝑘) ≠ 0)
3533, 30, 34divcld 10647 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑊) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
3635abscld 13966 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑊) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
3712, 36fvmpt2d 6184 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑊) → (𝑅𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
3837, 36eqeltrd 2684 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑊) → (𝑅𝑘) ∈ ℝ)
391, 9, 10, 38climrecl 14105 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ ℝ)
4039rexrd 9942 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ℝ*)
41 1re 9892 . . . . . . . . . . . . . 14 1 ∈ ℝ
4241rexri 9945 . . . . . . . . . . . . 13 1 ∈ ℝ*
43 elioo2 12040 . . . . . . . . . . . . 13 ((𝐿 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟𝑟 < 1)))
4440, 42, 43sylancl 692 . . . . . . . . . . . 12 (𝜑 → (𝑟 ∈ (𝐿(,)1) ↔ (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟𝑟 < 1)))
4544biimpa 499 . . . . . . . . . . 11 ((𝜑𝑟 ∈ (𝐿(,)1)) → (𝑟 ∈ ℝ ∧ 𝐿 < 𝑟𝑟 < 1))
4645simp3d 1067 . . . . . . . . . 10 ((𝜑𝑟 ∈ (𝐿(,)1)) → 𝑟 < 1)
4746ad2antrr 757 . . . . . . . . 9 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → 𝑟 < 1)
48 simplr 787 . . . . . . . . 9 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → 𝑛𝑊)
4931ex 448 . . . . . . . . . . 11 (𝜑 → (𝑖𝑊 → (𝐹𝑖) ∈ ℂ))
5049ad3antrrr 761 . . . . . . . . . 10 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → (𝑖𝑊 → (𝐹𝑖) ∈ ℂ))
5150imp 443 . . . . . . . . 9 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) ∧ 𝑖𝑊) → (𝐹𝑖) ∈ ℂ)
52 oveq1 6531 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
5352fveq2d 6089 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑖 + 1)))
5453fveq2d 6089 . . . . . . . . . . . 12 (𝑘 = 𝑖 → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘(𝐹‘(𝑖 + 1))))
5522fveq2d 6089 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (abs‘(𝐹𝑘)) = (abs‘(𝐹𝑖)))
5655oveq2d 6540 . . . . . . . . . . . 12 (𝑘 = 𝑖 → (𝑟 · (abs‘(𝐹𝑘))) = (𝑟 · (abs‘(𝐹𝑖))))
5754, 56breq12d 4587 . . . . . . . . . . 11 (𝑘 = 𝑖 → ((abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘))) ↔ (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑖)))))
5857rspccva 3277 . . . . . . . . . 10 ((∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘))) ∧ 𝑖 ∈ (ℤ𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑖))))
5958adantll 745 . . . . . . . . 9 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) ∧ 𝑖 ∈ (ℤ𝑛)) → (abs‘(𝐹‘(𝑖 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑖))))
601, 2, 4, 47, 48, 51, 59cvgrat 14397 . . . . . . . 8 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
619adantr 479 . . . . . . . . . 10 ((𝜑𝑟 ∈ (𝐿(,)1)) → 𝑁 ∈ ℤ)
6245simp2d 1066 . . . . . . . . . . 11 ((𝜑𝑟 ∈ (𝐿(,)1)) → 𝐿 < 𝑟)
63 difrp 11697 . . . . . . . . . . . 12 ((𝐿 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝐿 < 𝑟 ↔ (𝑟𝐿) ∈ ℝ+))
6439, 3, 63syl2an 492 . . . . . . . . . . 11 ((𝜑𝑟 ∈ (𝐿(,)1)) → (𝐿 < 𝑟 ↔ (𝑟𝐿) ∈ ℝ+))
6562, 64mpbid 220 . . . . . . . . . 10 ((𝜑𝑟 ∈ (𝐿(,)1)) → (𝑟𝐿) ∈ ℝ+)
6637adantlr 746 . . . . . . . . . 10 (((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑘𝑊) → (𝑅𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
6710adantr 479 . . . . . . . . . 10 ((𝜑𝑟 ∈ (𝐿(,)1)) → 𝑅𝐿)
681, 61, 65, 66, 67climi2 14033 . . . . . . . . 9 ((𝜑𝑟 ∈ (𝐿(,)1)) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿))
691uztrn2 11534 . . . . . . . . . . . . . . . . . 18 ((𝑛𝑊𝑘 ∈ (ℤ𝑛)) → 𝑘𝑊)
7069, 33sylan2 489 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛𝑊𝑘 ∈ (ℤ𝑛))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
7170anassrs 677 . . . . . . . . . . . . . . . 16 (((𝜑𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
7271adantllr 750 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
7372adantr 479 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
7473abscld 13966 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
753ad4antlr 764 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → 𝑟 ∈ ℝ)
7669, 30sylan2 489 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛𝑊𝑘 ∈ (ℤ𝑛))) → (𝐹𝑘) ∈ ℂ)
7776anassrs 677 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ∈ ℂ)
7877adantllr 750 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ∈ ℂ)
7978adantr 479 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (𝐹𝑘) ∈ ℂ)
8079abscld 13966 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹𝑘)) ∈ ℝ)
8175, 80remulcld 9923 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (𝑟 · (abs‘(𝐹𝑘))) ∈ ℝ)
8269, 34sylan2 489 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛𝑊𝑘 ∈ (ℤ𝑛))) → (𝐹𝑘) ≠ 0)
8382anassrs 677 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ≠ 0)
8483adantllr 750 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ≠ 0)
8584adantr 479 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (𝐹𝑘) ≠ 0)
8673, 79, 85absdivd 13985 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))))
8772, 78, 84divcld 10647 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
8887abscld 13966 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
8939ad3antrrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝐿 ∈ ℝ)
9088, 89resubcld 10306 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) ∈ ℝ)
913ad3antlr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑟 ∈ ℝ)
9291, 89resubcld 10306 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑟𝐿) ∈ ℝ)
9390, 92absltd 13959 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿) ↔ (-(𝑟𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) < (𝑟𝐿))))
9493simplbda 651 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) < (𝑟𝐿))
9573, 79, 85divcld 10647 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
9695abscld 13966 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
9739ad4antr 763 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → 𝐿 ∈ ℝ)
9896, 75, 97ltsub1d 10482 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) < 𝑟 ↔ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) < (𝑟𝐿)))
9994, 98mpbird 245 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) < 𝑟)
10086, 99eqbrtrrd 4598 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))) < 𝑟)
10179, 85absrpcld 13978 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹𝑘)) ∈ ℝ+)
10274, 75, 101ltdivmuld 11752 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))) < 𝑟 ↔ (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹𝑘)) · 𝑟)))
103100, 102mpbid 220 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < ((abs‘(𝐹𝑘)) · 𝑟))
104101rpcnd 11703 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹𝑘)) ∈ ℂ)
10575recnd 9921 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → 𝑟 ∈ ℂ)
106104, 105mulcomd 9914 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → ((abs‘(𝐹𝑘)) · 𝑟) = (𝑟 · (abs‘(𝐹𝑘))))
107103, 106breqtrd 4600 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) < (𝑟 · (abs‘(𝐹𝑘))))
10874, 81, 107ltled 10033 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘))))
109108ex 448 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))))
110109ralimdva 2941 . . . . . . . . . 10 (((𝜑𝑟 ∈ (𝐿(,)1)) ∧ 𝑛𝑊) → (∀𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿) → ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))))
111110reximdva 2996 . . . . . . . . 9 ((𝜑𝑟 ∈ (𝐿(,)1)) → (∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝑟𝐿) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘)))))
11268, 111mpd 15 . . . . . . . 8 ((𝜑𝑟 ∈ (𝐿(,)1)) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘(𝐹‘(𝑘 + 1))) ≤ (𝑟 · (abs‘(𝐹𝑘))))
11360, 112r19.29a 3056 . . . . . . 7 ((𝜑𝑟 ∈ (𝐿(,)1)) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
114113ralrimiva 2945 . . . . . 6 (𝜑 → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
115114adantr 479 . . . . 5 ((𝜑𝐿 < 1) → ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ )
116 ioon0 12025 . . . . . . . 8 ((𝐿 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
11740, 42, 116sylancl 692 . . . . . . 7 (𝜑 → ((𝐿(,)1) ≠ ∅ ↔ 𝐿 < 1))
118117biimpar 500 . . . . . 6 ((𝜑𝐿 < 1) → (𝐿(,)1) ≠ ∅)
119 r19.3rzv 4012 . . . . . 6 ((𝐿(,)1) ≠ ∅ → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
120118, 119syl 17 . . . . 5 ((𝜑𝐿 < 1) → (seq𝑁( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑟 ∈ (𝐿(,)1)seq𝑁( + , 𝐹) ∈ dom ⇝ ))
121115, 120mpbird 245 . . . 4 ((𝜑𝐿 < 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ )
1226, 5, 29iserex 14178 . . . . 5 (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
123122adantr 479 . . . 4 ((𝜑𝐿 < 1) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
124121, 123mpbird 245 . . 3 ((𝜑𝐿 < 1) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
125124ex 448 . 2 (𝜑 → (𝐿 < 1 → seq𝑀( + , 𝐹) ∈ dom ⇝ ))
126 cvgdvgrat.n1 . . . . . 6 (𝜑𝐿 ≠ 1)
127 1red 9908 . . . . . . 7 (𝜑 → 1 ∈ ℝ)
12839, 127lttri2d 10024 . . . . . 6 (𝜑 → (𝐿 ≠ 1 ↔ (𝐿 < 1 ∨ 1 < 𝐿)))
129126, 128mpbid 220 . . . . 5 (𝜑 → (𝐿 < 1 ∨ 1 < 𝐿))
130129orcanai 949 . . . 4 ((𝜑 ∧ ¬ 𝐿 < 1) → 1 < 𝐿)
131 simplr 787 . . . . . . . 8 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝑛𝑊)
132 cvgdvgrat.f . . . . . . . . 9 (𝜑𝐹𝑉)
133132ad3antrrr 761 . . . . . . . 8 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → 𝐹𝑉)
13449ad3antrrr 761 . . . . . . . . 9 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → (𝑖𝑊 → (𝐹𝑖) ∈ ℂ))
135134imp 443 . . . . . . . 8 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖𝑊) → (𝐹𝑖) ∈ ℂ)
1361uztrn2 11534 . . . . . . . . . . . 12 ((𝑛𝑊𝑖 ∈ (ℤ𝑛)) → 𝑖𝑊)
13722neeq1d 2837 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → ((𝐹𝑘) ≠ 0 ↔ (𝐹𝑖) ≠ 0))
13821, 137imbi12d 332 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (((𝜑𝑘𝑊) → (𝐹𝑘) ≠ 0) ↔ ((𝜑𝑖𝑊) → (𝐹𝑖) ≠ 0)))
139138, 34chvarv 2246 . . . . . . . . . . . 12 ((𝜑𝑖𝑊) → (𝐹𝑖) ≠ 0)
140136, 139sylan2 489 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛𝑊𝑖 ∈ (ℤ𝑛))) → (𝐹𝑖) ≠ 0)
141140anassrs 677 . . . . . . . . . 10 (((𝜑𝑛𝑊) ∧ 𝑖 ∈ (ℤ𝑛)) → (𝐹𝑖) ≠ 0)
142141adantllr 750 . . . . . . . . 9 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑖 ∈ (ℤ𝑛)) → (𝐹𝑖) ≠ 0)
143142adantlr 746 . . . . . . . 8 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ𝑛)) → (𝐹𝑖) ≠ 0)
14455, 54breq12d 4587 . . . . . . . . . 10 (𝑘 = 𝑖 → ((abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ↔ (abs‘(𝐹𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1)))))
145144rspccva 3277 . . . . . . . . 9 ((∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))) ∧ 𝑖 ∈ (ℤ𝑛)) → (abs‘(𝐹𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
146145adantll 745 . . . . . . . 8 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ∧ 𝑖 ∈ (ℤ𝑛)) → (abs‘(𝐹𝑖)) ≤ (abs‘(𝐹‘(𝑖 + 1))))
1471, 2, 131, 133, 135, 143, 146dvgrat 37333 . . . . . . 7 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
1489adantr 479 . . . . . . . . 9 ((𝜑 ∧ 1 < 𝐿) → 𝑁 ∈ ℤ)
149 difrp 11697 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ+))
15041, 39, 149sylancr 693 . . . . . . . . . 10 (𝜑 → (1 < 𝐿 ↔ (𝐿 − 1) ∈ ℝ+))
151150biimpa 499 . . . . . . . . 9 ((𝜑 ∧ 1 < 𝐿) → (𝐿 − 1) ∈ ℝ+)
15237adantlr 746 . . . . . . . . 9 (((𝜑 ∧ 1 < 𝐿) ∧ 𝑘𝑊) → (𝑅𝑘) = (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
15310adantr 479 . . . . . . . . 9 ((𝜑 ∧ 1 < 𝐿) → 𝑅𝐿)
1541, 148, 151, 152, 153climi2 14033 . . . . . . . 8 ((𝜑 ∧ 1 < 𝐿) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1))
15577adantllr 750 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ∈ ℂ)
156155adantr 479 . . . . . . . . . . . . 13 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹𝑘) ∈ ℂ)
157156abscld 13966 . . . . . . . . . . . 12 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) ∈ ℝ)
15871adantllr 750 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
159158adantr 479 . . . . . . . . . . . . 13 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
160159abscld 13966 . . . . . . . . . . . 12 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
16183adantllr 750 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹𝑘) ≠ 0)
162161adantr 479 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (𝐹𝑘) ≠ 0)
163156, 162absrpcld 13978 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) ∈ ℝ+)
164163rpcnd 11703 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) ∈ ℂ)
165164mulid2d 9911 . . . . . . . . . . . . 13 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹𝑘))) = (abs‘(𝐹𝑘)))
16639ad4antr 763 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℝ)
167166recnd 9921 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 𝐿 ∈ ℂ)
168 1cnd 9909 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℂ)
169167, 168negsubdi2d 10256 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) = (1 − 𝐿))
170158, 155, 161divcld 10647 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
171170abscld 13966 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
17239ad3antrrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝐿 ∈ ℝ)
173171, 172resubcld 10306 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) ∈ ℝ)
174 1red 9908 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → 1 ∈ ℝ)
175172, 174resubcld 10306 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐿 − 1) ∈ ℝ)
176173, 175absltd 13959 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1) ↔ (-(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) ∧ ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿) < (𝐿 − 1))))
177176simprbda 650 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → -(𝐿 − 1) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿))
178169, 177eqbrtrrd 4598 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿))
179 1red 9908 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 ∈ ℝ)
180159, 156, 162divcld 10647 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → ((𝐹‘(𝑘 + 1)) / (𝐹𝑘)) ∈ ℂ)
181180abscld 13966 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ∈ ℝ)
182179, 181, 166ltsub1d 10482 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) ↔ (1 − 𝐿) < ((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)))
183178, 182mpbird 245 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))))
184159, 156, 162absdivd 13985 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) = ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))))
185183, 184breqtrd 4600 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘))))
186179, 160, 163ltmuldivd 11748 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → ((1 · (abs‘(𝐹𝑘))) < (abs‘(𝐹‘(𝑘 + 1))) ↔ 1 < ((abs‘(𝐹‘(𝑘 + 1))) / (abs‘(𝐹𝑘)))))
187185, 186mpbird 245 . . . . . . . . . . . . 13 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (1 · (abs‘(𝐹𝑘))) < (abs‘(𝐹‘(𝑘 + 1))))
188165, 187eqbrtrrd 4598 . . . . . . . . . . . 12 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) < (abs‘(𝐹‘(𝑘 + 1))))
189157, 160, 188ltled 10033 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) ∧ (abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1)) → (abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
190189ex 448 . . . . . . . . . 10 ((((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) ∧ 𝑘 ∈ (ℤ𝑛)) → ((abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1) → (abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
191190ralimdva 2941 . . . . . . . . 9 (((𝜑 ∧ 1 < 𝐿) ∧ 𝑛𝑊) → (∀𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1) → ∀𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
192191reximdva 2996 . . . . . . . 8 ((𝜑 ∧ 1 < 𝐿) → (∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘((abs‘((𝐹‘(𝑘 + 1)) / (𝐹𝑘))) − 𝐿)) < (𝐿 − 1) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
193154, 192mpd 15 . . . . . . 7 ((𝜑 ∧ 1 < 𝐿) → ∃𝑛𝑊𝑘 ∈ (ℤ𝑛)(abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
194147, 193r19.29a 3056 . . . . . 6 ((𝜑 ∧ 1 < 𝐿) → seq𝑁( + , 𝐹) ∉ dom ⇝ )
195 df-nel 2779 . . . . . 6 (seq𝑁( + , 𝐹) ∉ dom ⇝ ↔ ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
196194, 195sylib 206 . . . . 5 ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑁( + , 𝐹) ∈ dom ⇝ )
197122adantr 479 . . . . 5 ((𝜑 ∧ 1 < 𝐿) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
198196, 197mtbird 313 . . . 4 ((𝜑 ∧ 1 < 𝐿) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
199130, 198syldan 485 . . 3 ((𝜑 ∧ ¬ 𝐿 < 1) → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
200199ex 448 . 2 (𝜑 → (¬ 𝐿 < 1 → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
201125, 200impcon4bid 215 1 (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2776  wnel 2777  wral 2892  wrex 2893  c0 3870   class class class wbr 4574  cmpt 4634  dom cdm 5025  cfv 5787  (class class class)co 6524  cc 9787  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   · cmul 9794  *cxr 9926   < clt 9927  cle 9928  cmin 10114  -cneg 10115   / cdiv 10530  cz 11207  cuz 11516  +crp 11661  (,)cioo 11999  seqcseq 12615  abscabs 13765  cli 14006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868  ax-mulf 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-oadd 7425  df-er 7603  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-n0 11137  df-z 11208  df-uz 11517  df-q 11618  df-rp 11662  df-ioo 12003  df-ico 12005  df-fz 12150  df-fzo 12287  df-fl 12407  df-seq 12616  df-exp 12675  df-hash 12932  df-shft 13598  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-limsup 13993  df-clim 14010  df-rlim 14011  df-sum 14208
This theorem is referenced by:  radcnvrat  37335
  Copyright terms: Public domain W3C validator