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 ffvelrn
 |-  ( ( 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 ffvelrn
 |-  ( ( 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 ffvelrnda
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. X )
132 peano2nn
 |-  ( k e. NN -> ( k + 1 ) e. NN )
133 ffvelrn
 |-  ( ( 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 ) )