Metamath Proof Explorer

Theorem radcnvrat

Description: Let L be the limit, if one exists, of the ratio ( abs( ( A( k + 1 ) ) / ( Ak ) ) ) (as in the ratio test cvgdvgrat ) as k increases. Then the radius of convergence of power series sum_ n e. NN0 ( ( An ) x. ( x ^ n ) ) is ( 1 / L ) if L is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020)

Ref Expression
Hypotheses radcnvrat.g 
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
radcnvrat.a 
|- ( ph -> A : NN0 --> CC )
radcnvrat.r 
|- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
radcnvrat.rat 
|- D = ( k e. NN0 |-> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) )
radcnvrat.z 
|- Z = ( ZZ>= ` M )
radcnvrat.m 
|- ( ph -> M e. NN0 )
radcnvrat.n0 
|- ( ( ph /\ k e. Z ) -> ( A ` k ) =/= 0 )
radcnvrat.l 
|- ( ph -> D ~~> L )
radcnvrat.ln0 
|- ( ph -> L =/= 0 )
Assertion radcnvrat 
|- ( ph -> R = ( 1 / L ) )

Proof

Step Hyp Ref Expression
1 radcnvrat.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 radcnvrat.a 
 |-  ( ph -> A : NN0 --> CC )
3 radcnvrat.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
4 radcnvrat.rat 
 |-  D = ( k e. NN0 |-> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) )
5 radcnvrat.z 
 |-  Z = ( ZZ>= ` M )
6 radcnvrat.m 
 |-  ( ph -> M e. NN0 )
7 radcnvrat.n0 
 |-  ( ( ph /\ k e. Z ) -> ( A ` k ) =/= 0 )
8 radcnvrat.l 
 |-  ( ph -> D ~~> L )
9 radcnvrat.ln0 
 |-  ( ph -> L =/= 0 )
10 xrltso 
 |-  < Or RR*
11 10 a1i 
 |-  ( ph -> < Or RR* )
12 6 nn0zd 
 |-  ( ph -> M e. ZZ )
13 5 reseq2i 
 |-  ( D |` Z ) = ( D |` ( ZZ>= ` M ) )
14 nn0ex 
 |-  NN0 e. _V
15 14 mptex 
 |-  ( k e. NN0 |-> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) ) e. _V
16 4 15 eqeltri 
 |-  D e. _V
17 climres 
 |-  ( ( M e. ZZ /\ D e. _V ) -> ( ( D |` ( ZZ>= ` M ) ) ~~> L <-> D ~~> L ) )
18 12 16 17 sylancl 
 |-  ( ph -> ( ( D |` ( ZZ>= ` M ) ) ~~> L <-> D ~~> L ) )
19 8 18 mpbird 
 |-  ( ph -> ( D |` ( ZZ>= ` M ) ) ~~> L )
20 13 19 eqbrtrid 
 |-  ( ph -> ( D |` Z ) ~~> L )
21 4 reseq1i 
 |-  ( D |` Z ) = ( ( k e. NN0 |-> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) ) |` Z )
22 eluznn0 
 |-  ( ( M e. NN0 /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
23 6 22 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
24 23 ex 
 |-  ( ph -> ( k e. ( ZZ>= ` M ) -> k e. NN0 ) )
25 24 ssrdv 
 |-  ( ph -> ( ZZ>= ` M ) C_ NN0 )
26 5 25 eqsstrid 
 |-  ( ph -> Z C_ NN0 )
27 26 resmptd 
 |-  ( ph -> ( ( k e. NN0 |-> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) ) |` Z ) = ( k e. Z |-> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) ) )
28 21 27 eqtrid 
 |-  ( ph -> ( D |` Z ) = ( k e. Z |-> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) ) )
29 fvexd 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) e. _V )
30 28 29 fvmpt2d 
 |-  ( ( ph /\ k e. Z ) -> ( ( D |` Z ) ` k ) = ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) )
31 5 peano2uzs 
 |-  ( k e. Z -> ( k + 1 ) e. Z )
32 26 sselda 
 |-  ( ( ph /\ ( k + 1 ) e. Z ) -> ( k + 1 ) e. NN0 )
33 2 ffvelcdmda 
 |-  ( ( ph /\ ( k + 1 ) e. NN0 ) -> ( A ` ( k + 1 ) ) e. CC )
34 32 33 syldan 
 |-  ( ( ph /\ ( k + 1 ) e. Z ) -> ( A ` ( k + 1 ) ) e. CC )
35 31 34 sylan2 
 |-  ( ( ph /\ k e. Z ) -> ( A ` ( k + 1 ) ) e. CC )
36 26 sselda 
 |-  ( ( ph /\ k e. Z ) -> k e. NN0 )
37 2 ffvelcdmda 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. CC )
38 36 37 syldan 
 |-  ( ( ph /\ k e. Z ) -> ( A ` k ) e. CC )
39 35 38 7 divcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( A ` ( k + 1 ) ) / ( A ` k ) ) e. CC )
40 39 abscld 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) e. RR )
41 30 40 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( D |` Z ) ` k ) e. RR )
42 5 12 20 41 climrecl 
 |-  ( ph -> L e. RR )
43 42 9 rereccld 
 |-  ( ph -> ( 1 / L ) e. RR )
44 43 rexrd 
 |-  ( ph -> ( 1 / L ) e. RR* )
45 simpr 
 |-  ( ( ph /\ x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
46 elrabi 
 |-  ( x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } -> x e. RR )
47 43 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( 1 / L ) e. RR )
48 recn 
 |-  ( x e. RR -> x e. CC )
49 48 abscld 
 |-  ( x e. RR -> ( abs ` x ) e. RR )
50 49 adantl 
 |-  ( ( ph /\ x e. RR ) -> ( abs ` x ) e. RR )
51 47 50 ltlend 
 |-  ( ( ph /\ x e. RR ) -> ( ( 1 / L ) < ( abs ` x ) <-> ( ( 1 / L ) <_ ( abs ` x ) /\ ( abs ` x ) =/= ( 1 / L ) ) ) )
52 51 simplbda 
 |-  ( ( ( ph /\ x e. RR ) /\ ( 1 / L ) < ( abs ` x ) ) -> ( abs ` x ) =/= ( 1 / L ) )
53 51 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( ( 1 / L ) < ( abs ` x ) <-> ( ( 1 / L ) <_ ( abs ` x ) /\ ( abs ` x ) =/= ( 1 / L ) ) ) )
54 simpr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( abs ` x ) =/= ( 1 / L ) )
55 54 biantrud 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( ( 1 / L ) <_ ( abs ` x ) <-> ( ( 1 / L ) <_ ( abs ` x ) /\ ( abs ` x ) =/= ( 1 / L ) ) ) )
56 47 50 lenltd 
 |-  ( ( ph /\ x e. RR ) -> ( ( 1 / L ) <_ ( abs ` x ) <-> -. ( abs ` x ) < ( 1 / L ) ) )
57 56 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( ( 1 / L ) <_ ( abs ` x ) <-> -. ( abs ` x ) < ( 1 / L ) ) )
58 53 55 57 3bitr2d 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( ( 1 / L ) < ( abs ` x ) <-> -. ( abs ` x ) < ( 1 / L ) ) )
59 1cnd 
 |-  ( ( ph /\ x e. RR ) -> 1 e. CC )
60 50 recnd 
 |-  ( ( ph /\ x e. RR ) -> ( abs ` x ) e. CC )
61 42 recnd 
 |-  ( ph -> L e. CC )
62 61 adantr 
 |-  ( ( ph /\ x e. RR ) -> L e. CC )
63 9 adantr 
 |-  ( ( ph /\ x e. RR ) -> L =/= 0 )
64 59 60 62 63 divmul3d 
 |-  ( ( ph /\ x e. RR ) -> ( ( 1 / L ) = ( abs ` x ) <-> 1 = ( ( abs ` x ) x. L ) ) )
65 eqcom 
 |-  ( ( 1 / L ) = ( abs ` x ) <-> ( abs ` x ) = ( 1 / L ) )
66 eqcom 
 |-  ( 1 = ( ( abs ` x ) x. L ) <-> ( ( abs ` x ) x. L ) = 1 )
67 64 65 66 3bitr3g 
 |-  ( ( ph /\ x e. RR ) -> ( ( abs ` x ) = ( 1 / L ) <-> ( ( abs ` x ) x. L ) = 1 ) )
68 67 necon3bid 
 |-  ( ( ph /\ x e. RR ) -> ( ( abs ` x ) =/= ( 1 / L ) <-> ( ( abs ` x ) x. L ) =/= 1 ) )
69 68 biimpa 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( ( abs ` x ) x. L ) =/= 1 )
70 1red 
 |-  ( ( ph /\ x e. RR ) -> 1 e. RR )
71 fvres 
 |-  ( k e. Z -> ( ( D |` Z ) ` k ) = ( D ` k ) )
72 71 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( ( D |` Z ) ` k ) = ( D ` k ) )
73 72 41 eqeltrrd 
 |-  ( ( ph /\ k e. Z ) -> ( D ` k ) e. RR )
74 39 absge0d 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) )
75 74 30 breqtrrd 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( ( D |` Z ) ` k ) )
76 75 72 breqtrd 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( D ` k ) )
77 5 12 8 73 76 climge0 
 |-  ( ph -> 0 <_ L )
78 42 77 9 ne0gt0d 
 |-  ( ph -> 0 < L )
79 42 78 elrpd 
 |-  ( ph -> L e. RR+ )
80 79 adantr 
 |-  ( ( ph /\ x e. RR ) -> L e. RR+ )
81 50 70 80 ltmuldivd 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( abs ` x ) x. L ) < 1 <-> ( abs ` x ) < ( 1 / L ) ) )
82 81 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( ( ( abs ` x ) x. L ) < 1 <-> ( abs ` x ) < ( 1 / L ) ) )
83 elun 
 |-  ( x e. ( ( RR i^i { 0 } ) u. ( RR \ { 0 } ) ) <-> ( x e. ( RR i^i { 0 } ) \/ x e. ( RR \ { 0 } ) ) )
84 inundif 
 |-  ( ( RR i^i { 0 } ) u. ( RR \ { 0 } ) ) = RR
85 84 eleq2i 
 |-  ( x e. ( ( RR i^i { 0 } ) u. ( RR \ { 0 } ) ) <-> x e. RR )
86 83 85 bitr3i 
 |-  ( ( x e. ( RR i^i { 0 } ) \/ x e. ( RR \ { 0 } ) ) <-> x e. RR )
87 elin 
 |-  ( x e. ( RR i^i { 0 } ) <-> ( x e. RR /\ x e. { 0 } ) )
88 87 simprbi 
 |-  ( x e. ( RR i^i { 0 } ) -> x e. { 0 } )
89 elsni 
 |-  ( x e. { 0 } -> x = 0 )
90 88 89 syl 
 |-  ( x e. ( RR i^i { 0 } ) -> x = 0 )
91 fveq2 
 |-  ( x = 0 -> ( abs ` x ) = ( abs ` 0 ) )
92 abs0 
 |-  ( abs ` 0 ) = 0
93 91 92 eqtrdi 
 |-  ( x = 0 -> ( abs ` x ) = 0 )
94 93 oveq1d 
 |-  ( x = 0 -> ( ( abs ` x ) x. L ) = ( 0 x. L ) )
95 61 mul02d 
 |-  ( ph -> ( 0 x. L ) = 0 )
96 94 95 sylan9eqr 
 |-  ( ( ph /\ x = 0 ) -> ( ( abs ` x ) x. L ) = 0 )
97 0lt1 
 |-  0 < 1
98 96 97 eqbrtrdi 
 |-  ( ( ph /\ x = 0 ) -> ( ( abs ` x ) x. L ) < 1 )
99 1 2 radcnv0 
 |-  ( ph -> 0 e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
100 eleq1 
 |-  ( x = 0 -> ( x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } <-> 0 e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
101 99 100 syl5ibrcom 
 |-  ( ph -> ( x = 0 -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
102 101 imp 
 |-  ( ( ph /\ x = 0 ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
103 98 102 2thd 
 |-  ( ( ph /\ x = 0 ) -> ( ( ( abs ` x ) x. L ) < 1 <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
104 90 103 sylan2 
 |-  ( ( ph /\ x e. ( RR i^i { 0 } ) ) -> ( ( ( abs ` x ) x. L ) < 1 <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
105 104 adantlr 
 |-  ( ( ( ph /\ ( ( abs ` x ) x. L ) =/= 1 ) /\ x e. ( RR i^i { 0 } ) ) -> ( ( ( abs ` x ) x. L ) < 1 <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
106 ax-resscn 
 |-  RR C_ CC
107 ssdif 
 |-  ( RR C_ CC -> ( RR \ { 0 } ) C_ ( CC \ { 0 } ) )
108 106 107 ax-mp 
 |-  ( RR \ { 0 } ) C_ ( CC \ { 0 } )
109 108 sseli 
 |-  ( x e. ( RR \ { 0 } ) -> x e. ( CC \ { 0 } ) )
110 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
111 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> M e. NN0 )
112 fvexd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( G ` x ) e. _V )
113 eldifi 
 |-  ( x e. ( CC \ { 0 } ) -> x e. CC )
114 1 a1i 
 |-  ( ph -> G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) ) )
115 14 mptex 
 |-  ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) e. _V
116 115 a1i 
 |-  ( ( ph /\ x e. CC ) -> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) e. _V )
117 114 116 fvmpt2d 
 |-  ( ( ph /\ x e. CC ) -> ( G ` x ) = ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
118 117 adantr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) -> ( G ` x ) = ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
119 fveq2 
 |-  ( n = k -> ( A ` n ) = ( A ` k ) )
120 oveq2 
 |-  ( n = k -> ( x ^ n ) = ( x ^ k ) )
121 119 120 oveq12d 
 |-  ( n = k -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` k ) x. ( x ^ k ) ) )
122 121 adantl 
 |-  ( ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) /\ n = k ) -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` k ) x. ( x ^ k ) ) )
123 simpr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) -> k e. NN0 )
124 ovexd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( x ^ k ) ) e. _V )
125 118 122 123 124 fvmptd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) -> ( ( G ` x ) ` k ) = ( ( A ` k ) x. ( x ^ k ) ) )
126 37 adantlr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
127 simplr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) -> x e. CC )
128 127 123 expcld 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) -> ( x ^ k ) e. CC )
129 126 128 mulcld 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( x ^ k ) ) e. CC )
130 125 129 eqeltrd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. NN0 ) -> ( ( G ` x ) ` k ) e. CC )
131 113 130 sylanl2 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. NN0 ) -> ( ( G ` x ) ` k ) e. CC )
132 131 adantlr 
 |-  ( ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) /\ k e. NN0 ) -> ( ( G ` x ) ` k ) e. CC )
133 36 adantlr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> k e. NN0 )
134 133 125 syldan 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> ( ( G ` x ) ` k ) = ( ( A ` k ) x. ( x ^ k ) ) )
135 113 134 sylanl2 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( G ` x ) ` k ) = ( ( A ` k ) x. ( x ^ k ) ) )
136 38 adantlr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( A ` k ) e. CC )
137 113 adantl 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> x e. CC )
138 137 adantr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> x e. CC )
139 36 adantlr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> k e. NN0 )
140 138 139 expcld 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( x ^ k ) e. CC )
141 7 adantlr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( A ` k ) =/= 0 )
142 eldifsni 
 |-  ( x e. ( CC \ { 0 } ) -> x =/= 0 )
143 142 ad2antlr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> x =/= 0 )
144 139 nn0zd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> k e. ZZ )
145 138 143 144 expne0d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( x ^ k ) =/= 0 )
146 136 140 141 145 mulne0d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( A ` k ) x. ( x ^ k ) ) =/= 0 )
147 135 146 eqnetrd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( G ` x ) ` k ) =/= 0 )
148 147 adantlr 
 |-  ( ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) /\ k e. Z ) -> ( ( G ` x ) ` k ) =/= 0 )
149 fvoveq1 
 |-  ( n = k -> ( ( G ` x ) ` ( n + 1 ) ) = ( ( G ` x ) ` ( k + 1 ) ) )
150 fveq2 
 |-  ( n = k -> ( ( G ` x ) ` n ) = ( ( G ` x ) ` k ) )
151 149 150 oveq12d 
 |-  ( n = k -> ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) = ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) )
152 151 fveq2d 
 |-  ( n = k -> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) = ( abs ` ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) ) )
153 152 cbvmptv 
 |-  ( n e. Z |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) = ( k e. Z |-> ( abs ` ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) ) )
154 5 reseq2i 
 |-  ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) |` Z ) = ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) |` ( ZZ>= ` M ) )
155 26 adantr 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> Z C_ NN0 )
156 155 resmptd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) |` Z ) = ( n e. Z |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) )
157 154 156 eqtr3id 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) |` ( ZZ>= ` M ) ) = ( n e. Z |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) )
158 12 adantr 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> M e. ZZ )
159 8 adantr 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> D ~~> L )
160 137 abscld 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( abs ` x ) e. RR )
161 160 recnd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( abs ` x ) e. CC )
162 14 mptex 
 |-  ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) e. _V
163 162 a1i 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) e. _V )
164 73 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( D ` k ) e. CC )
165 164 adantlr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( D ` k ) e. CC )
166 eqidd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) = ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) )
167 152 adantl 
 |-  ( ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) /\ n = k ) -> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) = ( abs ` ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) ) )
168 fvexd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( abs ` ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) ) e. _V )
169 166 167 139 168 fvmptd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) ` k ) = ( abs ` ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) ) )
170 117 adantr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> ( G ` x ) = ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
171 simpr 
 |-  ( ( ( ( ph /\ x e. CC ) /\ k e. Z ) /\ n = ( k + 1 ) ) -> n = ( k + 1 ) )
172 171 fveq2d 
 |-  ( ( ( ( ph /\ x e. CC ) /\ k e. Z ) /\ n = ( k + 1 ) ) -> ( A ` n ) = ( A ` ( k + 1 ) ) )
173 171 oveq2d 
 |-  ( ( ( ( ph /\ x e. CC ) /\ k e. Z ) /\ n = ( k + 1 ) ) -> ( x ^ n ) = ( x ^ ( k + 1 ) ) )
174 172 173 oveq12d 
 |-  ( ( ( ( ph /\ x e. CC ) /\ k e. Z ) /\ n = ( k + 1 ) ) -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` ( k + 1 ) ) x. ( x ^ ( k + 1 ) ) ) )
175 1nn0 
 |-  1 e. NN0
176 175 a1i 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> 1 e. NN0 )
177 133 176 nn0addcld 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> ( k + 1 ) e. NN0 )
178 ovexd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> ( ( A ` ( k + 1 ) ) x. ( x ^ ( k + 1 ) ) ) e. _V )
179 170 174 177 178 fvmptd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> ( ( G ` x ) ` ( k + 1 ) ) = ( ( A ` ( k + 1 ) ) x. ( x ^ ( k + 1 ) ) ) )
180 121 adantl 
 |-  ( ( ( ( ph /\ x e. CC ) /\ k e. Z ) /\ n = k ) -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` k ) x. ( x ^ k ) ) )
181 ovexd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> ( ( A ` k ) x. ( x ^ k ) ) e. _V )
182 170 180 133 181 fvmptd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> ( ( G ` x ) ` k ) = ( ( A ` k ) x. ( x ^ k ) ) )
183 179 182 oveq12d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. Z ) -> ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) = ( ( ( A ` ( k + 1 ) ) x. ( x ^ ( k + 1 ) ) ) / ( ( A ` k ) x. ( x ^ k ) ) ) )
184 113 183 sylanl2 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) = ( ( ( A ` ( k + 1 ) ) x. ( x ^ ( k + 1 ) ) ) / ( ( A ` k ) x. ( x ^ k ) ) ) )
185 35 adantlr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( A ` ( k + 1 ) ) e. CC )
186 113 177 sylanl2 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( k + 1 ) e. NN0 )
187 138 186 expcld 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( x ^ ( k + 1 ) ) e. CC )
188 185 136 187 140 141 145 divmuldivd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( ( A ` ( k + 1 ) ) / ( A ` k ) ) x. ( ( x ^ ( k + 1 ) ) / ( x ^ k ) ) ) = ( ( ( A ` ( k + 1 ) ) x. ( x ^ ( k + 1 ) ) ) / ( ( A ` k ) x. ( x ^ k ) ) ) )
189 139 nn0cnd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> k e. CC )
190 1cnd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> 1 e. CC )
191 189 190 pncan2d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( k + 1 ) - k ) = 1 )
192 191 oveq2d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( x ^ ( ( k + 1 ) - k ) ) = ( x ^ 1 ) )
193 186 nn0zd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( k + 1 ) e. ZZ )
194 138 143 144 193 expsubd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( x ^ ( ( k + 1 ) - k ) ) = ( ( x ^ ( k + 1 ) ) / ( x ^ k ) ) )
195 138 exp1d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( x ^ 1 ) = x )
196 192 194 195 3eqtr3d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( x ^ ( k + 1 ) ) / ( x ^ k ) ) = x )
197 196 oveq2d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( ( A ` ( k + 1 ) ) / ( A ` k ) ) x. ( ( x ^ ( k + 1 ) ) / ( x ^ k ) ) ) = ( ( ( A ` ( k + 1 ) ) / ( A ` k ) ) x. x ) )
198 184 188 197 3eqtr2d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) = ( ( ( A ` ( k + 1 ) ) / ( A ` k ) ) x. x ) )
199 198 fveq2d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( abs ` ( ( ( G ` x ) ` ( k + 1 ) ) / ( ( G ` x ) ` k ) ) ) = ( abs ` ( ( ( A ` ( k + 1 ) ) / ( A ` k ) ) x. x ) ) )
200 39 adantlr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( A ` ( k + 1 ) ) / ( A ` k ) ) e. CC )
201 200 138 absmuld 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( abs ` ( ( ( A ` ( k + 1 ) ) / ( A ` k ) ) x. x ) ) = ( ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) x. ( abs ` x ) ) )
202 169 199 201 3eqtrd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) ` k ) = ( ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) x. ( abs ` x ) ) )
203 72 30 eqtr3d 
 |-  ( ( ph /\ k e. Z ) -> ( D ` k ) = ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) )
204 203 adantlr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( D ` k ) = ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) )
205 204 eqcomd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) = ( D ` k ) )
206 205 oveq1d 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) x. ( abs ` x ) ) = ( ( D ` k ) x. ( abs ` x ) ) )
207 161 adantr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( abs ` x ) e. CC )
208 165 207 mulcomd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( D ` k ) x. ( abs ` x ) ) = ( ( abs ` x ) x. ( D ` k ) ) )
209 202 206 208 3eqtrd 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ k e. Z ) -> ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) ` k ) = ( ( abs ` x ) x. ( D ` k ) ) )
210 5 158 159 161 163 165 209 climmulc2 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) ~~> ( ( abs ` x ) x. L ) )
211 climres 
 |-  ( ( M e. ZZ /\ ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) e. _V ) -> ( ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) |` ( ZZ>= ` M ) ) ~~> ( ( abs ` x ) x. L ) <-> ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) ~~> ( ( abs ` x ) x. L ) ) )
212 158 162 211 sylancl 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) |` ( ZZ>= ` M ) ) ~~> ( ( abs ` x ) x. L ) <-> ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) ~~> ( ( abs ` x ) x. L ) ) )
213 210 212 mpbird 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( ( n e. NN0 |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) |` ( ZZ>= ` M ) ) ~~> ( ( abs ` x ) x. L ) )
214 157 213 eqbrtrrd 
 |-  ( ( ph /\ x e. ( CC \ { 0 } ) ) -> ( n e. Z |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) ~~> ( ( abs ` x ) x. L ) )
215 214 adantr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( n e. Z |-> ( abs ` ( ( ( G ` x ) ` ( n + 1 ) ) / ( ( G ` x ) ` n ) ) ) ) ~~> ( ( abs ` x ) x. L ) )
216 simpr 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( ( abs ` x ) x. L ) =/= 1 )
217 110 5 111 112 132 148 153 215 216 cvgdvgrat 
 |-  ( ( ( ph /\ x e. ( CC \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( ( ( abs ` x ) x. L ) < 1 <-> seq 0 ( + , ( G ` x ) ) e. dom ~~> ) )
218 109 217 sylanl2 
 |-  ( ( ( ph /\ x e. ( RR \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( ( ( abs ` x ) x. L ) < 1 <-> seq 0 ( + , ( G ` x ) ) e. dom ~~> ) )
219 eldifi 
 |-  ( x e. ( RR \ { 0 } ) -> x e. RR )
220 fveq2 
 |-  ( r = x -> ( G ` r ) = ( G ` x ) )
221 220 seqeq3d 
 |-  ( r = x -> seq 0 ( + , ( G ` r ) ) = seq 0 ( + , ( G ` x ) ) )
222 221 eleq1d 
 |-  ( r = x -> ( seq 0 ( + , ( G ` r ) ) e. dom ~~> <-> seq 0 ( + , ( G ` x ) ) e. dom ~~> ) )
223 222 elrab3 
 |-  ( x e. RR -> ( x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } <-> seq 0 ( + , ( G ` x ) ) e. dom ~~> ) )
224 219 223 syl 
 |-  ( x e. ( RR \ { 0 } ) -> ( x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } <-> seq 0 ( + , ( G ` x ) ) e. dom ~~> ) )
225 224 ad2antlr 
 |-  ( ( ( ph /\ x e. ( RR \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } <-> seq 0 ( + , ( G ` x ) ) e. dom ~~> ) )
226 218 225 bitr4d 
 |-  ( ( ( ph /\ x e. ( RR \ { 0 } ) ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( ( ( abs ` x ) x. L ) < 1 <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
227 226 an32s 
 |-  ( ( ( ph /\ ( ( abs ` x ) x. L ) =/= 1 ) /\ x e. ( RR \ { 0 } ) ) -> ( ( ( abs ` x ) x. L ) < 1 <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
228 105 227 jaodan 
 |-  ( ( ( ph /\ ( ( abs ` x ) x. L ) =/= 1 ) /\ ( x e. ( RR i^i { 0 } ) \/ x e. ( RR \ { 0 } ) ) ) -> ( ( ( abs ` x ) x. L ) < 1 <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
229 86 228 sylan2br 
 |-  ( ( ( ph /\ ( ( abs ` x ) x. L ) =/= 1 ) /\ x e. RR ) -> ( ( ( abs ` x ) x. L ) < 1 <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
230 229 an32s 
 |-  ( ( ( ph /\ x e. RR ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( ( ( abs ` x ) x. L ) < 1 <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
231 82 230 bitr3d 
 |-  ( ( ( ph /\ x e. RR ) /\ ( ( abs ` x ) x. L ) =/= 1 ) -> ( ( abs ` x ) < ( 1 / L ) <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
232 69 231 syldan 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( ( abs ` x ) < ( 1 / L ) <-> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
233 232 notbid 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( -. ( abs ` x ) < ( 1 / L ) <-> -. x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
234 58 233 bitrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( ( 1 / L ) < ( abs ` x ) <-> -. x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
235 234 biimpd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( ( 1 / L ) < ( abs ` x ) -> -. x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
236 235 impancom 
 |-  ( ( ( ph /\ x e. RR ) /\ ( 1 / L ) < ( abs ` x ) ) -> ( ( abs ` x ) =/= ( 1 / L ) -> -. x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
237 52 236 mpd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( 1 / L ) < ( abs ` x ) ) -> -. x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
238 237 ex 
 |-  ( ( ph /\ x e. RR ) -> ( ( 1 / L ) < ( abs ` x ) -> -. x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
239 238 con2d 
 |-  ( ( ph /\ x e. RR ) -> ( x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } -> -. ( 1 / L ) < ( abs ` x ) ) )
240 47 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( 1 / L ) < x ) -> ( 1 / L ) e. RR )
241 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( 1 / L ) < x ) -> x e. RR )
242 50 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( 1 / L ) < x ) -> ( abs ` x ) e. RR )
243 simpr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( 1 / L ) < x ) -> ( 1 / L ) < x )
244 241 leabsd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( 1 / L ) < x ) -> x <_ ( abs ` x ) )
245 240 241 242 243 244 ltletrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( 1 / L ) < x ) -> ( 1 / L ) < ( abs ` x ) )
246 245 ex 
 |-  ( ( ph /\ x e. RR ) -> ( ( 1 / L ) < x -> ( 1 / L ) < ( abs ` x ) ) )
247 239 246 nsyld 
 |-  ( ( ph /\ x e. RR ) -> ( x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } -> -. ( 1 / L ) < x ) )
248 46 247 sylan2 
 |-  ( ( ph /\ x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) -> ( x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } -> -. ( 1 / L ) < x ) )
249 45 248 mpd 
 |-  ( ( ph /\ x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) -> -. ( 1 / L ) < x )
250 43 renegcld 
 |-  ( ph -> -u ( 1 / L ) e. RR )
251 250 rexrd 
 |-  ( ph -> -u ( 1 / L ) e. RR* )
252 iooss1 
 |-  ( ( -u ( 1 / L ) e. RR* /\ -u ( 1 / L ) <_ x ) -> ( x (,) ( 1 / L ) ) C_ ( -u ( 1 / L ) (,) ( 1 / L ) ) )
253 251 252 sylan 
 |-  ( ( ph /\ -u ( 1 / L ) <_ x ) -> ( x (,) ( 1 / L ) ) C_ ( -u ( 1 / L ) (,) ( 1 / L ) ) )
254 253 adantlr 
 |-  ( ( ( ph /\ ( x e. RR* /\ x < ( 1 / L ) ) ) /\ -u ( 1 / L ) <_ x ) -> ( x (,) ( 1 / L ) ) C_ ( -u ( 1 / L ) (,) ( 1 / L ) ) )
255 eliooord 
 |-  ( k e. ( x (,) ( 1 / L ) ) -> ( x < k /\ k < ( 1 / L ) ) )
256 255 simpld 
 |-  ( k e. ( x (,) ( 1 / L ) ) -> x < k )
257 256 rgen 
 |-  A. k e. ( x (,) ( 1 / L ) ) x < k
258 ioon0 
 |-  ( ( x e. RR* /\ ( 1 / L ) e. RR* ) -> ( ( x (,) ( 1 / L ) ) =/= (/) <-> x < ( 1 / L ) ) )
259 44 258 sylan2 
 |-  ( ( x e. RR* /\ ph ) -> ( ( x (,) ( 1 / L ) ) =/= (/) <-> x < ( 1 / L ) ) )
260 259 ancoms 
 |-  ( ( ph /\ x e. RR* ) -> ( ( x (,) ( 1 / L ) ) =/= (/) <-> x < ( 1 / L ) ) )
261 260 biimpar 
 |-  ( ( ( ph /\ x e. RR* ) /\ x < ( 1 / L ) ) -> ( x (,) ( 1 / L ) ) =/= (/) )
262 r19.2zb 
 |-  ( ( x (,) ( 1 / L ) ) =/= (/) <-> ( A. k e. ( x (,) ( 1 / L ) ) x < k -> E. k e. ( x (,) ( 1 / L ) ) x < k ) )
263 261 262 sylib 
 |-  ( ( ( ph /\ x e. RR* ) /\ x < ( 1 / L ) ) -> ( A. k e. ( x (,) ( 1 / L ) ) x < k -> E. k e. ( x (,) ( 1 / L ) ) x < k ) )
264 257 263 mpi 
 |-  ( ( ( ph /\ x e. RR* ) /\ x < ( 1 / L ) ) -> E. k e. ( x (,) ( 1 / L ) ) x < k )
265 264 anasss 
 |-  ( ( ph /\ ( x e. RR* /\ x < ( 1 / L ) ) ) -> E. k e. ( x (,) ( 1 / L ) ) x < k )
266 265 adantr 
 |-  ( ( ( ph /\ ( x e. RR* /\ x < ( 1 / L ) ) ) /\ -u ( 1 / L ) <_ x ) -> E. k e. ( x (,) ( 1 / L ) ) x < k )
267 ssrexv 
 |-  ( ( x (,) ( 1 / L ) ) C_ ( -u ( 1 / L ) (,) ( 1 / L ) ) -> ( E. k e. ( x (,) ( 1 / L ) ) x < k -> E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k ) )
268 254 266 267 sylc 
 |-  ( ( ( ph /\ ( x e. RR* /\ x < ( 1 / L ) ) ) /\ -u ( 1 / L ) <_ x ) -> E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k )
269 simplr 
 |-  ( ( ( ph /\ x e. RR* ) /\ -. -u ( 1 / L ) <_ x ) -> x e. RR* )
270 xrltnle 
 |-  ( ( x e. RR* /\ -u ( 1 / L ) e. RR* ) -> ( x < -u ( 1 / L ) <-> -. -u ( 1 / L ) <_ x ) )
271 xrltle 
 |-  ( ( x e. RR* /\ -u ( 1 / L ) e. RR* ) -> ( x < -u ( 1 / L ) -> x <_ -u ( 1 / L ) ) )
272 270 271 sylbird 
 |-  ( ( x e. RR* /\ -u ( 1 / L ) e. RR* ) -> ( -. -u ( 1 / L ) <_ x -> x <_ -u ( 1 / L ) ) )
273 251 272 sylan2 
 |-  ( ( x e. RR* /\ ph ) -> ( -. -u ( 1 / L ) <_ x -> x <_ -u ( 1 / L ) ) )
274 273 ancoms 
 |-  ( ( ph /\ x e. RR* ) -> ( -. -u ( 1 / L ) <_ x -> x <_ -u ( 1 / L ) ) )
275 274 imp 
 |-  ( ( ( ph /\ x e. RR* ) /\ -. -u ( 1 / L ) <_ x ) -> x <_ -u ( 1 / L ) )
276 iooss1 
 |-  ( ( x e. RR* /\ x <_ -u ( 1 / L ) ) -> ( -u ( 1 / L ) (,) ( 1 / L ) ) C_ ( x (,) ( 1 / L ) ) )
277 269 275 276 syl2anc 
 |-  ( ( ( ph /\ x e. RR* ) /\ -. -u ( 1 / L ) <_ x ) -> ( -u ( 1 / L ) (,) ( 1 / L ) ) C_ ( x (,) ( 1 / L ) ) )
278 277 sselda 
 |-  ( ( ( ( ph /\ x e. RR* ) /\ -. -u ( 1 / L ) <_ x ) /\ k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) ) -> k e. ( x (,) ( 1 / L ) ) )
279 278 256 syl 
 |-  ( ( ( ( ph /\ x e. RR* ) /\ -. -u ( 1 / L ) <_ x ) /\ k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) ) -> x < k )
280 279 ralrimiva 
 |-  ( ( ( ph /\ x e. RR* ) /\ -. -u ( 1 / L ) <_ x ) -> A. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k )
281 42 78 recgt0d 
 |-  ( ph -> 0 < ( 1 / L ) )
282 43 43 281 281 addgt0d 
 |-  ( ph -> 0 < ( ( 1 / L ) + ( 1 / L ) ) )
283 43 recnd 
 |-  ( ph -> ( 1 / L ) e. CC )
284 283 283 subnegd 
 |-  ( ph -> ( ( 1 / L ) - -u ( 1 / L ) ) = ( ( 1 / L ) + ( 1 / L ) ) )
285 282 284 breqtrrd 
 |-  ( ph -> 0 < ( ( 1 / L ) - -u ( 1 / L ) ) )
286 250 43 posdifd 
 |-  ( ph -> ( -u ( 1 / L ) < ( 1 / L ) <-> 0 < ( ( 1 / L ) - -u ( 1 / L ) ) ) )
287 285 286 mpbird 
 |-  ( ph -> -u ( 1 / L ) < ( 1 / L ) )
288 ioon0 
 |-  ( ( -u ( 1 / L ) e. RR* /\ ( 1 / L ) e. RR* ) -> ( ( -u ( 1 / L ) (,) ( 1 / L ) ) =/= (/) <-> -u ( 1 / L ) < ( 1 / L ) ) )
289 251 44 288 syl2anc 
 |-  ( ph -> ( ( -u ( 1 / L ) (,) ( 1 / L ) ) =/= (/) <-> -u ( 1 / L ) < ( 1 / L ) ) )
290 287 289 mpbird 
 |-  ( ph -> ( -u ( 1 / L ) (,) ( 1 / L ) ) =/= (/) )
291 r19.2zb 
 |-  ( ( -u ( 1 / L ) (,) ( 1 / L ) ) =/= (/) <-> ( A. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k -> E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k ) )
292 290 291 sylib 
 |-  ( ph -> ( A. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k -> E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k ) )
293 292 ad2antrr 
 |-  ( ( ( ph /\ x e. RR* ) /\ -. -u ( 1 / L ) <_ x ) -> ( A. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k -> E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k ) )
294 280 293 mpd 
 |-  ( ( ( ph /\ x e. RR* ) /\ -. -u ( 1 / L ) <_ x ) -> E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k )
295 294 adantlrr 
 |-  ( ( ( ph /\ ( x e. RR* /\ x < ( 1 / L ) ) ) /\ -. -u ( 1 / L ) <_ x ) -> E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k )
296 268 295 pm2.61dan 
 |-  ( ( ph /\ ( x e. RR* /\ x < ( 1 / L ) ) ) -> E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k )
297 elioo2 
 |-  ( ( -u ( 1 / L ) e. RR* /\ ( 1 / L ) e. RR* ) -> ( x e. ( -u ( 1 / L ) (,) ( 1 / L ) ) <-> ( x e. RR /\ -u ( 1 / L ) < x /\ x < ( 1 / L ) ) ) )
298 251 44 297 syl2anc 
 |-  ( ph -> ( x e. ( -u ( 1 / L ) (,) ( 1 / L ) ) <-> ( x e. RR /\ -u ( 1 / L ) < x /\ x < ( 1 / L ) ) ) )
299 298 biimpa 
 |-  ( ( ph /\ x e. ( -u ( 1 / L ) (,) ( 1 / L ) ) ) -> ( x e. RR /\ -u ( 1 / L ) < x /\ x < ( 1 / L ) ) )
300 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
301 300 47 absltd 
 |-  ( ( ph /\ x e. RR ) -> ( ( abs ` x ) < ( 1 / L ) <-> ( -u ( 1 / L ) < x /\ x < ( 1 / L ) ) ) )
302 50 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) < ( 1 / L ) ) -> ( abs ` x ) e. RR )
303 simpr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) < ( 1 / L ) ) -> ( abs ` x ) < ( 1 / L ) )
304 302 303 ltned 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) < ( 1 / L ) ) -> ( abs ` x ) =/= ( 1 / L ) )
305 232 biimpd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) =/= ( 1 / L ) ) -> ( ( abs ` x ) < ( 1 / L ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
306 305 impancom 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) < ( 1 / L ) ) -> ( ( abs ` x ) =/= ( 1 / L ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
307 304 306 mpd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( abs ` x ) < ( 1 / L ) ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
308 307 ex 
 |-  ( ( ph /\ x e. RR ) -> ( ( abs ` x ) < ( 1 / L ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
309 301 308 sylbird 
 |-  ( ( ph /\ x e. RR ) -> ( ( -u ( 1 / L ) < x /\ x < ( 1 / L ) ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
310 309 impr 
 |-  ( ( ph /\ ( x e. RR /\ ( -u ( 1 / L ) < x /\ x < ( 1 / L ) ) ) ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
311 310 expcom 
 |-  ( ( x e. RR /\ ( -u ( 1 / L ) < x /\ x < ( 1 / L ) ) ) -> ( ph -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
312 311 3impb 
 |-  ( ( x e. RR /\ -u ( 1 / L ) < x /\ x < ( 1 / L ) ) -> ( ph -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
313 312 impcom 
 |-  ( ( ph /\ ( x e. RR /\ -u ( 1 / L ) < x /\ x < ( 1 / L ) ) ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
314 299 313 syldan 
 |-  ( ( ph /\ x e. ( -u ( 1 / L ) (,) ( 1 / L ) ) ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
315 314 ex 
 |-  ( ph -> ( x e. ( -u ( 1 / L ) (,) ( 1 / L ) ) -> x e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) )
316 315 ssrdv 
 |-  ( ph -> ( -u ( 1 / L ) (,) ( 1 / L ) ) C_ { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
317 ssrexv 
 |-  ( ( -u ( 1 / L ) (,) ( 1 / L ) ) C_ { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } -> ( E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k -> E. k e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } x < k ) )
318 316 317 syl 
 |-  ( ph -> ( E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k -> E. k e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } x < k ) )
319 318 adantr 
 |-  ( ( ph /\ ( x e. RR* /\ x < ( 1 / L ) ) ) -> ( E. k e. ( -u ( 1 / L ) (,) ( 1 / L ) ) x < k -> E. k e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } x < k ) )
320 296 319 mpd 
 |-  ( ( ph /\ ( x e. RR* /\ x < ( 1 / L ) ) ) -> E. k e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } x < k )
321 11 44 249 320 eqsupd 
 |-  ( ph -> sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) = ( 1 / L ) )
322 3 321 eqtrid 
 |-  ( ph -> R = ( 1 / L ) )