Metamath Proof Explorer


Theorem cvgdvgrat

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

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

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

Proof

Step Hyp Ref Expression
1 cvgdvgrat.z 𝑍 = ( ℤ𝑀 )
2 cvgdvgrat.w 𝑊 = ( ℤ𝑁 )
3 cvgdvgrat.n ( 𝜑𝑁𝑍 )
4 cvgdvgrat.f ( 𝜑𝐹𝑉 )
5 cvgdvgrat.c ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
6 cvgdvgrat.n0 ( ( 𝜑𝑘𝑊 ) → ( 𝐹𝑘 ) ≠ 0 )
7 cvgdvgrat.r 𝑅 = ( 𝑘𝑊 ↦ ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) )
8 cvgdvgrat.cvg ( 𝜑𝑅𝐿 )
9 cvgdvgrat.n1 ( 𝜑𝐿 ≠ 1 )
10 eqid ( ℤ𝑛 ) = ( ℤ𝑛 )
11 elioore ( 𝑟 ∈ ( 𝐿 (,) 1 ) → 𝑟 ∈ ℝ )
12 11 ad3antlr ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) → 𝑟 ∈ ℝ )
13 3 1 eleqtrdi ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
14 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
15 13 14 syl ( 𝜑𝑁 ∈ ℤ )
16 7 a1i ( 𝜑𝑅 = ( 𝑘𝑊 ↦ ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) ) )
17 2 peano2uzs ( 𝑘𝑊 → ( 𝑘 + 1 ) ∈ 𝑊 )
18 ovex ( 𝑘 + 1 ) ∈ V
19 eleq1 ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑖𝑊 ↔ ( 𝑘 + 1 ) ∈ 𝑊 ) )
20 19 anbi2d ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝜑𝑖𝑊 ) ↔ ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ 𝑊 ) ) )
21 fveq2 ( 𝑖 = ( 𝑘 + 1 ) → ( 𝐹𝑖 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
22 21 eleq1d ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝐹𝑖 ) ∈ ℂ ↔ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ ) )
23 20 22 imbi12d ( 𝑖 = ( 𝑘 + 1 ) → ( ( ( 𝜑𝑖𝑊 ) → ( 𝐹𝑖 ) ∈ ℂ ) ↔ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ ) ) )
24 eleq1 ( 𝑘 = 𝑖 → ( 𝑘𝑊𝑖𝑊 ) )
25 24 anbi2d ( 𝑘 = 𝑖 → ( ( 𝜑𝑘𝑊 ) ↔ ( 𝜑𝑖𝑊 ) ) )
26 fveq2 ( 𝑘 = 𝑖 → ( 𝐹𝑘 ) = ( 𝐹𝑖 ) )
27 26 eleq1d ( 𝑘 = 𝑖 → ( ( 𝐹𝑘 ) ∈ ℂ ↔ ( 𝐹𝑖 ) ∈ ℂ ) )
28 25 27 imbi12d ( 𝑘 = 𝑖 → ( ( ( 𝜑𝑘𝑊 ) → ( 𝐹𝑘 ) ∈ ℂ ) ↔ ( ( 𝜑𝑖𝑊 ) → ( 𝐹𝑖 ) ∈ ℂ ) ) )
29 2 eleq2i ( 𝑘𝑊𝑘 ∈ ( ℤ𝑁 ) )
30 1 uztrn2 ( ( 𝑁𝑍𝑘 ∈ ( ℤ𝑁 ) ) → 𝑘𝑍 )
31 3 30 sylan ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → 𝑘𝑍 )
32 29 31 sylan2b ( ( 𝜑𝑘𝑊 ) → 𝑘𝑍 )
33 32 5 syldan ( ( 𝜑𝑘𝑊 ) → ( 𝐹𝑘 ) ∈ ℂ )
34 28 33 chvarvv ( ( 𝜑𝑖𝑊 ) → ( 𝐹𝑖 ) ∈ ℂ )
35 18 23 34 vtocl ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
36 17 35 sylan2 ( ( 𝜑𝑘𝑊 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
37 36 33 6 divcld ( ( 𝜑𝑘𝑊 ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ∈ ℂ )
38 37 abscld ( ( 𝜑𝑘𝑊 ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) ∈ ℝ )
39 16 38 fvmpt2d ( ( 𝜑𝑘𝑊 ) → ( 𝑅𝑘 ) = ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) )
40 39 38 eqeltrd ( ( 𝜑𝑘𝑊 ) → ( 𝑅𝑘 ) ∈ ℝ )
41 2 15 8 40 climrecl ( 𝜑𝐿 ∈ ℝ )
42 41 rexrd ( 𝜑𝐿 ∈ ℝ* )
43 1xr 1 ∈ ℝ*
44 elioo2 ( ( 𝐿 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝑟 ∈ ( 𝐿 (,) 1 ) ↔ ( 𝑟 ∈ ℝ ∧ 𝐿 < 𝑟𝑟 < 1 ) ) )
45 42 43 44 sylancl ( 𝜑 → ( 𝑟 ∈ ( 𝐿 (,) 1 ) ↔ ( 𝑟 ∈ ℝ ∧ 𝐿 < 𝑟𝑟 < 1 ) ) )
46 45 biimpa ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → ( 𝑟 ∈ ℝ ∧ 𝐿 < 𝑟𝑟 < 1 ) )
47 46 simp3d ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → 𝑟 < 1 )
48 47 ad2antrr ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) → 𝑟 < 1 )
49 simplr ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) → 𝑛𝑊 )
50 34 ex ( 𝜑 → ( 𝑖𝑊 → ( 𝐹𝑖 ) ∈ ℂ ) )
51 50 ad3antrrr ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) → ( 𝑖𝑊 → ( 𝐹𝑖 ) ∈ ℂ ) )
52 51 imp ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) ∧ 𝑖𝑊 ) → ( 𝐹𝑖 ) ∈ ℂ )
53 fvoveq1 ( 𝑘 = 𝑖 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑖 + 1 ) ) )
54 53 fveq2d ( 𝑘 = 𝑖 → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) )
55 26 fveq2d ( 𝑘 = 𝑖 → ( abs ‘ ( 𝐹𝑘 ) ) = ( abs ‘ ( 𝐹𝑖 ) ) )
56 55 oveq2d ( 𝑘 = 𝑖 → ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) = ( 𝑟 · ( abs ‘ ( 𝐹𝑖 ) ) ) )
57 54 56 breq12d ( 𝑘 = 𝑖 → ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ↔ ( abs ‘ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑖 ) ) ) ) )
58 57 rspccva ( ( ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ∧ 𝑖 ∈ ( ℤ𝑛 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑖 ) ) ) )
59 58 adantll ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) ∧ 𝑖 ∈ ( ℤ𝑛 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑖 ) ) ) )
60 2 10 12 48 49 52 59 cvgrat ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
61 15 adantr ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → 𝑁 ∈ ℤ )
62 46 simp2d ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → 𝐿 < 𝑟 )
63 difrp ( ( 𝐿 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝐿 < 𝑟 ↔ ( 𝑟𝐿 ) ∈ ℝ+ ) )
64 41 11 63 syl2an ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → ( 𝐿 < 𝑟 ↔ ( 𝑟𝐿 ) ∈ ℝ+ ) )
65 62 64 mpbid ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → ( 𝑟𝐿 ) ∈ ℝ+ )
66 39 adantlr ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑘𝑊 ) → ( 𝑅𝑘 ) = ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) )
67 8 adantr ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → 𝑅𝐿 )
68 2 61 65 66 67 climi2 ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → ∃ 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) )
69 2 uztrn2 ( ( 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ) → 𝑘𝑊 )
70 69 36 sylan2 ( ( 𝜑 ∧ ( 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
71 70 anassrs ( ( ( 𝜑𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
72 71 adantllr ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
73 72 adantr ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
74 73 abscld ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
75 11 ad4antlr ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → 𝑟 ∈ ℝ )
76 69 33 sylan2 ( ( 𝜑 ∧ ( 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ) ) → ( 𝐹𝑘 ) ∈ ℂ )
77 76 anassrs ( ( ( 𝜑𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
78 77 adantllr ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
79 78 adantr ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
80 79 abscld ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( 𝐹𝑘 ) ) ∈ ℝ )
81 75 80 remulcld ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ∈ ℝ )
82 69 6 sylan2 ( ( 𝜑 ∧ ( 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ) ) → ( 𝐹𝑘 ) ≠ 0 )
83 82 anassrs ( ( ( 𝜑𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑘 ) ≠ 0 )
84 83 adantllr ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑘 ) ≠ 0 )
85 84 adantr ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( 𝐹𝑘 ) ≠ 0 )
86 73 79 85 absdivd ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( abs ‘ ( 𝐹𝑘 ) ) ) )
87 72 78 84 divcld ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ∈ ℂ )
88 87 abscld ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) ∈ ℝ )
89 41 ad3antrrr ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → 𝐿 ∈ ℝ )
90 88 89 resubcld ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ∈ ℝ )
91 11 ad3antlr ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → 𝑟 ∈ ℝ )
92 91 89 resubcld ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝑟𝐿 ) ∈ ℝ )
93 90 92 absltd ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ↔ ( - ( 𝑟𝐿 ) < ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) < ( 𝑟𝐿 ) ) ) )
94 93 simplbda ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) < ( 𝑟𝐿 ) )
95 73 79 85 divcld ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ∈ ℂ )
96 95 abscld ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) ∈ ℝ )
97 41 ad4antr ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → 𝐿 ∈ ℝ )
98 96 75 97 ltsub1d ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) < 𝑟 ↔ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) < ( 𝑟𝐿 ) ) )
99 94 98 mpbird ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) < 𝑟 )
100 86 99 eqbrtrrd ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( abs ‘ ( 𝐹𝑘 ) ) ) < 𝑟 )
101 79 85 absrpcld ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( 𝐹𝑘 ) ) ∈ ℝ+ )
102 74 75 101 ltdivmuld ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( abs ‘ ( 𝐹𝑘 ) ) ) < 𝑟 ↔ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) < ( ( abs ‘ ( 𝐹𝑘 ) ) · 𝑟 ) ) )
103 100 102 mpbid ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) < ( ( abs ‘ ( 𝐹𝑘 ) ) · 𝑟 ) )
104 101 rpcnd ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( 𝐹𝑘 ) ) ∈ ℂ )
105 75 recnd ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → 𝑟 ∈ ℂ )
106 104 105 mulcomd ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( ( abs ‘ ( 𝐹𝑘 ) ) · 𝑟 ) = ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) )
107 103 106 breqtrd ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) < ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) )
108 74 81 107 ltled ( ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) )
109 108 ex ( ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) )
110 109 ralimdva ( ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) ∧ 𝑛𝑊 ) → ( ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) → ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) )
111 110 reximdva ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → ( ∃ 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝑟𝐿 ) → ∃ 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) ) )
112 68 111 mpd ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → ∃ 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝑟 · ( abs ‘ ( 𝐹𝑘 ) ) ) )
113 60 112 r19.29a ( ( 𝜑𝑟 ∈ ( 𝐿 (,) 1 ) ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
114 113 ralrimiva ( 𝜑 → ∀ 𝑟 ∈ ( 𝐿 (,) 1 ) seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
115 114 adantr ( ( 𝜑𝐿 < 1 ) → ∀ 𝑟 ∈ ( 𝐿 (,) 1 ) seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
116 ioon0 ( ( 𝐿 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 𝐿 (,) 1 ) ≠ ∅ ↔ 𝐿 < 1 ) )
117 42 43 116 sylancl ( 𝜑 → ( ( 𝐿 (,) 1 ) ≠ ∅ ↔ 𝐿 < 1 ) )
118 117 biimpar ( ( 𝜑𝐿 < 1 ) → ( 𝐿 (,) 1 ) ≠ ∅ )
119 r19.3rzv ( ( 𝐿 (,) 1 ) ≠ ∅ → ( seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ↔ ∀ 𝑟 ∈ ( 𝐿 (,) 1 ) seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
120 118 119 syl ( ( 𝜑𝐿 < 1 ) → ( seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ↔ ∀ 𝑟 ∈ ( 𝐿 (,) 1 ) seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
121 115 120 mpbird ( ( 𝜑𝐿 < 1 ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
122 1 3 5 iserex ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
123 122 adantr ( ( 𝜑𝐿 < 1 ) → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
124 121 123 mpbird ( ( 𝜑𝐿 < 1 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
125 124 ex ( 𝜑 → ( 𝐿 < 1 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) )
126 1red ( 𝜑 → 1 ∈ ℝ )
127 41 126 lttri2d ( 𝜑 → ( 𝐿 ≠ 1 ↔ ( 𝐿 < 1 ∨ 1 < 𝐿 ) ) )
128 9 127 mpbid ( 𝜑 → ( 𝐿 < 1 ∨ 1 < 𝐿 ) )
129 128 orcanai ( ( 𝜑 ∧ ¬ 𝐿 < 1 ) → 1 < 𝐿 )
130 simplr ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑛𝑊 )
131 4 ad3antrrr ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → 𝐹𝑉 )
132 50 ad3antrrr ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑖𝑊 → ( 𝐹𝑖 ) ∈ ℂ ) )
133 132 imp ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ∧ 𝑖𝑊 ) → ( 𝐹𝑖 ) ∈ ℂ )
134 2 uztrn2 ( ( 𝑛𝑊𝑖 ∈ ( ℤ𝑛 ) ) → 𝑖𝑊 )
135 26 neeq1d ( 𝑘 = 𝑖 → ( ( 𝐹𝑘 ) ≠ 0 ↔ ( 𝐹𝑖 ) ≠ 0 ) )
136 25 135 imbi12d ( 𝑘 = 𝑖 → ( ( ( 𝜑𝑘𝑊 ) → ( 𝐹𝑘 ) ≠ 0 ) ↔ ( ( 𝜑𝑖𝑊 ) → ( 𝐹𝑖 ) ≠ 0 ) ) )
137 136 6 chvarvv ( ( 𝜑𝑖𝑊 ) → ( 𝐹𝑖 ) ≠ 0 )
138 134 137 sylan2 ( ( 𝜑 ∧ ( 𝑛𝑊𝑖 ∈ ( ℤ𝑛 ) ) ) → ( 𝐹𝑖 ) ≠ 0 )
139 138 anassrs ( ( ( 𝜑𝑛𝑊 ) ∧ 𝑖 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑖 ) ≠ 0 )
140 139 adantllr ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑖 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑖 ) ≠ 0 )
141 140 adantlr ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ∧ 𝑖 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑖 ) ≠ 0 )
142 55 54 breq12d ( 𝑘 = 𝑖 → ( ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( abs ‘ ( 𝐹𝑖 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ) )
143 142 rspccva ( ( ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∧ 𝑖 ∈ ( ℤ𝑛 ) ) → ( abs ‘ ( 𝐹𝑖 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) )
144 143 adantll ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ∧ 𝑖 ∈ ( ℤ𝑛 ) ) → ( abs ‘ ( 𝐹𝑖 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) )
145 2 10 130 131 133 141 144 dvgrat ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) → seq 𝑁 ( + , 𝐹 ) ∉ dom ⇝ )
146 15 adantr ( ( 𝜑 ∧ 1 < 𝐿 ) → 𝑁 ∈ ℤ )
147 1re 1 ∈ ℝ
148 difrp ( ( 1 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 1 < 𝐿 ↔ ( 𝐿 − 1 ) ∈ ℝ+ ) )
149 147 41 148 sylancr ( 𝜑 → ( 1 < 𝐿 ↔ ( 𝐿 − 1 ) ∈ ℝ+ ) )
150 149 biimpa ( ( 𝜑 ∧ 1 < 𝐿 ) → ( 𝐿 − 1 ) ∈ ℝ+ )
151 39 adantlr ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑘𝑊 ) → ( 𝑅𝑘 ) = ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) )
152 8 adantr ( ( 𝜑 ∧ 1 < 𝐿 ) → 𝑅𝐿 )
153 2 146 150 151 152 climi2 ( ( 𝜑 ∧ 1 < 𝐿 ) → ∃ 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) )
154 77 adantllr ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
155 154 adantr ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
156 155 abscld ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( abs ‘ ( 𝐹𝑘 ) ) ∈ ℝ )
157 71 adantllr ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
158 157 adantr ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
159 158 abscld ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
160 83 adantllr ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑘 ) ≠ 0 )
161 160 adantr ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( 𝐹𝑘 ) ≠ 0 )
162 155 161 absrpcld ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( abs ‘ ( 𝐹𝑘 ) ) ∈ ℝ+ )
163 162 rpcnd ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( abs ‘ ( 𝐹𝑘 ) ) ∈ ℂ )
164 163 mulid2d ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( 1 · ( abs ‘ ( 𝐹𝑘 ) ) ) = ( abs ‘ ( 𝐹𝑘 ) ) )
165 41 ad4antr ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → 𝐿 ∈ ℝ )
166 165 recnd ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → 𝐿 ∈ ℂ )
167 1cnd ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → 1 ∈ ℂ )
168 166 167 negsubdi2d ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → - ( 𝐿 − 1 ) = ( 1 − 𝐿 ) )
169 157 154 160 divcld ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ∈ ℂ )
170 169 abscld ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) ∈ ℝ )
171 41 ad3antrrr ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → 𝐿 ∈ ℝ )
172 170 171 resubcld ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ∈ ℝ )
173 1red ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → 1 ∈ ℝ )
174 171 173 resubcld ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( 𝐿 − 1 ) ∈ ℝ )
175 172 174 absltd ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ↔ ( - ( 𝐿 − 1 ) < ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) < ( 𝐿 − 1 ) ) ) )
176 175 simprbda ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → - ( 𝐿 − 1 ) < ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) )
177 168 176 eqbrtrrd ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( 1 − 𝐿 ) < ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) )
178 1red ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → 1 ∈ ℝ )
179 158 155 161 divcld ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ∈ ℂ )
180 179 abscld ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) ∈ ℝ )
181 178 180 165 ltsub1d ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( 1 < ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) ↔ ( 1 − 𝐿 ) < ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) )
182 177 181 mpbird ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → 1 < ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) )
183 158 155 161 absdivd ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( abs ‘ ( 𝐹𝑘 ) ) ) )
184 182 183 breqtrd ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → 1 < ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( abs ‘ ( 𝐹𝑘 ) ) ) )
185 178 159 162 ltmuldivd ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( ( 1 · ( abs ‘ ( 𝐹𝑘 ) ) ) < ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ 1 < ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( abs ‘ ( 𝐹𝑘 ) ) ) ) )
186 184 185 mpbird ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( 1 · ( abs ‘ ( 𝐹𝑘 ) ) ) < ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
187 164 186 eqbrtrrd ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( abs ‘ ( 𝐹𝑘 ) ) < ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
188 156 159 187 ltled ( ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) ∧ ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) ) → ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
189 188 ex ( ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) → ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
190 189 ralimdva ( ( ( 𝜑 ∧ 1 < 𝐿 ) ∧ 𝑛𝑊 ) → ( ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) → ∀ 𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
191 190 reximdva ( ( 𝜑 ∧ 1 < 𝐿 ) → ( ∃ 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹𝑘 ) ) ) − 𝐿 ) ) < ( 𝐿 − 1 ) → ∃ 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
192 153 191 mpd ( ( 𝜑 ∧ 1 < 𝐿 ) → ∃ 𝑛𝑊𝑘 ∈ ( ℤ𝑛 ) ( abs ‘ ( 𝐹𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
193 145 192 r19.29a ( ( 𝜑 ∧ 1 < 𝐿 ) → seq 𝑁 ( + , 𝐹 ) ∉ dom ⇝ )
194 df-nel ( seq 𝑁 ( + , 𝐹 ) ∉ dom ⇝ ↔ ¬ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
195 193 194 sylib ( ( 𝜑 ∧ 1 < 𝐿 ) → ¬ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
196 122 adantr ( ( 𝜑 ∧ 1 < 𝐿 ) → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
197 195 196 mtbird ( ( 𝜑 ∧ 1 < 𝐿 ) → ¬ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
198 129 197 syldan ( ( 𝜑 ∧ ¬ 𝐿 < 1 ) → ¬ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
199 198 ex ( 𝜑 → ( ¬ 𝐿 < 1 → ¬ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) )
200 125 199 impcon4bid ( 𝜑 → ( 𝐿 < 1 ↔ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) )