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 syl5eq
 |-  ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 syl5eq
 |-  ( ph -> R = ( 1 / L ) )