Metamath Proof Explorer

Theorem geomcau

Description: If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses lmclim2.2 
|- ( ph -> D e. ( Met ` X ) )
lmclim2.3 
|- ( ph -> F : NN --> X )
geomcau.4 
|- ( ph -> A e. RR )
geomcau.5 
|- ( ph -> B e. RR+ )
geomcau.6 
|- ( ph -> B < 1 )
geomcau.7 
|- ( ( ph /\ k e. NN ) -> ( ( F ` k ) D ( F ` ( k + 1 ) ) ) <_ ( A x. ( B ^ k ) ) )
Assertion geomcau 
|- ( ph -> F e. ( Cau ` D ) )

Proof

Step Hyp Ref Expression
1 lmclim2.2 
 |-  ( ph -> D e. ( Met ` X ) )
2 lmclim2.3 
 |-  ( ph -> F : NN --> X )
3 geomcau.4 
 |-  ( ph -> A e. RR )
4 geomcau.5 
 |-  ( ph -> B e. RR+ )
5 geomcau.6 
 |-  ( ph -> B < 1 )
6 geomcau.7 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) D ( F ` ( k + 1 ) ) ) <_ ( A x. ( B ^ k ) ) )
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 1zzd 
 |-  ( ph -> 1 e. ZZ )
9 4 rpcnd 
 |-  ( ph -> B e. CC )
10 4 rpred 
 |-  ( ph -> B e. RR )
11 4 rpge0d 
 |-  ( ph -> 0 <_ B )
12 10 11 absidd 
 |-  ( ph -> ( abs ` B ) = B )
13 12 5 eqbrtrd 
 |-  ( ph -> ( abs ` B ) < 1 )
14 9 13 expcnv 
 |-  ( ph -> ( m e. NN0 |-> ( B ^ m ) ) ~~> 0 )
15 1re 
 |-  1 e. RR
16 resubcl 
 |-  ( ( 1 e. RR /\ B e. RR ) -> ( 1 - B ) e. RR )
17 15 10 16 sylancr 
 |-  ( ph -> ( 1 - B ) e. RR )
18 posdif 
 |-  ( ( B e. RR /\ 1 e. RR ) -> ( B < 1 <-> 0 < ( 1 - B ) ) )
19 10 15 18 sylancl 
 |-  ( ph -> ( B < 1 <-> 0 < ( 1 - B ) ) )
20 5 19 mpbid 
 |-  ( ph -> 0 < ( 1 - B ) )
21 17 20 elrpd 
 |-  ( ph -> ( 1 - B ) e. RR+ )
22 3 21 rerpdivcld 
 |-  ( ph -> ( A / ( 1 - B ) ) e. RR )
23 22 recnd 
 |-  ( ph -> ( A / ( 1 - B ) ) e. CC )
24 nnex 
 |-  NN e. _V
25 24 mptex 
 |-  ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) ) e. _V
26 25 a1i 
 |-  ( ph -> ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) ) e. _V )
27 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
28 27 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. NN0 )
29 oveq2 
 |-  ( m = n -> ( B ^ m ) = ( B ^ n ) )
30 eqid 
 |-  ( m e. NN0 |-> ( B ^ m ) ) = ( m e. NN0 |-> ( B ^ m ) )
31 ovex 
 |-  ( B ^ n ) e. _V
32 29 30 31 fvmpt 
 |-  ( n e. NN0 -> ( ( m e. NN0 |-> ( B ^ m ) ) ` n ) = ( B ^ n ) )
33 28 32 syl 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN0 |-> ( B ^ m ) ) ` n ) = ( B ^ n ) )
34 nnz 
 |-  ( n e. NN -> n e. ZZ )
35 rpexpcl 
 |-  ( ( B e. RR+ /\ n e. ZZ ) -> ( B ^ n ) e. RR+ )
36 4 34 35 syl2an 
 |-  ( ( ph /\ n e. NN ) -> ( B ^ n ) e. RR+ )
37 36 rpcnd 
 |-  ( ( ph /\ n e. NN ) -> ( B ^ n ) e. CC )
38 33 37 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN0 |-> ( B ^ m ) ) ` n ) e. CC )
39 23 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( A / ( 1 - B ) ) e. CC )
40 37 39 mulcomd 
 |-  ( ( ph /\ n e. NN ) -> ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) = ( ( A / ( 1 - B ) ) x. ( B ^ n ) ) )
41 29 oveq1d 
 |-  ( m = n -> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) = ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) )
42 eqid 
 |-  ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) ) = ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) )
43 ovex 
 |-  ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) e. _V
44 41 42 43 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) ) ` n ) = ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) )
45 44 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) ) ` n ) = ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) )
46 33 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( A / ( 1 - B ) ) x. ( ( m e. NN0 |-> ( B ^ m ) ) ` n ) ) = ( ( A / ( 1 - B ) ) x. ( B ^ n ) ) )
47 40 45 46 3eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) ) ` n ) = ( ( A / ( 1 - B ) ) x. ( ( m e. NN0 |-> ( B ^ m ) ) ` n ) ) )
48 7 8 14 23 26 38 47 climmulc2 
 |-  ( ph -> ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) ) ~~> ( ( A / ( 1 - B ) ) x. 0 ) )
49 23 mul01d 
 |-  ( ph -> ( ( A / ( 1 - B ) ) x. 0 ) = 0 )
50 48 49 breqtrd 
 |-  ( ph -> ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) ) ~~> 0 )
51 36 rpred 
 |-  ( ( ph /\ n e. NN ) -> ( B ^ n ) e. RR )
52 22 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( A / ( 1 - B ) ) e. RR )
53 51 52 remulcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) e. RR )
54 53 recnd 
 |-  ( ( ph /\ n e. NN ) -> ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) e. CC )
55 7 8 26 45 54 clim0c 
 |-  ( ph -> ( ( m e. NN |-> ( ( B ^ m ) x. ( A / ( 1 - B ) ) ) ) ~~> 0 <-> A. x e. RR+ E. j e. NN A. n e. ( ZZ>= ` j ) ( abs ` ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) ) < x ) )
56 50 55 mpbid 
 |-  ( ph -> A. x e. RR+ E. j e. NN A. n e. ( ZZ>= ` j ) ( abs ` ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) ) < x )
57 nnz 
 |-  ( j e. NN -> j e. ZZ )
58 57 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> j e. ZZ )
59 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
60 oveq2 
 |-  ( n = j -> ( B ^ n ) = ( B ^ j ) )
61 60 fvoveq1d 
 |-  ( n = j -> ( abs ` ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) ) = ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) )
62 61 breq1d 
 |-  ( n = j -> ( ( abs ` ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) ) < x <-> ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) < x ) )
63 62 rspcv 
 |-  ( j e. ( ZZ>= ` j ) -> ( A. n e. ( ZZ>= ` j ) ( abs ` ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) ) < x -> ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) < x ) )
64 58 59 63 3syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( A. n e. ( ZZ>= ` j ) ( abs ` ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) ) < x -> ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) < x ) )
65 1 adantr 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> D e. ( Met ` X ) )
66 simpl 
 |-  ( ( j e. NN /\ n e. ( ZZ>= ` j ) ) -> j e. NN )
67 ffvelcdm 
 |-  ( ( F : NN --> X /\ j e. NN ) -> ( F ` j ) e. X )
68 2 66 67 syl2an 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( F ` j ) e. X )
69 eluznn 
 |-  ( ( j e. NN /\ n e. ( ZZ>= ` j ) ) -> n e. NN )
70 ffvelcdm 
 |-  ( ( F : NN --> X /\ n e. NN ) -> ( F ` n ) e. X )
71 2 69 70 syl2an 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( F ` n ) e. X )
72 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` j ) e. X /\ ( F ` n ) e. X ) -> ( ( F ` j ) D ( F ` n ) ) e. RR )
73 65 68 71 72 syl3anc 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( F ` j ) D ( F ` n ) ) e. RR )
74 eqid 
 |-  ( ZZ>= ` j ) = ( ZZ>= ` j )
75 nnnn0 
 |-  ( j e. NN -> j e. NN0 )
76 75 ad2antrl 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> j e. NN0 )
77 76 nn0zd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> j e. ZZ )
78 oveq2 
 |-  ( m = k -> ( B ^ m ) = ( B ^ k ) )
79 78 oveq2d 
 |-  ( m = k -> ( A x. ( B ^ m ) ) = ( A x. ( B ^ k ) ) )
80 eqid 
 |-  ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) = ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) )
81 ovex 
 |-  ( A x. ( B ^ k ) ) e. _V
82 79 80 81 fvmpt 
 |-  ( k e. ( ZZ>= ` j ) -> ( ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) ` k ) = ( A x. ( B ^ k ) ) )
83 82 adantl 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) ` k ) = ( A x. ( B ^ k ) ) )
84 3 ad2antrr 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> A e. RR )
85 10 ad2antrr 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> B e. RR )
86 eluznn0 
 |-  ( ( j e. NN0 /\ k e. ( ZZ>= ` j ) ) -> k e. NN0 )
87 76 86 sylan 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. NN0 )
88 85 87 reexpcld 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( B ^ k ) e. RR )
89 84 88 remulcld 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( A x. ( B ^ k ) ) e. RR )
90 89 recnd 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( A x. ( B ^ k ) ) e. CC )
91 3 recnd 
 |-  ( ph -> A e. CC )
92 91 adantr 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> A e. CC )
93 9 adantr 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> B e. CC )
94 13 adantr 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` B ) < 1 )
95 eqid 
 |-  ( m e. ( ZZ>= ` j ) |-> ( B ^ m ) ) = ( m e. ( ZZ>= ` j ) |-> ( B ^ m ) )
96 ovex 
 |-  ( B ^ k ) e. _V
97 78 95 96 fvmpt 
 |-  ( k e. ( ZZ>= ` j ) -> ( ( m e. ( ZZ>= ` j ) |-> ( B ^ m ) ) ` k ) = ( B ^ k ) )
98 97 adantl 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( m e. ( ZZ>= ` j ) |-> ( B ^ m ) ) ` k ) = ( B ^ k ) )
99 93 94 76 98 geolim2 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> seq j ( + , ( m e. ( ZZ>= ` j ) |-> ( B ^ m ) ) ) ~~> ( ( B ^ j ) / ( 1 - B ) ) )
100 88 recnd 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( B ^ k ) e. CC )
101 98 100 eqeltrd 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( m e. ( ZZ>= ` j ) |-> ( B ^ m ) ) ` k ) e. CC )
102 98 oveq2d 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( A x. ( ( m e. ( ZZ>= ` j ) |-> ( B ^ m ) ) ` k ) ) = ( A x. ( B ^ k ) ) )
103 83 102 eqtr4d 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) ` k ) = ( A x. ( ( m e. ( ZZ>= ` j ) |-> ( B ^ m ) ) ` k ) ) )
104 74 77 92 99 101 103 isermulc2 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> seq j ( + , ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) ) ~~> ( A x. ( ( B ^ j ) / ( 1 - B ) ) ) )
105 4 adantr 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> B e. RR+ )
106 105 77 rpexpcld 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( B ^ j ) e. RR+ )
107 106 rpcnd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( B ^ j ) e. CC )
108 17 recnd 
 |-  ( ph -> ( 1 - B ) e. CC )
109 108 adantr 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( 1 - B ) e. CC )
110 21 rpne0d 
 |-  ( ph -> ( 1 - B ) =/= 0 )
111 110 adantr 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( 1 - B ) =/= 0 )
112 92 107 109 111 div12d 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( A x. ( ( B ^ j ) / ( 1 - B ) ) ) = ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) )
113 104 112 breqtrd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> seq j ( + , ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) ) ~~> ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) )
114 74 77 83 90 113 isumclim 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( ZZ>= ` j ) ( A x. ( B ^ k ) ) = ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) )
115 seqex 
 |-  seq j ( + , ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) ) e. _V
116 ovex 
 |-  ( A x. ( ( B ^ j ) / ( 1 - B ) ) ) e. _V
117 115 116 breldm 
 |-  ( seq j ( + , ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) ) ~~> ( A x. ( ( B ^ j ) / ( 1 - B ) ) ) -> seq j ( + , ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) ) e. dom ~~> )
118 104 117 syl 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> seq j ( + , ( m e. ( ZZ>= ` j ) |-> ( A x. ( B ^ m ) ) ) ) e. dom ~~> )
119 74 77 83 89 118 isumrecl 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( ZZ>= ` j ) ( A x. ( B ^ k ) ) e. RR )
120 114 119 eqeltrrd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) e. RR )
121 120 recnd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) e. CC )
122 121 abscld 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) e. RR )
123 fzfid 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( j ... ( n - 1 ) ) e. Fin )
124 simpll 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( j ... ( n - 1 ) ) ) -> ph )
125 elfzuz 
 |-  ( k e. ( j ... ( n - 1 ) ) -> k e. ( ZZ>= ` j ) )
126 simprl 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> j e. NN )
127 eluznn 
 |-  ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
128 126 127 sylan 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
129 125 128 sylan2 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( j ... ( n - 1 ) ) ) -> k e. NN )
130 1 adantr 
 |-  ( ( ph /\ k e. NN ) -> D e. ( Met ` X ) )
131 2 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. X )
132 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
133 ffvelcdm 
 |-  ( ( F : NN --> X /\ ( k + 1 ) e. NN ) -> ( F ` ( k + 1 ) ) e. X )
134 2 132 133 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) e. X )
135 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` k ) e. X /\ ( F ` ( k + 1 ) ) e. X ) -> ( ( F ` k ) D ( F ` ( k + 1 ) ) ) e. RR )
136 130 131 134 135 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) D ( F ` ( k + 1 ) ) ) e. RR )
137 124 129 136 syl2anc 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( j ... ( n - 1 ) ) ) -> ( ( F ` k ) D ( F ` ( k + 1 ) ) ) e. RR )
138 123 137 fsumrecl 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( j ... ( n - 1 ) ) ( ( F ` k ) D ( F ` ( k + 1 ) ) ) e. RR )
139 simprr 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> n e. ( ZZ>= ` j ) )
140 elfzuz 
 |-  ( k e. ( j ... n ) -> k e. ( ZZ>= ` j ) )
141 simpll 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ph )
142 141 128 131 syl2anc 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. X )
143 140 142 sylan2 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( j ... n ) ) -> ( F ` k ) e. X )
144 65 139 143 mettrifi 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( F ` j ) D ( F ` n ) ) <_ sum_ k e. ( j ... ( n - 1 ) ) ( ( F ` k ) D ( F ` ( k + 1 ) ) ) )
145 125 89 sylan2 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( j ... ( n - 1 ) ) ) -> ( A x. ( B ^ k ) ) e. RR )
146 123 145 fsumrecl 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( j ... ( n - 1 ) ) ( A x. ( B ^ k ) ) e. RR )
147 124 129 6 syl2anc 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( j ... ( n - 1 ) ) ) -> ( ( F ` k ) D ( F ` ( k + 1 ) ) ) <_ ( A x. ( B ^ k ) ) )
148 123 137 145 147 fsumle 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( j ... ( n - 1 ) ) ( ( F ` k ) D ( F ` ( k + 1 ) ) ) <_ sum_ k e. ( j ... ( n - 1 ) ) ( A x. ( B ^ k ) ) )
149 fzssuz 
 |-  ( j ... ( n - 1 ) ) C_ ( ZZ>= ` j )
150 149 a1i 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( j ... ( n - 1 ) ) C_ ( ZZ>= ` j ) )
151 0red 
 |-  ( ( ph /\ k e. NN ) -> 0 e. RR )
152 nnz 
 |-  ( k e. NN -> k e. ZZ )
153 rpexpcl 
 |-  ( ( B e. RR+ /\ k e. ZZ ) -> ( B ^ k ) e. RR+ )
154 4 152 153 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( B ^ k ) e. RR+ )
155 136 154 rerpdivcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( F ` k ) D ( F ` ( k + 1 ) ) ) / ( B ^ k ) ) e. RR )
156 3 adantr 
 |-  ( ( ph /\ k e. NN ) -> A e. RR )
157 metge0 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` k ) e. X /\ ( F ` ( k + 1 ) ) e. X ) -> 0 <_ ( ( F ` k ) D ( F ` ( k + 1 ) ) ) )
158 130 131 134 157 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> 0 <_ ( ( F ` k ) D ( F ` ( k + 1 ) ) ) )
159 136 154 158 divge0d 
 |-  ( ( ph /\ k e. NN ) -> 0 <_ ( ( ( F ` k ) D ( F ` ( k + 1 ) ) ) / ( B ^ k ) ) )
160 136 156 154 ledivmul2d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( ( F ` k ) D ( F ` ( k + 1 ) ) ) / ( B ^ k ) ) <_ A <-> ( ( F ` k ) D ( F ` ( k + 1 ) ) ) <_ ( A x. ( B ^ k ) ) ) )
161 6 160 mpbird 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( F ` k ) D ( F ` ( k + 1 ) ) ) / ( B ^ k ) ) <_ A )
162 151 155 156 159 161 letrd 
 |-  ( ( ph /\ k e. NN ) -> 0 <_ A )
163 141 128 162 syl2anc 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> 0 <_ A )
164 141 128 154 syl2anc 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( B ^ k ) e. RR+ )
165 164 rpge0d 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> 0 <_ ( B ^ k ) )
166 84 88 163 165 mulge0d 
 |-  ( ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ZZ>= ` j ) ) -> 0 <_ ( A x. ( B ^ k ) ) )
167 74 77 123 150 83 89 166 118 isumless 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( j ... ( n - 1 ) ) ( A x. ( B ^ k ) ) <_ sum_ k e. ( ZZ>= ` j ) ( A x. ( B ^ k ) ) )
168 138 146 119 148 167 letrd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( j ... ( n - 1 ) ) ( ( F ` k ) D ( F ` ( k + 1 ) ) ) <_ sum_ k e. ( ZZ>= ` j ) ( A x. ( B ^ k ) ) )
169 73 138 119 144 168 letrd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( F ` j ) D ( F ` n ) ) <_ sum_ k e. ( ZZ>= ` j ) ( A x. ( B ^ k ) ) )
170 169 114 breqtrd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( F ` j ) D ( F ` n ) ) <_ ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) )
171 120 leabsd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) <_ ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) )
172 73 120 122 170 171 letrd 
 |-  ( ( ph /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( F ` j ) D ( F ` n ) ) <_ ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) )
173 172 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( F ` j ) D ( F ` n ) ) <_ ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) )
174 73 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( F ` j ) D ( F ` n ) ) e. RR )
175 122 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) e. RR )
176 rpre 
 |-  ( x e. RR+ -> x e. RR )
177 176 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> x e. RR )
178 lelttr 
 |-  ( ( ( ( F ` j ) D ( F ` n ) ) e. RR /\ ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) e. RR /\ x e. RR ) -> ( ( ( ( F ` j ) D ( F ` n ) ) <_ ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) /\ ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) < x ) -> ( ( F ` j ) D ( F ` n ) ) < x ) )
179 174 175 177 178 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( ( F ` j ) D ( F ` n ) ) <_ ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) /\ ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) < x ) -> ( ( F ` j ) D ( F ` n ) ) < x ) )
180 173 179 mpand 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ n e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) < x -> ( ( F ` j ) D ( F ` n ) ) < x ) )
181 180 anassrs 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) /\ n e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) < x -> ( ( F ` j ) D ( F ` n ) ) < x ) )
182 181 ralrimdva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( abs ` ( ( B ^ j ) x. ( A / ( 1 - B ) ) ) ) < x -> A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x ) )
183 64 182 syld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( A. n e. ( ZZ>= ` j ) ( abs ` ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) ) < x -> A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x ) )
184 183 reximdva 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. NN A. n e. ( ZZ>= ` j ) ( abs ` ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) ) < x -> E. j e. NN A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x ) )
185 184 ralimdva 
 |-  ( ph -> ( A. x e. RR+ E. j e. NN A. n e. ( ZZ>= ` j ) ( abs ` ( ( B ^ n ) x. ( A / ( 1 - B ) ) ) ) < x -> A. x e. RR+ E. j e. NN A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x ) )
186 56 185 mpd 
 |-  ( ph -> A. x e. RR+ E. j e. NN A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x )
187 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
188 1 187 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
189 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( F ` n ) )
190 eqidd 
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) = ( F ` j ) )
191 7 188 8 189 190 2 iscauf 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> A. x e. RR+ E. j e. NN A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x ) )
192 186 191 mpbird 
 |-  ( ph -> F e. ( Cau ` D ) )