Metamath Proof Explorer

Theorem bfplem1

Description: Lemma for bfp . The sequence G , which simply starts from any point in the space and iterates F , satisfies the property that the distance from G ( n ) to G ( n + 1 ) decreases by at least K after each step. Thus, the total distance from any G ( i ) to G ( j ) is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point ( ( ~>tJ )G ) since the space is complete. (Contributed by Jeff Madsen, 17-Jun-2014)

Ref Expression
Hypotheses bfp.2 
|- ( ph -> D e. ( CMet ` X ) )
bfp.3 
|- ( ph -> X =/= (/) )
bfp.4 
|- ( ph -> K e. RR+ )
bfp.5 
|- ( ph -> K < 1 )
bfp.6 
|- ( ph -> F : X --> X )
bfp.7 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
bfp.8 
|- J = ( MetOpen ` D )
bfp.9 
|- ( ph -> A e. X )
bfp.10 
|- G = seq 1 ( ( F o. 1st ) , ( NN X. { A } ) )
Assertion bfplem1 
|- ( ph -> G ( ~~>t ` J ) ( ( ~~>t ` J ) ` G ) )

Proof

Step Hyp Ref Expression
1 bfp.2 
 |-  ( ph -> D e. ( CMet ` X ) )
2 bfp.3 
 |-  ( ph -> X =/= (/) )
3 bfp.4 
 |-  ( ph -> K e. RR+ )
4 bfp.5 
 |-  ( ph -> K < 1 )
5 bfp.6 
 |-  ( ph -> F : X --> X )
6 bfp.7 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
7 bfp.8 
 |-  J = ( MetOpen ` D )
8 bfp.9 
 |-  ( ph -> A e. X )
9 bfp.10 
 |-  G = seq 1 ( ( F o. 1st ) , ( NN X. { A } ) )
10 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
11 1 10 syl 
 |-  ( ph -> D e. ( Met ` X ) )
12 nnuz 
 |-  NN = ( ZZ>= ` 1 )
13 1zzd 
 |-  ( ph -> 1 e. ZZ )
14 12 9 13 8 5 algrf 
 |-  ( ph -> G : NN --> X )
15 5 8 ffvelrnd 
 |-  ( ph -> ( F ` A ) e. X )
16 metcl 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ ( F ` A ) e. X ) -> ( A D ( F ` A ) ) e. RR )
17 11 8 15 16 syl3anc 
 |-  ( ph -> ( A D ( F ` A ) ) e. RR )
18 17 3 rerpdivcld 
 |-  ( ph -> ( ( A D ( F ` A ) ) / K ) e. RR )
19 fveq2 
 |-  ( j = 1 -> ( G ` j ) = ( G ` 1 ) )
20 fvoveq1 
 |-  ( j = 1 -> ( G ` ( j + 1 ) ) = ( G ` ( 1 + 1 ) ) )
21 19 20 oveq12d 
 |-  ( j = 1 -> ( ( G ` j ) D ( G ` ( j + 1 ) ) ) = ( ( G ` 1 ) D ( G ` ( 1 + 1 ) ) ) )
22 oveq2 
 |-  ( j = 1 -> ( K ^ j ) = ( K ^ 1 ) )
23 22 oveq2d 
 |-  ( j = 1 -> ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ j ) ) = ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ 1 ) ) )
24 21 23 breq12d 
 |-  ( j = 1 -> ( ( ( G ` j ) D ( G ` ( j + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ j ) ) <-> ( ( G ` 1 ) D ( G ` ( 1 + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ 1 ) ) ) )
25 24 imbi2d 
 |-  ( j = 1 -> ( ( ph -> ( ( G ` j ) D ( G ` ( j + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ j ) ) ) <-> ( ph -> ( ( G ` 1 ) D ( G ` ( 1 + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ 1 ) ) ) ) )
26 fveq2 
 |-  ( j = k -> ( G ` j ) = ( G ` k ) )
27 fvoveq1 
 |-  ( j = k -> ( G ` ( j + 1 ) ) = ( G ` ( k + 1 ) ) )
28 26 27 oveq12d 
 |-  ( j = k -> ( ( G ` j ) D ( G ` ( j + 1 ) ) ) = ( ( G ` k ) D ( G ` ( k + 1 ) ) ) )
29 oveq2 
 |-  ( j = k -> ( K ^ j ) = ( K ^ k ) )
30 29 oveq2d 
 |-  ( j = k -> ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ j ) ) = ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) )
31 28 30 breq12d 
 |-  ( j = k -> ( ( ( G ` j ) D ( G ` ( j + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ j ) ) <-> ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) ) )
32 31 imbi2d 
 |-  ( j = k -> ( ( ph -> ( ( G ` j ) D ( G ` ( j + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ j ) ) ) <-> ( ph -> ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) ) ) )
33 fveq2 
 |-  ( j = ( k + 1 ) -> ( G ` j ) = ( G ` ( k + 1 ) ) )
34 fvoveq1 
 |-  ( j = ( k + 1 ) -> ( G ` ( j + 1 ) ) = ( G ` ( ( k + 1 ) + 1 ) ) )
35 33 34 oveq12d 
 |-  ( j = ( k + 1 ) -> ( ( G ` j ) D ( G ` ( j + 1 ) ) ) = ( ( G ` ( k + 1 ) ) D ( G ` ( ( k + 1 ) + 1 ) ) ) )
36 oveq2 
 |-  ( j = ( k + 1 ) -> ( K ^ j ) = ( K ^ ( k + 1 ) ) )
37 36 oveq2d 
 |-  ( j = ( k + 1 ) -> ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ j ) ) = ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) )
38 35 37 breq12d 
 |-  ( j = ( k + 1 ) -> ( ( ( G ` j ) D ( G ` ( j + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ j ) ) <-> ( ( G ` ( k + 1 ) ) D ( G ` ( ( k + 1 ) + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) )
39 38 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ph -> ( ( G ` j ) D ( G ` ( j + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ j ) ) ) <-> ( ph -> ( ( G ` ( k + 1 ) ) D ( G ` ( ( k + 1 ) + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) ) )
40 17 leidd 
 |-  ( ph -> ( A D ( F ` A ) ) <_ ( A D ( F ` A ) ) )
41 12 9 13 8 algr0 
 |-  ( ph -> ( G ` 1 ) = A )
42 1nn 
 |-  1 e. NN
43 12 9 13 8 5 algrp1 
 |-  ( ( ph /\ 1 e. NN ) -> ( G ` ( 1 + 1 ) ) = ( F ` ( G ` 1 ) ) )
44 42 43 mpan2 
 |-  ( ph -> ( G ` ( 1 + 1 ) ) = ( F ` ( G ` 1 ) ) )
45 41 fveq2d 
 |-  ( ph -> ( F ` ( G ` 1 ) ) = ( F ` A ) )
46 44 45 eqtrd 
 |-  ( ph -> ( G ` ( 1 + 1 ) ) = ( F ` A ) )
47 41 46 oveq12d 
 |-  ( ph -> ( ( G ` 1 ) D ( G ` ( 1 + 1 ) ) ) = ( A D ( F ` A ) ) )
48 3 rpred 
 |-  ( ph -> K e. RR )
49 48 recnd 
 |-  ( ph -> K e. CC )
50 49 exp1d 
 |-  ( ph -> ( K ^ 1 ) = K )
51 50 oveq2d 
 |-  ( ph -> ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ 1 ) ) = ( ( ( A D ( F ` A ) ) / K ) x. K ) )
52 17 recnd 
 |-  ( ph -> ( A D ( F ` A ) ) e. CC )
53 3 rpne0d 
 |-  ( ph -> K =/= 0 )
54 52 49 53 divcan1d 
 |-  ( ph -> ( ( ( A D ( F ` A ) ) / K ) x. K ) = ( A D ( F ` A ) ) )
55 51 54 eqtrd 
 |-  ( ph -> ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ 1 ) ) = ( A D ( F ` A ) ) )
56 40 47 55 3brtr4d 
 |-  ( ph -> ( ( G ` 1 ) D ( G ` ( 1 + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ 1 ) ) )
57 14 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) e. X )
58 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
59 ffvelrn 
 |-  ( ( G : NN --> X /\ ( k + 1 ) e. NN ) -> ( G ` ( k + 1 ) ) e. X )
60 14 58 59 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( G ` ( k + 1 ) ) e. X )
61 57 60 jca 
 |-  ( ( ph /\ k e. NN ) -> ( ( G ` k ) e. X /\ ( G ` ( k + 1 ) ) e. X ) )
62 6 ralrimivva 
 |-  ( ph -> A. x e. X A. y e. X ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
63 62 adantr 
 |-  ( ( ph /\ k e. NN ) -> A. x e. X A. y e. X ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
64 fveq2 
 |-  ( x = ( G ` k ) -> ( F ` x ) = ( F ` ( G ` k ) ) )
65 64 oveq1d 
 |-  ( x = ( G ` k ) -> ( ( F ` x ) D ( F ` y ) ) = ( ( F ` ( G ` k ) ) D ( F ` y ) ) )
66 oveq1 
 |-  ( x = ( G ` k ) -> ( x D y ) = ( ( G ` k ) D y ) )
67 66 oveq2d 
 |-  ( x = ( G ` k ) -> ( K x. ( x D y ) ) = ( K x. ( ( G ` k ) D y ) ) )
68 65 67 breq12d 
 |-  ( x = ( G ` k ) -> ( ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) <-> ( ( F ` ( G ` k ) ) D ( F ` y ) ) <_ ( K x. ( ( G ` k ) D y ) ) ) )
69 fveq2 
 |-  ( y = ( G ` ( k + 1 ) ) -> ( F ` y ) = ( F ` ( G ` ( k + 1 ) ) ) )
70 69 oveq2d 
 |-  ( y = ( G ` ( k + 1 ) ) -> ( ( F ` ( G ` k ) ) D ( F ` y ) ) = ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) )
71 oveq2 
 |-  ( y = ( G ` ( k + 1 ) ) -> ( ( G ` k ) D y ) = ( ( G ` k ) D ( G ` ( k + 1 ) ) ) )
72 71 oveq2d 
 |-  ( y = ( G ` ( k + 1 ) ) -> ( K x. ( ( G ` k ) D y ) ) = ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) )
73 70 72 breq12d 
 |-  ( y = ( G ` ( k + 1 ) ) -> ( ( ( F ` ( G ` k ) ) D ( F ` y ) ) <_ ( K x. ( ( G ` k ) D y ) ) <-> ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) <_ ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) ) )
74 68 73 rspc2v 
 |-  ( ( ( G ` k ) e. X /\ ( G ` ( k + 1 ) ) e. X ) -> ( A. x e. X A. y e. X ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) -> ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) <_ ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) ) )
75 61 63 74 sylc 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) <_ ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) )
76 11 adantr 
 |-  ( ( ph /\ k e. NN ) -> D e. ( Met ` X ) )
77 5 adantr 
 |-  ( ( ph /\ k e. NN ) -> F : X --> X )
78 77 57 ffvelrnd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( G ` k ) ) e. X )
79 77 60 ffvelrnd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( G ` ( k + 1 ) ) ) e. X )
80 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` ( G ` k ) ) e. X /\ ( F ` ( G ` ( k + 1 ) ) ) e. X ) -> ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) e. RR )
81 76 78 79 80 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) e. RR )
82 48 adantr 
 |-  ( ( ph /\ k e. NN ) -> K e. RR )
83 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( G ` k ) e. X /\ ( G ` ( k + 1 ) ) e. X ) -> ( ( G ` k ) D ( G ` ( k + 1 ) ) ) e. RR )
84 76 57 60 83 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( G ` k ) D ( G ` ( k + 1 ) ) ) e. RR )
85 82 84 remulcld 
 |-  ( ( ph /\ k e. NN ) -> ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) e. RR )
86 18 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( ( A D ( F ` A ) ) / K ) e. RR )
87 58 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
88 87 nnnn0d 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN0 )
89 82 88 reexpcld 
 |-  ( ( ph /\ k e. NN ) -> ( K ^ ( k + 1 ) ) e. RR )
90 86 89 remulcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) e. RR )
91 letr 
 |-  ( ( ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) e. RR /\ ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) e. RR /\ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) e. RR ) -> ( ( ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) <_ ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) /\ ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) -> ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) )
92 81 85 90 91 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) <_ ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) /\ ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) -> ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) )
93 75 92 mpand 
 |-  ( ( ph /\ k e. NN ) -> ( ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) -> ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) )
94 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
95 reexpcl 
 |-  ( ( K e. RR /\ k e. NN0 ) -> ( K ^ k ) e. RR )
96 48 94 95 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( K ^ k ) e. RR )
97 86 96 remulcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) e. RR )
98 3 rpgt0d 
 |-  ( ph -> 0 < K )
99 98 adantr 
 |-  ( ( ph /\ k e. NN ) -> 0 < K )
100 lemul1 
 |-  ( ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) e. RR /\ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) e. RR /\ ( K e. RR /\ 0 < K ) ) -> ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) <-> ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) x. K ) <_ ( ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) x. K ) ) )
101 84 97 82 99 100 syl112anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) <-> ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) x. K ) <_ ( ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) x. K ) ) )
102 84 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( ( G ` k ) D ( G ` ( k + 1 ) ) ) e. CC )
103 49 adantr 
 |-  ( ( ph /\ k e. NN ) -> K e. CC )
104 102 103 mulcomd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) x. K ) = ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) )
105 86 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( ( A D ( F ` A ) ) / K ) e. CC )
106 96 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( K ^ k ) e. CC )
107 105 106 103 mulassd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) x. K ) = ( ( ( A D ( F ` A ) ) / K ) x. ( ( K ^ k ) x. K ) ) )
108 expp1 
 |-  ( ( K e. CC /\ k e. NN0 ) -> ( K ^ ( k + 1 ) ) = ( ( K ^ k ) x. K ) )
109 49 94 108 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( K ^ ( k + 1 ) ) = ( ( K ^ k ) x. K ) )
110 109 oveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) = ( ( ( A D ( F ` A ) ) / K ) x. ( ( K ^ k ) x. K ) ) )
111 107 110 eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) x. K ) = ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) )
112 104 111 breq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) x. K ) <_ ( ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) x. K ) <-> ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) )
113 101 112 bitrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) <-> ( K x. ( ( G ` k ) D ( G ` ( k + 1 ) ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) )
114 12 9 13 8 5 algrp1 
 |-  ( ( ph /\ k e. NN ) -> ( G ` ( k + 1 ) ) = ( F ` ( G ` k ) ) )
115 12 9 13 8 5 algrp1 
 |-  ( ( ph /\ ( k + 1 ) e. NN ) -> ( G ` ( ( k + 1 ) + 1 ) ) = ( F ` ( G ` ( k + 1 ) ) ) )
116 58 115 sylan2 
 |-  ( ( ph /\ k e. NN ) -> ( G ` ( ( k + 1 ) + 1 ) ) = ( F ` ( G ` ( k + 1 ) ) ) )
117 114 116 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( G ` ( k + 1 ) ) D ( G ` ( ( k + 1 ) + 1 ) ) ) = ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) )
118 117 breq1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( G ` ( k + 1 ) ) D ( G ` ( ( k + 1 ) + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) <-> ( ( F ` ( G ` k ) ) D ( F ` ( G ` ( k + 1 ) ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) )
119 93 113 118 3imtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) -> ( ( G ` ( k + 1 ) ) D ( G ` ( ( k + 1 ) + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) )
120 119 expcom 
 |-  ( k e. NN -> ( ph -> ( ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) -> ( ( G ` ( k + 1 ) ) D ( G ` ( ( k + 1 ) + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) ) )
121 120 a2d 
 |-  ( k e. NN -> ( ( ph -> ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) ) -> ( ph -> ( ( G ` ( k + 1 ) ) D ( G ` ( ( k + 1 ) + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ ( k + 1 ) ) ) ) ) )
122 25 32 39 32 56 121 nnind 
 |-  ( k e. NN -> ( ph -> ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) ) )
123 122 impcom 
 |-  ( ( ph /\ k e. NN ) -> ( ( G ` k ) D ( G ` ( k + 1 ) ) ) <_ ( ( ( A D ( F ` A ) ) / K ) x. ( K ^ k ) ) )
124 11 14 18 3 4 123 geomcau 
 |-  ( ph -> G e. ( Cau ` D ) )
125 7 cmetcau 
 |-  ( ( D e. ( CMet ` X ) /\ G e. ( Cau ` D ) ) -> G e. dom ( ~~>t ` J ) )
126 1 124 125 syl2anc 
 |-  ( ph -> G e. dom ( ~~>t ` J ) )
127 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
128 7 methaus 
 |-  ( D e. ( *Met ` X ) -> J e. Haus )
129 11 127 128 3syl 
 |-  ( ph -> J e. Haus )
130 lmfun 
 |-  ( J e. Haus -> Fun ( ~~>t ` J ) )
131 funfvbrb 
 |-  ( Fun ( ~~>t ` J ) -> ( G e. dom ( ~~>t ` J ) <-> G ( ~~>t ` J ) ( ( ~~>t ` J ) ` G ) ) )
132 129 130 131 3syl 
 |-  ( ph -> ( G e. dom ( ~~>t ` J ) <-> G ( ~~>t ` J ) ( ( ~~>t ` J ) ` G ) ) )
133 126 132 mpbid 
 |-  ( ph -> G ( ~~>t ` J ) ( ( ~~>t ` J ) ` G ) )