This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvlip

Description: A function with derivative bounded by M is M-Lipschitz continuous. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses dvlip.a 
|- ( ph -> A e. RR )
dvlip.b 
|- ( ph -> B e. RR )
dvlip.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
dvlip.d 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
dvlip.m 
|- ( ph -> M e. RR )
dvlip.l 
|- ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )
Assertion dvlip 
|- ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) )

Proof

Step Hyp Ref Expression
1 dvlip.a 
 |-  ( ph -> A e. RR )
2 dvlip.b 
 |-  ( ph -> B e. RR )
3 dvlip.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
4 dvlip.d 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
5 dvlip.m 
 |-  ( ph -> M e. RR )
6 dvlip.l 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )
7 fveq2 
 |-  ( a = Y -> ( F ` a ) = ( F ` Y ) )
8 7 oveq2d 
 |-  ( a = Y -> ( ( F ` b ) - ( F ` a ) ) = ( ( F ` b ) - ( F ` Y ) ) )
9 8 fveq2d 
 |-  ( a = Y -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) = ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) )
10 oveq2 
 |-  ( a = Y -> ( b - a ) = ( b - Y ) )
11 10 fveq2d 
 |-  ( a = Y -> ( abs ` ( b - a ) ) = ( abs ` ( b - Y ) ) )
12 11 oveq2d 
 |-  ( a = Y -> ( M x. ( abs ` ( b - a ) ) ) = ( M x. ( abs ` ( b - Y ) ) ) )
13 9 12 breq12d 
 |-  ( a = Y -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) <-> ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( b - Y ) ) ) ) )
14 13 imbi2d 
 |-  ( a = Y -> ( ( ph -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) ) <-> ( ph -> ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( b - Y ) ) ) ) ) )
15 fveq2 
 |-  ( b = X -> ( F ` b ) = ( F ` X ) )
16 15 fvoveq1d 
 |-  ( b = X -> ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) = ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) )
17 fvoveq1 
 |-  ( b = X -> ( abs ` ( b - Y ) ) = ( abs ` ( X - Y ) ) )
18 17 oveq2d 
 |-  ( b = X -> ( M x. ( abs ` ( b - Y ) ) ) = ( M x. ( abs ` ( X - Y ) ) ) )
19 16 18 breq12d 
 |-  ( b = X -> ( ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( b - Y ) ) ) <-> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) ) )
20 19 imbi2d 
 |-  ( b = X -> ( ( ph -> ( abs ` ( ( F ` b ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( b - Y ) ) ) ) <-> ( ph -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) ) ) )
21 fveq2 
 |-  ( y = b -> ( F ` y ) = ( F ` b ) )
22 fveq2 
 |-  ( x = a -> ( F ` x ) = ( F ` a ) )
23 21 22 oveqan12d 
 |-  ( ( y = b /\ x = a ) -> ( ( F ` y ) - ( F ` x ) ) = ( ( F ` b ) - ( F ` a ) ) )
24 23 fveq2d 
 |-  ( ( y = b /\ x = a ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) = ( abs ` ( ( F ` b ) - ( F ` a ) ) ) )
25 oveq12 
 |-  ( ( y = b /\ x = a ) -> ( y - x ) = ( b - a ) )
26 25 fveq2d 
 |-  ( ( y = b /\ x = a ) -> ( abs ` ( y - x ) ) = ( abs ` ( b - a ) ) )
27 26 oveq2d 
 |-  ( ( y = b /\ x = a ) -> ( M x. ( abs ` ( y - x ) ) ) = ( M x. ( abs ` ( b - a ) ) ) )
28 24 27 breq12d 
 |-  ( ( y = b /\ x = a ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( M x. ( abs ` ( y - x ) ) ) <-> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) ) )
29 28 ancoms 
 |-  ( ( x = a /\ y = b ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( M x. ( abs ` ( y - x ) ) ) <-> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) ) )
30 fveq2 
 |-  ( y = a -> ( F ` y ) = ( F ` a ) )
31 fveq2 
 |-  ( x = b -> ( F ` x ) = ( F ` b ) )
32 30 31 oveqan12d 
 |-  ( ( y = a /\ x = b ) -> ( ( F ` y ) - ( F ` x ) ) = ( ( F ` a ) - ( F ` b ) ) )
33 32 fveq2d 
 |-  ( ( y = a /\ x = b ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) = ( abs ` ( ( F ` a ) - ( F ` b ) ) ) )
34 oveq12 
 |-  ( ( y = a /\ x = b ) -> ( y - x ) = ( a - b ) )
35 34 fveq2d 
 |-  ( ( y = a /\ x = b ) -> ( abs ` ( y - x ) ) = ( abs ` ( a - b ) ) )
36 35 oveq2d 
 |-  ( ( y = a /\ x = b ) -> ( M x. ( abs ` ( y - x ) ) ) = ( M x. ( abs ` ( a - b ) ) ) )
37 33 36 breq12d 
 |-  ( ( y = a /\ x = b ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( M x. ( abs ` ( y - x ) ) ) <-> ( abs ` ( ( F ` a ) - ( F ` b ) ) ) <_ ( M x. ( abs ` ( a - b ) ) ) ) )
38 37 ancoms 
 |-  ( ( x = b /\ y = a ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( M x. ( abs ` ( y - x ) ) ) <-> ( abs ` ( ( F ` a ) - ( F ` b ) ) ) <_ ( M x. ( abs ` ( a - b ) ) ) ) )
39 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
40 1 2 39 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
41 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
42 3 41 syl 
 |-  ( ph -> F : ( A [,] B ) --> CC )
43 ffvelcdm 
 |-  ( ( F : ( A [,] B ) --> CC /\ a e. ( A [,] B ) ) -> ( F ` a ) e. CC )
44 ffvelcdm 
 |-  ( ( F : ( A [,] B ) --> CC /\ b e. ( A [,] B ) ) -> ( F ` b ) e. CC )
45 43 44 anim12dan 
 |-  ( ( F : ( A [,] B ) --> CC /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( ( F ` a ) e. CC /\ ( F ` b ) e. CC ) )
46 42 45 sylan 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( ( F ` a ) e. CC /\ ( F ` b ) e. CC ) )
47 46 simprd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( F ` b ) e. CC )
48 46 simpld 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( F ` a ) e. CC )
49 47 48 abssubd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) = ( abs ` ( ( F ` a ) - ( F ` b ) ) ) )
50 ax-resscn 
 |-  RR C_ CC
51 40 50 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
52 51 sselda 
 |-  ( ( ph /\ b e. ( A [,] B ) ) -> b e. CC )
53 52 adantrl 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> b e. CC )
54 51 sselda 
 |-  ( ( ph /\ a e. ( A [,] B ) ) -> a e. CC )
55 54 adantrr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> a e. CC )
56 53 55 abssubd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( abs ` ( b - a ) ) = ( abs ` ( a - b ) ) )
57 56 oveq2d 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( M x. ( abs ` ( b - a ) ) ) = ( M x. ( abs ` ( a - b ) ) ) )
58 49 57 breq12d 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) <-> ( abs ` ( ( F ` a ) - ( F ` b ) ) ) <_ ( M x. ( abs ` ( a - b ) ) ) ) )
59 42 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> F : ( A [,] B ) --> CC )
60 simpr2 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. ( A [,] B ) )
61 59 60 ffvelcdmd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( F ` b ) e. CC )
62 simpr1 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. ( A [,] B ) )
63 59 62 ffvelcdmd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( F ` a ) e. CC )
64 61 63 subeq0ad 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( ( F ` b ) - ( F ` a ) ) = 0 <-> ( F ` b ) = ( F ` a ) ) )
65 64 biimpar 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) = ( F ` a ) ) -> ( ( F ` b ) - ( F ` a ) ) = 0 )
66 65 abs00bd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) = ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) = 0 )
67 40 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( A [,] B ) C_ RR )
68 67 62 sseldd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. RR )
69 68 rexrd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. RR* )
70 67 60 sseldd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. RR )
71 70 rexrd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. RR* )
72 ioon0 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( ( a (,) b ) =/= (/) <-> a < b ) )
73 69 71 72 syl2anc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( a (,) b ) =/= (/) <-> a < b ) )
74 5 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> M e. RR )
75 70 68 resubcld 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( b - a ) e. RR )
76 75 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> ( b - a ) e. RR )
77 1 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> A e. RR )
78 77 rexrd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> A e. RR* )
79 2 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> B e. RR )
80 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( a e. ( A [,] B ) <-> ( a e. RR /\ A <_ a /\ a <_ B ) ) )
81 77 79 80 syl2anc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a e. ( A [,] B ) <-> ( a e. RR /\ A <_ a /\ a <_ B ) ) )
82 62 81 mpbid 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a e. RR /\ A <_ a /\ a <_ B ) )
83 82 simp2d 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> A <_ a )
84 iooss1 
 |-  ( ( A e. RR* /\ A <_ a ) -> ( a (,) b ) C_ ( A (,) b ) )
85 78 83 84 syl2anc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a (,) b ) C_ ( A (,) b ) )
86 79 rexrd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> B e. RR* )
87 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( b e. ( A [,] B ) <-> ( b e. RR /\ A <_ b /\ b <_ B ) ) )
88 77 79 87 syl2anc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( b e. ( A [,] B ) <-> ( b e. RR /\ A <_ b /\ b <_ B ) ) )
89 60 88 mpbid 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( b e. RR /\ A <_ b /\ b <_ B ) )
90 89 simp3d 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b <_ B )
91 iooss2 
 |-  ( ( B e. RR* /\ b <_ B ) -> ( A (,) b ) C_ ( A (,) B ) )
92 86 90 91 syl2anc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( A (,) b ) C_ ( A (,) B ) )
93 85 92 sstrd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a (,) b ) C_ ( A (,) B ) )
94 ssn0 
 |-  ( ( ( a (,) b ) C_ ( A (,) B ) /\ ( a (,) b ) =/= (/) ) -> ( A (,) B ) =/= (/) )
95 93 94 sylan 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> ( A (,) B ) =/= (/) )
96 n0 
 |-  ( ( A (,) B ) =/= (/) <-> E. x x e. ( A (,) B ) )
97 0red 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 e. RR )
98 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
99 4 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> CC <-> ( RR _D F ) : ( A (,) B ) --> CC ) )
100 98 99 mpbii 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
101 100 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
102 101 abscld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) e. RR )
103 5 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> M e. RR )
104 101 absge0d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 <_ ( abs ` ( ( RR _D F ) ` x ) ) )
105 97 102 103 104 6 letrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 <_ M )
106 105 ex 
 |-  ( ph -> ( x e. ( A (,) B ) -> 0 <_ M ) )
107 106 exlimdv 
 |-  ( ph -> ( E. x x e. ( A (,) B ) -> 0 <_ M ) )
108 107 imp 
 |-  ( ( ph /\ E. x x e. ( A (,) B ) ) -> 0 <_ M )
109 96 108 sylan2b 
 |-  ( ( ph /\ ( A (,) B ) =/= (/) ) -> 0 <_ M )
110 109 adantlr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( A (,) B ) =/= (/) ) -> 0 <_ M )
111 95 110 syldan 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> 0 <_ M )
112 simpr3 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a <_ b )
113 70 68 subge0d 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( 0 <_ ( b - a ) <-> a <_ b ) )
114 112 113 mpbird 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> 0 <_ ( b - a ) )
115 114 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> 0 <_ ( b - a ) )
116 74 76 111 115 mulge0d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( a (,) b ) =/= (/) ) -> 0 <_ ( M x. ( b - a ) ) )
117 116 ex 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( a (,) b ) =/= (/) -> 0 <_ ( M x. ( b - a ) ) ) )
118 73 117 sylbird 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a < b -> 0 <_ ( M x. ( b - a ) ) ) )
119 70 recnd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. CC )
120 68 recnd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. CC )
121 119 120 subeq0ad 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( b - a ) = 0 <-> b = a ) )
122 equcom 
 |-  ( b = a <-> a = b )
123 121 122 bitrdi 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( b - a ) = 0 <-> a = b ) )
124 0re 
 |-  0 e. RR
125 5 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> M e. RR )
126 125 recnd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> M e. CC )
127 126 mul01d 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( M x. 0 ) = 0 )
128 127 eqcomd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> 0 = ( M x. 0 ) )
129 eqle 
 |-  ( ( 0 e. RR /\ 0 = ( M x. 0 ) ) -> 0 <_ ( M x. 0 ) )
130 124 128 129 sylancr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> 0 <_ ( M x. 0 ) )
131 oveq2 
 |-  ( ( b - a ) = 0 -> ( M x. ( b - a ) ) = ( M x. 0 ) )
132 131 breq2d 
 |-  ( ( b - a ) = 0 -> ( 0 <_ ( M x. ( b - a ) ) <-> 0 <_ ( M x. 0 ) ) )
133 130 132 syl5ibrcom 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( b - a ) = 0 -> 0 <_ ( M x. ( b - a ) ) ) )
134 123 133 sylbird 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a = b -> 0 <_ ( M x. ( b - a ) ) ) )
135 68 70 leloed 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a <_ b <-> ( a < b \/ a = b ) ) )
136 112 135 mpbid 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a < b \/ a = b ) )
137 118 134 136 mpjaod 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> 0 <_ ( M x. ( b - a ) ) )
138 137 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) = ( F ` a ) ) -> 0 <_ ( M x. ( b - a ) ) )
139 66 138 eqbrtrd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) = ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) )
140 61 63 subcld 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( F ` b ) - ( F ` a ) ) e. CC )
141 140 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( F ` b ) - ( F ` a ) ) e. CC )
142 141 abscld 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) e. RR )
143 142 recnd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) e. CC )
144 75 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( b - a ) e. RR )
145 144 recnd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( b - a ) e. CC )
146 136 ord 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( -. a < b -> a = b ) )
147 fveq2 
 |-  ( a = b -> ( F ` a ) = ( F ` b ) )
148 147 eqcomd 
 |-  ( a = b -> ( F ` b ) = ( F ` a ) )
149 146 148 syl6 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( -. a < b -> ( F ` b ) = ( F ` a ) ) )
150 149 necon1ad 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( F ` b ) =/= ( F ` a ) -> a < b ) )
151 150 imp 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> a < b )
152 68 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> a e. RR )
153 70 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> b e. RR )
154 152 153 posdifd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a < b <-> 0 < ( b - a ) ) )
155 151 154 mpbid 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> 0 < ( b - a ) )
156 155 gt0ne0d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( b - a ) =/= 0 )
157 143 145 156 divrec2d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) / ( b - a ) ) = ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) )
158 iccss2 
 |-  ( ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) -> ( a [,] b ) C_ ( A [,] B ) )
159 62 60 158 syl2anc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( a [,] b ) C_ ( A [,] B ) )
160 159 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a [,] b ) C_ ( A [,] B ) )
161 160 sselda 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> y e. ( A [,] B ) )
162 42 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> F : ( A [,] B ) --> CC )
163 162 ffvelcdmda 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( A [,] B ) ) -> ( F ` y ) e. CC )
164 161 163 syldan 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( F ` y ) e. CC )
165 140 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( ( F ` b ) - ( F ` a ) ) e. CC )
166 64 necon3bid 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( ( F ` b ) - ( F ` a ) ) =/= 0 <-> ( F ` b ) =/= ( F ` a ) ) )
167 166 biimpar 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( F ` b ) - ( F ` a ) ) =/= 0 )
168 167 adantr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( ( F ` b ) - ( F ` a ) ) =/= 0 )
169 164 165 168 divcld 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
170 162 160 feqresmpt 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F |` ( a [,] b ) ) = ( y e. ( a [,] b ) |-> ( F ` y ) ) )
171 eqidd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) = ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) )
172 oveq1 
 |-  ( x = ( F ` y ) -> ( x / ( ( F ` b ) - ( F ` a ) ) ) = ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) )
173 164 170 171 172 fmptco 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) o. ( F |` ( a [,] b ) ) ) = ( y e. ( a [,] b ) |-> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
174 ref 
 |-  Re : CC --> RR
175 174 a1i 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> Re : CC --> RR )
176 175 feqmptd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> Re = ( x e. CC |-> ( Re ` x ) ) )
177 fveq2 
 |-  ( x = ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) -> ( Re ` x ) = ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
178 169 173 176 177 fmptco 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re o. ( ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) o. ( F |` ( a [,] b ) ) ) ) = ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
179 3 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> F e. ( ( A [,] B ) -cn-> CC ) )
180 rescncf 
 |-  ( ( a [,] b ) C_ ( A [,] B ) -> ( F e. ( ( A [,] B ) -cn-> CC ) -> ( F |` ( a [,] b ) ) e. ( ( a [,] b ) -cn-> CC ) ) )
181 159 179 180 sylc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( F |` ( a [,] b ) ) e. ( ( a [,] b ) -cn-> CC ) )
182 181 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F |` ( a [,] b ) ) e. ( ( a [,] b ) -cn-> CC ) )
183 eqid 
 |-  ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) = ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) )
184 183 divccncf 
 |-  ( ( ( ( F ` b ) - ( F ` a ) ) e. CC /\ ( ( F ` b ) - ( F ` a ) ) =/= 0 ) -> ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) e. ( CC -cn-> CC ) )
185 141 167 184 syl2anc 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) e. ( CC -cn-> CC ) )
186 182 185 cncfco 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) o. ( F |` ( a [,] b ) ) ) e. ( ( a [,] b ) -cn-> CC ) )
187 recncf 
 |-  Re e. ( CC -cn-> RR )
188 187 a1i 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> Re e. ( CC -cn-> RR ) )
189 186 188 cncfco 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re o. ( ( x e. CC |-> ( x / ( ( F ` b ) - ( F ` a ) ) ) ) o. ( F |` ( a [,] b ) ) ) ) e. ( ( a [,] b ) -cn-> RR ) )
190 178 189 eqeltrrd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) e. ( ( a [,] b ) -cn-> RR ) )
191 50 a1i 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> RR C_ CC )
192 iccssre 
 |-  ( ( a e. RR /\ b e. RR ) -> ( a [,] b ) C_ RR )
193 152 153 192 syl2anc 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a [,] b ) C_ RR )
194 169 recld 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. RR )
195 194 recnd 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a [,] b ) ) -> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. CC )
196 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
197 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
198 iccntr 
 |-  ( ( a e. RR /\ b e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( a [,] b ) ) = ( a (,) b ) )
199 68 70 198 syl2anc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( a [,] b ) ) = ( a (,) b ) )
200 199 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( a [,] b ) ) = ( a (,) b ) )
201 191 193 195 196 197 200 dvmptntr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = ( RR _D ( y e. ( a (,) b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) )
202 ioossicc 
 |-  ( a (,) b ) C_ ( a [,] b )
203 202 sseli 
 |-  ( y e. ( a (,) b ) -> y e. ( a [,] b ) )
204 203 169 sylan2 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
205 ovexd 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) e. _V )
206 reelprrecn 
 |-  RR e. { RR , CC }
207 206 a1i 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> RR e. { RR , CC } )
208 203 164 sylan2 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> ( F ` y ) e. CC )
209 93 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a (,) b ) C_ ( A (,) B ) )
210 209 sselda 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> y e. ( A (,) B ) )
211 100 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D F ) : ( A (,) B ) --> CC )
212 211 ffvelcdmda 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( A (,) B ) ) -> ( ( RR _D F ) ` y ) e. CC )
213 210 212 syldan 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ y e. ( a (,) b ) ) -> ( ( RR _D F ) ` y ) e. CC )
214 40 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( A [,] B ) C_ RR )
215 ioossre 
 |-  ( a (,) b ) C_ RR
216 215 a1i 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a (,) b ) C_ RR )
217 197 196 dvres 
 |-  ( ( ( RR C_ CC /\ F : ( A [,] B ) --> CC ) /\ ( ( A [,] B ) C_ RR /\ ( a (,) b ) C_ RR ) ) -> ( RR _D ( F |` ( a (,) b ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) ) )
218 191 162 214 216 217 syl22anc 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( F |` ( a (,) b ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) ) )
219 retop 
 |-  ( topGen ` ran (,) ) e. Top
220 iooretop 
 |-  ( a (,) b ) e. ( topGen ` ran (,) )
221 isopn3i 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( a (,) b ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) = ( a (,) b ) )
222 219 220 221 mp2an 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) = ( a (,) b )
223 222 reseq2i 
 |-  ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( a (,) b ) ) ) = ( ( RR _D F ) |` ( a (,) b ) )
224 218 223 eqtrdi 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( F |` ( a (,) b ) ) ) = ( ( RR _D F ) |` ( a (,) b ) ) )
225 202 160 sstrid 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( a (,) b ) C_ ( A [,] B ) )
226 162 225 feqresmpt 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F |` ( a (,) b ) ) = ( y e. ( a (,) b ) |-> ( F ` y ) ) )
227 226 oveq2d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( F |` ( a (,) b ) ) ) = ( RR _D ( y e. ( a (,) b ) |-> ( F ` y ) ) ) )
228 100 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( RR _D F ) : ( A (,) B ) --> CC )
229 228 93 fssresd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( RR _D F ) |` ( a (,) b ) ) : ( a (,) b ) --> CC )
230 229 feqmptd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( ( RR _D F ) |` ( a (,) b ) ) = ( y e. ( a (,) b ) |-> ( ( ( RR _D F ) |` ( a (,) b ) ) ` y ) ) )
231 230 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( RR _D F ) |` ( a (,) b ) ) = ( y e. ( a (,) b ) |-> ( ( ( RR _D F ) |` ( a (,) b ) ) ` y ) ) )
232 fvres 
 |-  ( y e. ( a (,) b ) -> ( ( ( RR _D F ) |` ( a (,) b ) ) ` y ) = ( ( RR _D F ) ` y ) )
233 232 mpteq2ia 
 |-  ( y e. ( a (,) b ) |-> ( ( ( RR _D F ) |` ( a (,) b ) ) ` y ) ) = ( y e. ( a (,) b ) |-> ( ( RR _D F ) ` y ) )
234 231 233 eqtrdi 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( RR _D F ) |` ( a (,) b ) ) = ( y e. ( a (,) b ) |-> ( ( RR _D F ) ` y ) ) )
235 224 227 234 3eqtr3d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a (,) b ) |-> ( F ` y ) ) ) = ( y e. ( a (,) b ) |-> ( ( RR _D F ) ` y ) ) )
236 207 208 213 235 141 167 dvmptdivc 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a (,) b ) |-> ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( y e. ( a (,) b ) |-> ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
237 204 205 236 dvmptre 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a (,) b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
238 201 237 eqtrd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
239 238 dmeqd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> dom ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = dom ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
240 dmmptg 
 |-  ( A. y e. ( a (,) b ) ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V -> dom ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( a (,) b ) )
241 fvex 
 |-  ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V
242 241 a1i 
 |-  ( y e. ( a (,) b ) -> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V )
243 240 242 mprg 
 |-  dom ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( a (,) b )
244 239 243 eqtrdi 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> dom ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) = ( a (,) b ) )
245 152 153 151 190 244 mvth 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> E. x e. ( a (,) b ) ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) / ( b - a ) ) )
246 238 fveq1d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` x ) )
247 fveq2 
 |-  ( y = x -> ( ( RR _D F ) ` y ) = ( ( RR _D F ) ` x ) )
248 247 fvoveq1d 
 |-  ( y = x -> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
249 eqid 
 |-  ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
250 fvex 
 |-  ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V
251 248 249 250 fvmpt 
 |-  ( x e. ( a (,) b ) -> ( ( y e. ( a (,) b ) |-> ( Re ` ( ( ( RR _D F ) ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` x ) = ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
252 246 251 sylan9eq 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
253 ubicc2 
 |-  ( ( a e. RR* /\ b e. RR* /\ a <_ b ) -> b e. ( a [,] b ) )
254 69 71 112 253 syl3anc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> b e. ( a [,] b ) )
255 254 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> b e. ( a [,] b ) )
256 21 fvoveq1d 
 |-  ( y = b -> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
257 eqid 
 |-  ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
258 fvex 
 |-  ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V
259 256 257 258 fvmpt 
 |-  ( b e. ( a [,] b ) -> ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) = ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
260 255 259 syl 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) = ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
261 lbicc2 
 |-  ( ( a e. RR* /\ b e. RR* /\ a <_ b ) -> a e. ( a [,] b ) )
262 69 71 112 261 syl3anc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> a e. ( a [,] b ) )
263 262 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> a e. ( a [,] b ) )
264 30 fvoveq1d 
 |-  ( y = a -> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
265 fvex 
 |-  ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. _V
266 264 257 265 fvmpt 
 |-  ( a e. ( a [,] b ) -> ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) = ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
267 263 266 syl 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) = ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
268 260 267 oveq12d 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) = ( ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) - ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
269 61 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F ` b ) e. CC )
270 269 141 167 divcld 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
271 63 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( F ` a ) e. CC )
272 271 141 167 divcld 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
273 270 272 resubd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re ` ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) - ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) )
274 269 271 141 167 divsubdird 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( ( F ` b ) - ( F ` a ) ) / ( ( F ` b ) - ( F ` a ) ) ) = ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
275 141 167 dividd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( ( F ` b ) - ( F ` a ) ) / ( ( F ` b ) - ( F ` a ) ) ) = 1 )
276 274 275 eqtr3d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) = 1 )
277 276 fveq2d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re ` ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = ( Re ` 1 ) )
278 re1 
 |-  ( Re ` 1 ) = 1
279 277 278 eqtrdi 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( Re ` ( ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) - ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = 1 )
280 273 279 eqtr3d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) - ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = 1 )
281 280 adantr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( F ` b ) / ( ( F ` b ) - ( F ` a ) ) ) ) - ( Re ` ( ( F ` a ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) = 1 )
282 268 281 eqtrd 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) = 1 )
283 282 oveq1d 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) / ( b - a ) ) = ( 1 / ( b - a ) ) )
284 252 283 eqeq12d 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) / ( b - a ) ) <-> ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) ) )
285 284 rexbidva 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( E. x e. ( a (,) b ) ( ( RR _D ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ) ` x ) = ( ( ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` b ) - ( ( y e. ( a [,] b ) |-> ( Re ` ( ( F ` y ) / ( ( F ` b ) - ( F ` a ) ) ) ) ) ` a ) ) / ( b - a ) ) <-> E. x e. ( a (,) b ) ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) ) )
286 245 285 mpbid 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> E. x e. ( a (,) b ) ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) )
287 209 sselda 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> x e. ( A (,) B ) )
288 211 ffvelcdmda 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
289 287 288 syldan 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( RR _D F ) ` x ) e. CC )
290 140 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( F ` b ) - ( F ` a ) ) e. CC )
291 167 adantr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( F ` b ) - ( F ` a ) ) =/= 0 )
292 289 290 291 divcld 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) e. CC )
293 292 recld 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. RR )
294 142 adantr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) e. RR )
295 293 294 remulcld 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) e. RR )
296 289 abscld 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) e. RR )
297 125 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> M e. RR )
298 292 abscld 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) e. RR )
299 141 absge0d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> 0 <_ ( abs ` ( ( F ` b ) - ( F ` a ) ) ) )
300 299 adantr 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> 0 <_ ( abs ` ( ( F ` b ) - ( F ` a ) ) ) )
301 292 releabsd 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) <_ ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) )
302 293 298 294 300 301 lemul1ad 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ ( ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) )
303 292 290 absmuld 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) x. ( ( F ` b ) - ( F ` a ) ) ) ) = ( ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) )
304 289 290 291 divcan1d 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) x. ( ( F ` b ) - ( F ` a ) ) ) = ( ( RR _D F ) ` x ) )
305 304 fveq2d 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) x. ( ( F ` b ) - ( F ` a ) ) ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
306 303 305 eqtr3d 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( abs ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
307 302 306 breqtrd 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ ( abs ` ( ( RR _D F ) ` x ) ) )
308 6 ad4ant14 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )
309 287 308 syldan 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) <_ M )
310 295 296 297 307 309 letrd 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M )
311 oveq1 
 |-  ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) = ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) )
312 311 breq1d 
 |-  ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) -> ( ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M <-> ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M ) )
313 310 312 syl5ibcom 
 |-  ( ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) /\ x e. ( a (,) b ) ) -> ( ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) -> ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M ) )
314 313 rexlimdva 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( E. x e. ( a (,) b ) ( Re ` ( ( ( RR _D F ) ` x ) / ( ( F ` b ) - ( F ` a ) ) ) ) = ( 1 / ( b - a ) ) -> ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M ) )
315 286 314 mpd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( 1 / ( b - a ) ) x. ( abs ` ( ( F ` b ) - ( F ` a ) ) ) ) <_ M )
316 157 315 eqbrtrd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) / ( b - a ) ) <_ M )
317 5 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> M e. RR )
318 ledivmul2 
 |-  ( ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) e. RR /\ M e. RR /\ ( ( b - a ) e. RR /\ 0 < ( b - a ) ) ) -> ( ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) / ( b - a ) ) <_ M <-> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) ) )
319 142 317 144 155 318 syl112anc 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) / ( b - a ) ) <_ M <-> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) ) )
320 316 319 mpbid 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) /\ ( F ` b ) =/= ( F ` a ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) )
321 139 320 pm2.61dane 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( b - a ) ) )
322 68 70 112 abssubge0d 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( abs ` ( b - a ) ) = ( b - a ) )
323 322 oveq2d 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( M x. ( abs ` ( b - a ) ) ) = ( M x. ( b - a ) ) )
324 321 323 breqtrrd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) /\ a <_ b ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) )
325 29 38 40 58 324 wlogle 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) )
326 325 expcom 
 |-  ( ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) -> ( ph -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( M x. ( abs ` ( b - a ) ) ) ) )
327 14 20 326 vtocl2ga 
 |-  ( ( Y e. ( A [,] B ) /\ X e. ( A [,] B ) ) -> ( ph -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) ) )
328 327 ancoms 
 |-  ( ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) -> ( ph -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) ) )
329 328 impcom 
 |-  ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` X ) - ( F ` Y ) ) ) <_ ( M x. ( abs ` ( X - Y ) ) ) )