Metamath Proof Explorer

Theorem bfplem2

Description: Lemma for bfp . Using the point found in bfplem1 , we show that this convergent point is a fixed point of F . Since for any positive x , the sequence G is in B ( x / 2 , P ) for all k e. ( ZZ>=j ) (where P = ( ( ~>tJ )G ) ), we have D ( G ( j + 1 ) , F ( P ) ) <_ D ( G ( j ) , P ) < x / 2 and D ( G ( j + 1 ) , P ) < x / 2 , so F ( P ) is in every neighborhood of P and P is a fixed point of F . (Contributed by Jeff Madsen, 5-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 bfplem2 
|- ( ph -> E. z e. X ( F ` z ) = z )

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 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
13 7 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
14 11 12 13 3syl 
 |-  ( ph -> J e. ( TopOn ` X ) )
15 1 2 3 4 5 6 7 8 9 bfplem1 
 |-  ( ph -> G ( ~~>t ` J ) ( ( ~~>t ` J ) ` G ) )
16 lmcl 
 |-  ( ( J e. ( TopOn ` X ) /\ G ( ~~>t ` J ) ( ( ~~>t ` J ) ` G ) ) -> ( ( ~~>t ` J ) ` G ) e. X )
17 14 15 16 syl2anc 
 |-  ( ph -> ( ( ~~>t ` J ) ` G ) e. X )
18 11 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> D e. ( Met ` X ) )
19 18 12 syl 
 |-  ( ( ph /\ x e. RR+ ) -> D e. ( *Met ` X ) )
20 nnuz 
 |-  NN = ( ZZ>= ` 1 )
21 1zzd 
 |-  ( ( ph /\ x e. RR+ ) -> 1 e. ZZ )
22 eqidd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. NN ) -> ( G ` k ) = ( G ` k ) )
23 15 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> G ( ~~>t ` J ) ( ( ~~>t ` J ) ` G ) )
24 rphalfcl 
 |-  ( x e. RR+ -> ( x / 2 ) e. RR+ )
25 24 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
26 7 19 20 21 22 23 25 lmmcvg 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( G ` k ) e. X /\ ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) )
27 simpr 
 |-  ( ( ( G ` k ) e. X /\ ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) -> ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) )
28 27 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( G ` k ) e. X /\ ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) )
29 nnz 
 |-  ( j e. NN -> j e. ZZ )
30 29 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> j e. ZZ )
31 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
32 fveq2 
 |-  ( k = j -> ( G ` k ) = ( G ` j ) )
33 32 oveq1d 
 |-  ( k = j -> ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) = ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) )
34 33 breq1d 
 |-  ( k = j -> ( ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) <-> ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) )
35 34 rspcv 
 |-  ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) -> ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) )
36 30 31 35 3syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) -> ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) )
37 30 31 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> j e. ( ZZ>= ` j ) )
38 peano2uz 
 |-  ( j e. ( ZZ>= ` j ) -> ( j + 1 ) e. ( ZZ>= ` j ) )
39 fveq2 
 |-  ( k = ( j + 1 ) -> ( G ` k ) = ( G ` ( j + 1 ) ) )
40 39 oveq1d 
 |-  ( k = ( j + 1 ) -> ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) = ( ( G ` ( j + 1 ) ) D ( ( ~~>t ` J ) ` G ) ) )
41 40 breq1d 
 |-  ( k = ( j + 1 ) -> ( ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) <-> ( ( G ` ( j + 1 ) ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) )
42 41 rspcv 
 |-  ( ( j + 1 ) e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) -> ( ( G ` ( j + 1 ) ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) )
43 37 38 42 3syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) -> ( ( G ` ( j + 1 ) ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) )
44 1zzd 
 |-  ( ph -> 1 e. ZZ )
45 20 9 44 8 5 algrp1 
 |-  ( ( ph /\ j e. NN ) -> ( G ` ( j + 1 ) ) = ( F ` ( G ` j ) ) )
46 45 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( G ` ( j + 1 ) ) = ( F ` ( G ` j ) ) )
47 46 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( G ` ( j + 1 ) ) D ( ( ~~>t ` J ) ` G ) ) = ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) )
48 47 breq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( ( G ` ( j + 1 ) ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) <-> ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) )
49 43 48 sylibd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) -> ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) )
50 36 49 jcad 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) -> ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) /\ ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) ) )
51 11 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> D e. ( Met ` X ) )
52 20 9 44 8 5 algrf 
 |-  ( ph -> G : NN --> X )
53 52 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> G : NN --> X )
54 53 ffvelrnda 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( G ` j ) e. X )
55 17 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( ~~>t ` J ) ` G ) e. X )
56 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( G ` j ) e. X /\ ( ( ~~>t ` J ) ` G ) e. X ) -> ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) e. RR )
57 51 54 55 56 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) e. RR )
58 5 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> F : X --> X )
59 58 54 ffvelrnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( F ` ( G ` j ) ) e. X )
60 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` ( G ` j ) ) e. X /\ ( ( ~~>t ` J ) ` G ) e. X ) -> ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR )
61 51 59 55 60 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR )
62 rpre 
 |-  ( x e. RR+ -> x e. RR )
63 62 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> x e. RR )
64 lt2halves 
 |-  ( ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) e. RR /\ ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR /\ x e. RR ) -> ( ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) /\ ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) -> ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) < x ) )
65 57 61 63 64 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) /\ ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) -> ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) < x ) )
66 5 17 ffvelrnd 
 |-  ( ph -> ( F ` ( ( ~~>t ` J ) ` G ) ) e. X )
67 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` ( ( ~~>t ` J ) ` G ) ) e. X /\ ( ( ~~>t ` J ) ` G ) e. X ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR )
68 11 66 17 67 syl3anc 
 |-  ( ph -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR )
69 68 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR )
70 58 55 ffvelrnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( F ` ( ( ~~>t ` J ) ` G ) ) e. X )
71 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` ( G ` j ) ) e. X /\ ( F ` ( ( ~~>t ` J ) ` G ) ) e. X ) -> ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) e. RR )
72 51 59 70 71 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) e. RR )
73 72 61 readdcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) e. RR )
74 57 61 readdcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) e. RR )
75 mettri2 
 |-  ( ( D e. ( Met ` X ) /\ ( ( F ` ( G ` j ) ) e. X /\ ( F ` ( ( ~~>t ` J ) ` G ) ) e. X /\ ( ( ~~>t ` J ) ` G ) e. X ) ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ ( ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) )
76 51 59 70 55 75 syl13anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ ( ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) )
77 3 rpred 
 |-  ( ph -> K e. RR )
78 77 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> K e. RR )
79 78 57 remulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( K x. ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) ) e. RR )
80 54 55 jca 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( G ` j ) e. X /\ ( ( ~~>t ` J ) ` G ) e. X ) )
81 6 ralrimivva 
 |-  ( ph -> A. x e. X A. y e. X ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
82 81 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> A. x e. X A. y e. X ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )
83 fveq2 
 |-  ( x = ( G ` j ) -> ( F ` x ) = ( F ` ( G ` j ) ) )
84 83 oveq1d 
 |-  ( x = ( G ` j ) -> ( ( F ` x ) D ( F ` y ) ) = ( ( F ` ( G ` j ) ) D ( F ` y ) ) )
85 oveq1 
 |-  ( x = ( G ` j ) -> ( x D y ) = ( ( G ` j ) D y ) )
86 85 oveq2d 
 |-  ( x = ( G ` j ) -> ( K x. ( x D y ) ) = ( K x. ( ( G ` j ) D y ) ) )
87 84 86 breq12d 
 |-  ( x = ( G ` j ) -> ( ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) <-> ( ( F ` ( G ` j ) ) D ( F ` y ) ) <_ ( K x. ( ( G ` j ) D y ) ) ) )
88 fveq2 
 |-  ( y = ( ( ~~>t ` J ) ` G ) -> ( F ` y ) = ( F ` ( ( ~~>t ` J ) ` G ) ) )
89 88 oveq2d 
 |-  ( y = ( ( ~~>t ` J ) ` G ) -> ( ( F ` ( G ` j ) ) D ( F ` y ) ) = ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) )
90 oveq2 
 |-  ( y = ( ( ~~>t ` J ) ` G ) -> ( ( G ` j ) D y ) = ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) )
91 90 oveq2d 
 |-  ( y = ( ( ~~>t ` J ) ` G ) -> ( K x. ( ( G ` j ) D y ) ) = ( K x. ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) ) )
92 89 91 breq12d 
 |-  ( y = ( ( ~~>t ` J ) ` G ) -> ( ( ( F ` ( G ` j ) ) D ( F ` y ) ) <_ ( K x. ( ( G ` j ) D y ) ) <-> ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) <_ ( K x. ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) ) ) )
93 87 92 rspc2v 
 |-  ( ( ( G ` j ) e. X /\ ( ( ~~>t ` J ) ` G ) e. X ) -> ( A. x e. X A. y e. X ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) -> ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) <_ ( K x. ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) ) ) )
94 80 82 93 sylc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) <_ ( K x. ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) ) )
95 1red 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> 1 e. RR )
96 metge0 
 |-  ( ( D e. ( Met ` X ) /\ ( G ` j ) e. X /\ ( ( ~~>t ` J ) ` G ) e. X ) -> 0 <_ ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) )
97 51 54 55 96 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> 0 <_ ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) )
98 1re 
 |-  1 e. RR
99 ltle 
 |-  ( ( K e. RR /\ 1 e. RR ) -> ( K < 1 -> K <_ 1 ) )
100 77 98 99 sylancl 
 |-  ( ph -> ( K < 1 -> K <_ 1 ) )
101 4 100 mpd 
 |-  ( ph -> K <_ 1 )
102 101 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> K <_ 1 )
103 78 95 57 97 102 lemul1ad 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( K x. ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) ) <_ ( 1 x. ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) ) )
104 57 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) e. CC )
105 104 mulid2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( 1 x. ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) ) = ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) )
106 103 105 breqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( K x. ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) ) <_ ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) )
107 72 79 57 94 106 letrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) <_ ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) )
108 72 57 61 107 leadd1dd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( ( F ` ( G ` j ) ) D ( F ` ( ( ~~>t ` J ) ` G ) ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) <_ ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) )
109 69 73 74 76 108 letrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) )
110 lelttr 
 |-  ( ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR /\ ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) e. RR /\ x e. RR ) -> ( ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) /\ ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) < x ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) < x ) )
111 69 74 63 110 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) /\ ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) < x ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) < x ) )
112 109 111 mpand 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( ( ( ( G ` j ) D ( ( ~~>t ` J ) ` G ) ) + ( ( F ` ( G ` j ) ) D ( ( ~~>t ` J ) ` G ) ) ) < x -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) < x ) )
113 50 65 112 3syld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) < x ) )
114 28 113 syl5 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` k ) e. X /\ ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) < x ) )
115 114 rexlimdva 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( G ` k ) e. X /\ ( ( G ` k ) D ( ( ~~>t ` J ) ` G ) ) < ( x / 2 ) ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) < x ) )
116 26 115 mpd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) < x )
117 ltle 
 |-  ( ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR /\ x e. RR ) -> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) < x -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ x ) )
118 68 62 117 syl2an 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) < x -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ x ) )
119 116 118 mpd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ x )
120 62 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
121 120 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
122 121 addid2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( 0 + x ) = x )
123 119 122 breqtrrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ ( 0 + x ) )
124 123 ralrimiva 
 |-  ( ph -> A. x e. RR+ ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ ( 0 + x ) )
125 0re 
 |-  0 e. RR
126 alrple 
 |-  ( ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR /\ 0 e. RR ) -> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ 0 <-> A. x e. RR+ ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ ( 0 + x ) ) )
127 68 125 126 sylancl 
 |-  ( ph -> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ 0 <-> A. x e. RR+ ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ ( 0 + x ) ) )
128 124 127 mpbird 
 |-  ( ph -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ 0 )
129 metge0 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` ( ( ~~>t ` J ) ` G ) ) e. X /\ ( ( ~~>t ` J ) ` G ) e. X ) -> 0 <_ ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) )
130 11 66 17 129 syl3anc 
 |-  ( ph -> 0 <_ ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) )
131 letri3 
 |-  ( ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) e. RR /\ 0 e. RR ) -> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) = 0 <-> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ 0 /\ 0 <_ ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) ) ) )
132 68 125 131 sylancl 
 |-  ( ph -> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) = 0 <-> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) <_ 0 /\ 0 <_ ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) ) ) )
133 128 130 132 mpbir2and 
 |-  ( ph -> ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) = 0 )
134 meteq0 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` ( ( ~~>t ` J ) ` G ) ) e. X /\ ( ( ~~>t ` J ) ` G ) e. X ) -> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) = 0 <-> ( F ` ( ( ~~>t ` J ) ` G ) ) = ( ( ~~>t ` J ) ` G ) ) )
135 11 66 17 134 syl3anc 
 |-  ( ph -> ( ( ( F ` ( ( ~~>t ` J ) ` G ) ) D ( ( ~~>t ` J ) ` G ) ) = 0 <-> ( F ` ( ( ~~>t ` J ) ` G ) ) = ( ( ~~>t ` J ) ` G ) ) )
136 133 135 mpbid 
 |-  ( ph -> ( F ` ( ( ~~>t ` J ) ` G ) ) = ( ( ~~>t ` J ) ` G ) )
137 fveq2 
 |-  ( z = ( ( ~~>t ` J ) ` G ) -> ( F ` z ) = ( F ` ( ( ~~>t ` J ) ` G ) ) )
138 id 
 |-  ( z = ( ( ~~>t ` J ) ` G ) -> z = ( ( ~~>t ` J ) ` G ) )
139 137 138 eqeq12d 
 |-  ( z = ( ( ~~>t ` J ) ` G ) -> ( ( F ` z ) = z <-> ( F ` ( ( ~~>t ` J ) ` G ) ) = ( ( ~~>t ` J ) ` G ) ) )
140 139 rspcev 
 |-  ( ( ( ( ~~>t ` J ) ` G ) e. X /\ ( F ` ( ( ~~>t ` J ) ` G ) ) = ( ( ~~>t ` J ) ` G ) ) -> E. z e. X ( F ` z ) = z )
141 17 136 140 syl2anc 
 |-  ( ph -> E. z e. X ( F ` z ) = z )