Metamath Proof Explorer

Theorem dvferm1lem

Description: Lemma for dvferm . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses dvferm.a 
|- ( ph -> F : X --> RR )
dvferm.b 
|- ( ph -> X C_ RR )
dvferm.u 
|- ( ph -> U e. ( A (,) B ) )
dvferm.s 
|- ( ph -> ( A (,) B ) C_ X )
dvferm.d 
|- ( ph -> U e. dom ( RR _D F ) )
dvferm1.r 
|- ( ph -> A. y e. ( U (,) B ) ( F ` y ) <_ ( F ` U ) )
dvferm1.z 
|- ( ph -> 0 < ( ( RR _D F ) ` U ) )
dvferm1.t 
|- ( ph -> T e. RR+ )
dvferm1.l 
|- ( ph -> A. z e. ( X \ { U } ) ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) -> ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) ) )
dvferm1.x 
|- S = ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 )
Assertion dvferm1lem 
|- -. ph

Proof

Step Hyp Ref Expression
1 dvferm.a 
 |-  ( ph -> F : X --> RR )
2 dvferm.b 
 |-  ( ph -> X C_ RR )
3 dvferm.u 
 |-  ( ph -> U e. ( A (,) B ) )
4 dvferm.s 
 |-  ( ph -> ( A (,) B ) C_ X )
5 dvferm.d 
 |-  ( ph -> U e. dom ( RR _D F ) )
6 dvferm1.r 
 |-  ( ph -> A. y e. ( U (,) B ) ( F ` y ) <_ ( F ` U ) )
7 dvferm1.z 
 |-  ( ph -> 0 < ( ( RR _D F ) ` U ) )
8 dvferm1.t 
 |-  ( ph -> T e. RR+ )
9 dvferm1.l 
 |-  ( ph -> A. z e. ( X \ { U } ) ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) -> ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) ) )
10 dvferm1.x 
 |-  S = ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 )
11 dvfre 
 |-  ( ( F : X --> RR /\ X C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
12 1 2 11 syl2anc 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
13 12 5 ffvelrnd 
 |-  ( ph -> ( ( RR _D F ) ` U ) e. RR )
14 13 recnd 
 |-  ( ph -> ( ( RR _D F ) ` U ) e. CC )
15 14 subidd 
 |-  ( ph -> ( ( ( RR _D F ) ` U ) - ( ( RR _D F ) ` U ) ) = 0 )
16 ioossre 
 |-  ( A (,) B ) C_ RR
17 16 3 sseldi 
 |-  ( ph -> U e. RR )
18 eliooord 
 |-  ( U e. ( A (,) B ) -> ( A < U /\ U < B ) )
19 3 18 syl 
 |-  ( ph -> ( A < U /\ U < B ) )
20 19 simprd 
 |-  ( ph -> U < B )
21 17 8 ltaddrpd 
 |-  ( ph -> U < ( U + T ) )
22 breq2 
 |-  ( B = if ( B <_ ( U + T ) , B , ( U + T ) ) -> ( U < B <-> U < if ( B <_ ( U + T ) , B , ( U + T ) ) ) )
23 breq2 
 |-  ( ( U + T ) = if ( B <_ ( U + T ) , B , ( U + T ) ) -> ( U < ( U + T ) <-> U < if ( B <_ ( U + T ) , B , ( U + T ) ) ) )
24 22 23 ifboth 
 |-  ( ( U < B /\ U < ( U + T ) ) -> U < if ( B <_ ( U + T ) , B , ( U + T ) ) )
25 20 21 24 syl2anc 
 |-  ( ph -> U < if ( B <_ ( U + T ) , B , ( U + T ) ) )
26 ne0i 
 |-  ( U e. ( A (,) B ) -> ( A (,) B ) =/= (/) )
27 ndmioo 
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = (/) )
28 27 necon1ai 
 |-  ( ( A (,) B ) =/= (/) -> ( A e. RR* /\ B e. RR* ) )
29 3 26 28 3syl 
 |-  ( ph -> ( A e. RR* /\ B e. RR* ) )
30 29 simprd 
 |-  ( ph -> B e. RR* )
31 8 rpred 
 |-  ( ph -> T e. RR )
32 17 31 readdcld 
 |-  ( ph -> ( U + T ) e. RR )
33 32 rexrd 
 |-  ( ph -> ( U + T ) e. RR* )
34 30 33 ifcld 
 |-  ( ph -> if ( B <_ ( U + T ) , B , ( U + T ) ) e. RR* )
35 mnfxr 
 |-  -oo e. RR*
36 35 a1i 
 |-  ( ph -> -oo e. RR* )
37 17 rexrd 
 |-  ( ph -> U e. RR* )
38 17 mnfltd 
 |-  ( ph -> -oo < U )
39 36 37 30 38 20 xrlttrd 
 |-  ( ph -> -oo < B )
40 32 mnfltd 
 |-  ( ph -> -oo < ( U + T ) )
41 breq2 
 |-  ( B = if ( B <_ ( U + T ) , B , ( U + T ) ) -> ( -oo < B <-> -oo < if ( B <_ ( U + T ) , B , ( U + T ) ) ) )
42 breq2 
 |-  ( ( U + T ) = if ( B <_ ( U + T ) , B , ( U + T ) ) -> ( -oo < ( U + T ) <-> -oo < if ( B <_ ( U + T ) , B , ( U + T ) ) ) )
43 41 42 ifboth 
 |-  ( ( -oo < B /\ -oo < ( U + T ) ) -> -oo < if ( B <_ ( U + T ) , B , ( U + T ) ) )
44 39 40 43 syl2anc 
 |-  ( ph -> -oo < if ( B <_ ( U + T ) , B , ( U + T ) ) )
45 xrmin2 
 |-  ( ( B e. RR* /\ ( U + T ) e. RR* ) -> if ( B <_ ( U + T ) , B , ( U + T ) ) <_ ( U + T ) )
46 30 33 45 syl2anc 
 |-  ( ph -> if ( B <_ ( U + T ) , B , ( U + T ) ) <_ ( U + T ) )
47 xrre 
 |-  ( ( ( if ( B <_ ( U + T ) , B , ( U + T ) ) e. RR* /\ ( U + T ) e. RR ) /\ ( -oo < if ( B <_ ( U + T ) , B , ( U + T ) ) /\ if ( B <_ ( U + T ) , B , ( U + T ) ) <_ ( U + T ) ) ) -> if ( B <_ ( U + T ) , B , ( U + T ) ) e. RR )
48 34 32 44 46 47 syl22anc 
 |-  ( ph -> if ( B <_ ( U + T ) , B , ( U + T ) ) e. RR )
49 avglt1 
 |-  ( ( U e. RR /\ if ( B <_ ( U + T ) , B , ( U + T ) ) e. RR ) -> ( U < if ( B <_ ( U + T ) , B , ( U + T ) ) <-> U < ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 ) ) )
50 17 48 49 syl2anc 
 |-  ( ph -> ( U < if ( B <_ ( U + T ) , B , ( U + T ) ) <-> U < ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 ) ) )
51 25 50 mpbid 
 |-  ( ph -> U < ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 ) )
52 51 10 breqtrrdi 
 |-  ( ph -> U < S )
53 17 52 gtned 
 |-  ( ph -> S =/= U )
54 17 48 readdcld 
 |-  ( ph -> ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) e. RR )
55 54 rehalfcld 
 |-  ( ph -> ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 ) e. RR )
56 10 55 eqeltrid 
 |-  ( ph -> S e. RR )
57 17 56 52 ltled 
 |-  ( ph -> U <_ S )
58 17 56 57 abssubge0d 
 |-  ( ph -> ( abs ` ( S - U ) ) = ( S - U ) )
59 avglt2 
 |-  ( ( U e. RR /\ if ( B <_ ( U + T ) , B , ( U + T ) ) e. RR ) -> ( U < if ( B <_ ( U + T ) , B , ( U + T ) ) <-> ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 ) < if ( B <_ ( U + T ) , B , ( U + T ) ) ) )
60 17 48 59 syl2anc 
 |-  ( ph -> ( U < if ( B <_ ( U + T ) , B , ( U + T ) ) <-> ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 ) < if ( B <_ ( U + T ) , B , ( U + T ) ) ) )
61 25 60 mpbid 
 |-  ( ph -> ( ( U + if ( B <_ ( U + T ) , B , ( U + T ) ) ) / 2 ) < if ( B <_ ( U + T ) , B , ( U + T ) ) )
62 10 61 eqbrtrid 
 |-  ( ph -> S < if ( B <_ ( U + T ) , B , ( U + T ) ) )
63 56 48 32 62 46 ltletrd 
 |-  ( ph -> S < ( U + T ) )
64 56 17 31 ltsubadd2d 
 |-  ( ph -> ( ( S - U ) < T <-> S < ( U + T ) ) )
65 63 64 mpbird 
 |-  ( ph -> ( S - U ) < T )
66 58 65 eqbrtrd 
 |-  ( ph -> ( abs ` ( S - U ) ) < T )
67 neeq1 
 |-  ( z = S -> ( z =/= U <-> S =/= U ) )
68 fvoveq1 
 |-  ( z = S -> ( abs ` ( z - U ) ) = ( abs ` ( S - U ) ) )
69 68 breq1d 
 |-  ( z = S -> ( ( abs ` ( z - U ) ) < T <-> ( abs ` ( S - U ) ) < T ) )
70 67 69 anbi12d 
 |-  ( z = S -> ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) <-> ( S =/= U /\ ( abs ` ( S - U ) ) < T ) ) )
71 fveq2 
 |-  ( z = S -> ( F ` z ) = ( F ` S ) )
72 71 oveq1d 
 |-  ( z = S -> ( ( F ` z ) - ( F ` U ) ) = ( ( F ` S ) - ( F ` U ) ) )
73 oveq1 
 |-  ( z = S -> ( z - U ) = ( S - U ) )
74 72 73 oveq12d 
 |-  ( z = S -> ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) = ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) )
75 74 fvoveq1d 
 |-  ( z = S -> ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) = ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) )
76 75 breq1d 
 |-  ( z = S -> ( ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) <-> ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) ) )
77 70 76 imbi12d 
 |-  ( z = S -> ( ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) -> ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) ) <-> ( ( S =/= U /\ ( abs ` ( S - U ) ) < T ) -> ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) ) ) )
78 29 simpld 
 |-  ( ph -> A e. RR* )
79 19 simpld 
 |-  ( ph -> A < U )
80 78 37 79 xrltled 
 |-  ( ph -> A <_ U )
81 iooss1 
 |-  ( ( A e. RR* /\ A <_ U ) -> ( U (,) B ) C_ ( A (,) B ) )
82 78 80 81 syl2anc 
 |-  ( ph -> ( U (,) B ) C_ ( A (,) B ) )
83 82 4 sstrd 
 |-  ( ph -> ( U (,) B ) C_ X )
84 56 rexrd 
 |-  ( ph -> S e. RR* )
85 xrmin1 
 |-  ( ( B e. RR* /\ ( U + T ) e. RR* ) -> if ( B <_ ( U + T ) , B , ( U + T ) ) <_ B )
86 30 33 85 syl2anc 
 |-  ( ph -> if ( B <_ ( U + T ) , B , ( U + T ) ) <_ B )
87 84 34 30 62 86 xrltletrd 
 |-  ( ph -> S < B )
88 elioo2 
 |-  ( ( U e. RR* /\ B e. RR* ) -> ( S e. ( U (,) B ) <-> ( S e. RR /\ U < S /\ S < B ) ) )
89 37 30 88 syl2anc 
 |-  ( ph -> ( S e. ( U (,) B ) <-> ( S e. RR /\ U < S /\ S < B ) ) )
90 56 52 87 89 mpbir3and 
 |-  ( ph -> S e. ( U (,) B ) )
91 83 90 sseldd 
 |-  ( ph -> S e. X )
92 eldifsn 
 |-  ( S e. ( X \ { U } ) <-> ( S e. X /\ S =/= U ) )
93 91 53 92 sylanbrc 
 |-  ( ph -> S e. ( X \ { U } ) )
94 77 9 93 rspcdva 
 |-  ( ph -> ( ( S =/= U /\ ( abs ` ( S - U ) ) < T ) -> ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) ) )
95 53 66 94 mp2and 
 |-  ( ph -> ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) )
96 1 91 ffvelrnd 
 |-  ( ph -> ( F ` S ) e. RR )
97 4 3 sseldd 
 |-  ( ph -> U e. X )
98 1 97 ffvelrnd 
 |-  ( ph -> ( F ` U ) e. RR )
99 96 98 resubcld 
 |-  ( ph -> ( ( F ` S ) - ( F ` U ) ) e. RR )
100 56 17 resubcld 
 |-  ( ph -> ( S - U ) e. RR )
101 17 56 posdifd 
 |-  ( ph -> ( U < S <-> 0 < ( S - U ) ) )
102 52 101 mpbid 
 |-  ( ph -> 0 < ( S - U ) )
103 100 102 elrpd 
 |-  ( ph -> ( S - U ) e. RR+ )
104 99 103 rerpdivcld 
 |-  ( ph -> ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) e. RR )
105 104 13 13 absdifltd 
 |-  ( ph -> ( ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < ( ( RR _D F ) ` U ) <-> ( ( ( ( RR _D F ) ` U ) - ( ( RR _D F ) ` U ) ) < ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) /\ ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) < ( ( ( RR _D F ) ` U ) + ( ( RR _D F ) ` U ) ) ) ) )
106 95 105 mpbid 
 |-  ( ph -> ( ( ( ( RR _D F ) ` U ) - ( ( RR _D F ) ` U ) ) < ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) /\ ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) < ( ( ( RR _D F ) ` U ) + ( ( RR _D F ) ` U ) ) ) )
107 106 simpld 
 |-  ( ph -> ( ( ( RR _D F ) ` U ) - ( ( RR _D F ) ` U ) ) < ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) )
108 15 107 eqbrtrrd 
 |-  ( ph -> 0 < ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) )
109 gt0div 
 |-  ( ( ( ( F ` S ) - ( F ` U ) ) e. RR /\ ( S - U ) e. RR /\ 0 < ( S - U ) ) -> ( 0 < ( ( F ` S ) - ( F ` U ) ) <-> 0 < ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) ) )
110 99 100 102 109 syl3anc 
 |-  ( ph -> ( 0 < ( ( F ` S ) - ( F ` U ) ) <-> 0 < ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) ) )
111 108 110 mpbird 
 |-  ( ph -> 0 < ( ( F ` S ) - ( F ` U ) ) )
112 98 96 posdifd 
 |-  ( ph -> ( ( F ` U ) < ( F ` S ) <-> 0 < ( ( F ` S ) - ( F ` U ) ) ) )
113 111 112 mpbird 
 |-  ( ph -> ( F ` U ) < ( F ` S ) )
114 fveq2 
 |-  ( y = S -> ( F ` y ) = ( F ` S ) )
115 114 breq1d 
 |-  ( y = S -> ( ( F ` y ) <_ ( F ` U ) <-> ( F ` S ) <_ ( F ` U ) ) )
116 115 6 90 rspcdva 
 |-  ( ph -> ( F ` S ) <_ ( F ` U ) )
117 96 98 116 lensymd 
 |-  ( ph -> -. ( F ` U ) < ( F ` S ) )
118 113 117 pm2.65i 
 |-  -. ph