Metamath Proof Explorer

Theorem dvferm2lem

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 ) )
dvferm2.r 
|- ( ph -> A. y e. ( A (,) U ) ( F ` y ) <_ ( F ` U ) )
dvferm2.z 
|- ( ph -> ( ( RR _D F ) ` U ) < 0 )
dvferm2.t 
|- ( ph -> T e. RR+ )
dvferm2.l 
|- ( ph -> A. z e. ( X \ { U } ) ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) -> ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) ) )
dvferm2.x 
|- S = ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 )
Assertion dvferm2lem 
|- -. 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 dvferm2.r 
 |-  ( ph -> A. y e. ( A (,) U ) ( F ` y ) <_ ( F ` U ) )
7 dvferm2.z 
 |-  ( ph -> ( ( RR _D F ) ` U ) < 0 )
8 dvferm2.t 
 |-  ( ph -> T e. RR+ )
9 dvferm2.l 
 |-  ( ph -> A. z e. ( X \ { U } ) ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) -> ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) ) )
10 dvferm2.x 
 |-  S = ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 )
11 mnfxr 
 |-  -oo e. RR*
12 11 a1i 
 |-  ( ph -> -oo e. RR* )
13 ioossre 
 |-  ( A (,) B ) C_ RR
14 13 3 sseldi 
 |-  ( ph -> U e. RR )
15 8 rpred 
 |-  ( ph -> T e. RR )
16 14 15 resubcld 
 |-  ( ph -> ( U - T ) e. RR )
17 16 rexrd 
 |-  ( ph -> ( U - T ) e. RR* )
18 ne0i 
 |-  ( U e. ( A (,) B ) -> ( A (,) B ) =/= (/) )
19 ndmioo 
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = (/) )
20 19 necon1ai 
 |-  ( ( A (,) B ) =/= (/) -> ( A e. RR* /\ B e. RR* ) )
21 3 18 20 3syl 
 |-  ( ph -> ( A e. RR* /\ B e. RR* ) )
22 21 simpld 
 |-  ( ph -> A e. RR* )
23 17 22 ifcld 
 |-  ( ph -> if ( A <_ ( U - T ) , ( U - T ) , A ) e. RR* )
24 14 rexrd 
 |-  ( ph -> U e. RR* )
25 16 mnfltd 
 |-  ( ph -> -oo < ( U - T ) )
26 xrmax2 
 |-  ( ( A e. RR* /\ ( U - T ) e. RR* ) -> ( U - T ) <_ if ( A <_ ( U - T ) , ( U - T ) , A ) )
27 22 17 26 syl2anc 
 |-  ( ph -> ( U - T ) <_ if ( A <_ ( U - T ) , ( U - T ) , A ) )
28 12 17 23 25 27 xrltletrd 
 |-  ( ph -> -oo < if ( A <_ ( U - T ) , ( U - T ) , A ) )
29 14 8 ltsubrpd 
 |-  ( ph -> ( U - T ) < U )
30 eliooord 
 |-  ( U e. ( A (,) B ) -> ( A < U /\ U < B ) )
31 3 30 syl 
 |-  ( ph -> ( A < U /\ U < B ) )
32 31 simpld 
 |-  ( ph -> A < U )
33 breq1 
 |-  ( ( U - T ) = if ( A <_ ( U - T ) , ( U - T ) , A ) -> ( ( U - T ) < U <-> if ( A <_ ( U - T ) , ( U - T ) , A ) < U ) )
34 breq1 
 |-  ( A = if ( A <_ ( U - T ) , ( U - T ) , A ) -> ( A < U <-> if ( A <_ ( U - T ) , ( U - T ) , A ) < U ) )
35 33 34 ifboth 
 |-  ( ( ( U - T ) < U /\ A < U ) -> if ( A <_ ( U - T ) , ( U - T ) , A ) < U )
36 29 32 35 syl2anc 
 |-  ( ph -> if ( A <_ ( U - T ) , ( U - T ) , A ) < U )
37 xrre2 
 |-  ( ( ( -oo e. RR* /\ if ( A <_ ( U - T ) , ( U - T ) , A ) e. RR* /\ U e. RR* ) /\ ( -oo < if ( A <_ ( U - T ) , ( U - T ) , A ) /\ if ( A <_ ( U - T ) , ( U - T ) , A ) < U ) ) -> if ( A <_ ( U - T ) , ( U - T ) , A ) e. RR )
38 12 23 24 28 36 37 syl32anc 
 |-  ( ph -> if ( A <_ ( U - T ) , ( U - T ) , A ) e. RR )
39 38 14 readdcld 
 |-  ( ph -> ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) e. RR )
40 39 rehalfcld 
 |-  ( ph -> ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 ) e. RR )
41 10 40 eqeltrid 
 |-  ( ph -> S e. RR )
42 avglt2 
 |-  ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) e. RR /\ U e. RR ) -> ( if ( A <_ ( U - T ) , ( U - T ) , A ) < U <-> ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 ) < U ) )
43 38 14 42 syl2anc 
 |-  ( ph -> ( if ( A <_ ( U - T ) , ( U - T ) , A ) < U <-> ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 ) < U ) )
44 36 43 mpbid 
 |-  ( ph -> ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 ) < U )
45 10 44 eqbrtrid 
 |-  ( ph -> S < U )
46 41 45 ltned 
 |-  ( ph -> S =/= U )
47 41 14 45 ltled 
 |-  ( ph -> S <_ U )
48 41 14 47 abssuble0d 
 |-  ( ph -> ( abs ` ( S - U ) ) = ( U - S ) )
49 avglt1 
 |-  ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) e. RR /\ U e. RR ) -> ( if ( A <_ ( U - T ) , ( U - T ) , A ) < U <-> if ( A <_ ( U - T ) , ( U - T ) , A ) < ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 ) ) )
50 38 14 49 syl2anc 
 |-  ( ph -> ( if ( A <_ ( U - T ) , ( U - T ) , A ) < U <-> if ( A <_ ( U - T ) , ( U - T ) , A ) < ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 ) ) )
51 36 50 mpbid 
 |-  ( ph -> if ( A <_ ( U - T ) , ( U - T ) , A ) < ( ( if ( A <_ ( U - T ) , ( U - T ) , A ) + U ) / 2 ) )
52 51 10 breqtrrdi 
 |-  ( ph -> if ( A <_ ( U - T ) , ( U - T ) , A ) < S )
53 16 38 41 27 52 lelttrd 
 |-  ( ph -> ( U - T ) < S )
54 14 15 41 53 ltsub23d 
 |-  ( ph -> ( U - S ) < T )
55 48 54 eqbrtrd 
 |-  ( ph -> ( abs ` ( S - U ) ) < T )
56 neeq1 
 |-  ( z = S -> ( z =/= U <-> S =/= U ) )
57 fvoveq1 
 |-  ( z = S -> ( abs ` ( z - U ) ) = ( abs ` ( S - U ) ) )
58 57 breq1d 
 |-  ( z = S -> ( ( abs ` ( z - U ) ) < T <-> ( abs ` ( S - U ) ) < T ) )
59 56 58 anbi12d 
 |-  ( z = S -> ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) <-> ( S =/= U /\ ( abs ` ( S - U ) ) < T ) ) )
60 fveq2 
 |-  ( z = S -> ( F ` z ) = ( F ` S ) )
61 60 oveq1d 
 |-  ( z = S -> ( ( F ` z ) - ( F ` U ) ) = ( ( F ` S ) - ( F ` U ) ) )
62 oveq1 
 |-  ( z = S -> ( z - U ) = ( S - U ) )
63 61 62 oveq12d 
 |-  ( z = S -> ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) = ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) )
64 63 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 ) ) ) )
65 64 breq1d 
 |-  ( z = S -> ( ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) <-> ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) ) )
66 59 65 imbi12d 
 |-  ( z = S -> ( ( ( z =/= U /\ ( abs ` ( z - U ) ) < T ) -> ( abs ` ( ( ( ( F ` z ) - ( F ` U ) ) / ( z - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) ) <-> ( ( S =/= U /\ ( abs ` ( S - U ) ) < T ) -> ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) ) ) )
67 21 simprd 
 |-  ( ph -> B e. RR* )
68 31 simprd 
 |-  ( ph -> U < B )
69 24 67 68 xrltled 
 |-  ( ph -> U <_ B )
70 iooss2 
 |-  ( ( B e. RR* /\ U <_ B ) -> ( A (,) U ) C_ ( A (,) B ) )
71 67 69 70 syl2anc 
 |-  ( ph -> ( A (,) U ) C_ ( A (,) B ) )
72 71 4 sstrd 
 |-  ( ph -> ( A (,) U ) C_ X )
73 41 rexrd 
 |-  ( ph -> S e. RR* )
74 xrmax1 
 |-  ( ( A e. RR* /\ ( U - T ) e. RR* ) -> A <_ if ( A <_ ( U - T ) , ( U - T ) , A ) )
75 22 17 74 syl2anc 
 |-  ( ph -> A <_ if ( A <_ ( U - T ) , ( U - T ) , A ) )
76 22 23 73 75 52 xrlelttrd 
 |-  ( ph -> A < S )
77 elioo2 
 |-  ( ( A e. RR* /\ U e. RR* ) -> ( S e. ( A (,) U ) <-> ( S e. RR /\ A < S /\ S < U ) ) )
78 22 24 77 syl2anc 
 |-  ( ph -> ( S e. ( A (,) U ) <-> ( S e. RR /\ A < S /\ S < U ) ) )
79 41 76 45 78 mpbir3and 
 |-  ( ph -> S e. ( A (,) U ) )
80 72 79 sseldd 
 |-  ( ph -> S e. X )
81 eldifsn 
 |-  ( S e. ( X \ { U } ) <-> ( S e. X /\ S =/= U ) )
82 80 46 81 sylanbrc 
 |-  ( ph -> S e. ( X \ { U } ) )
83 66 9 82 rspcdva 
 |-  ( ph -> ( ( S =/= U /\ ( abs ` ( S - U ) ) < T ) -> ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) ) )
84 46 55 83 mp2and 
 |-  ( ph -> ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) )
85 1 80 ffvelrnd 
 |-  ( ph -> ( F ` S ) e. RR )
86 4 3 sseldd 
 |-  ( ph -> U e. X )
87 1 86 ffvelrnd 
 |-  ( ph -> ( F ` U ) e. RR )
88 85 87 resubcld 
 |-  ( ph -> ( ( F ` S ) - ( F ` U ) ) e. RR )
89 41 14 resubcld 
 |-  ( ph -> ( S - U ) e. RR )
90 41 recnd 
 |-  ( ph -> S e. CC )
91 14 recnd 
 |-  ( ph -> U e. CC )
92 90 91 46 subne0d 
 |-  ( ph -> ( S - U ) =/= 0 )
93 88 89 92 redivcld 
 |-  ( ph -> ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) e. RR )
94 dvfre 
 |-  ( ( F : X --> RR /\ X C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
95 1 2 94 syl2anc 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
96 95 5 ffvelrnd 
 |-  ( ph -> ( ( RR _D F ) ` U ) e. RR )
97 96 renegcld 
 |-  ( ph -> -u ( ( RR _D F ) ` U ) e. RR )
98 93 96 97 absdifltd 
 |-  ( ph -> ( ( abs ` ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) - ( ( RR _D F ) ` U ) ) ) < -u ( ( RR _D F ) ` U ) <-> ( ( ( ( RR _D F ) ` U ) - -u ( ( RR _D F ) ` U ) ) < ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) /\ ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) < ( ( ( RR _D F ) ` U ) + -u ( ( RR _D F ) ` U ) ) ) ) )
99 84 98 mpbid 
 |-  ( ph -> ( ( ( ( RR _D F ) ` U ) - -u ( ( RR _D F ) ` U ) ) < ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) /\ ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) < ( ( ( RR _D F ) ` U ) + -u ( ( RR _D F ) ` U ) ) ) )
100 99 simprd 
 |-  ( ph -> ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) < ( ( ( RR _D F ) ` U ) + -u ( ( RR _D F ) ` U ) ) )
101 96 recnd 
 |-  ( ph -> ( ( RR _D F ) ` U ) e. CC )
102 101 negidd 
 |-  ( ph -> ( ( ( RR _D F ) ` U ) + -u ( ( RR _D F ) ` U ) ) = 0 )
103 100 102 breqtrd 
 |-  ( ph -> ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) < 0 )
104 93 lt0neg1d 
 |-  ( ph -> ( ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) < 0 <-> 0 < -u ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) ) )
105 103 104 mpbid 
 |-  ( ph -> 0 < -u ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) )
106 88 recnd 
 |-  ( ph -> ( ( F ` S ) - ( F ` U ) ) e. CC )
107 89 recnd 
 |-  ( ph -> ( S - U ) e. CC )
108 106 107 92 divneg2d 
 |-  ( ph -> -u ( ( ( F ` S ) - ( F ` U ) ) / ( S - U ) ) = ( ( ( F ` S ) - ( F ` U ) ) / -u ( S - U ) ) )
109 105 108 breqtrd 
 |-  ( ph -> 0 < ( ( ( F ` S ) - ( F ` U ) ) / -u ( S - U ) ) )
110 89 renegcld 
 |-  ( ph -> -u ( S - U ) e. RR )
111 41 14 posdifd 
 |-  ( ph -> ( S < U <-> 0 < ( U - S ) ) )
112 45 111 mpbid 
 |-  ( ph -> 0 < ( U - S ) )
113 90 91 negsubdi2d 
 |-  ( ph -> -u ( S - U ) = ( U - S ) )
114 112 113 breqtrrd 
 |-  ( ph -> 0 < -u ( S - U ) )
115 gt0div 
 |-  ( ( ( ( F ` S ) - ( F ` U ) ) e. RR /\ -u ( S - U ) e. RR /\ 0 < -u ( S - U ) ) -> ( 0 < ( ( F ` S ) - ( F ` U ) ) <-> 0 < ( ( ( F ` S ) - ( F ` U ) ) / -u ( S - U ) ) ) )
116 88 110 114 115 syl3anc 
 |-  ( ph -> ( 0 < ( ( F ` S ) - ( F ` U ) ) <-> 0 < ( ( ( F ` S ) - ( F ` U ) ) / -u ( S - U ) ) ) )
117 109 116 mpbird 
 |-  ( ph -> 0 < ( ( F ` S ) - ( F ` U ) ) )
118 87 85 posdifd 
 |-  ( ph -> ( ( F ` U ) < ( F ` S ) <-> 0 < ( ( F ` S ) - ( F ` U ) ) ) )
119 117 118 mpbird 
 |-  ( ph -> ( F ` U ) < ( F ` S ) )
120 fveq2 
 |-  ( y = S -> ( F ` y ) = ( F ` S ) )
121 120 breq1d 
 |-  ( y = S -> ( ( F ` y ) <_ ( F ` U ) <-> ( F ` S ) <_ ( F ` U ) ) )
122 121 6 79 rspcdva 
 |-  ( ph -> ( F ` S ) <_ ( F ` U ) )
123 85 87 122 lensymd 
 |-  ( ph -> -. ( F ` U ) < ( F ` S ) )
124 119 123 pm2.65i 
 |-  -. ph