Metamath Proof Explorer

Theorem dvgt0lem1

Description: Lemma for dvgt0 and dvlt0 . (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses dvgt0.a 
|- ( ph -> A e. RR )
dvgt0.b 
|- ( ph -> B e. RR )
dvgt0.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
dvgt0lem.d 
|- ( ph -> ( RR _D F ) : ( A (,) B ) --> S )
Assertion dvgt0lem1 
|- ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. S )

Proof

Step Hyp Ref Expression
1 dvgt0.a 
 |-  ( ph -> A e. RR )
2 dvgt0.b 
 |-  ( ph -> B e. RR )
3 dvgt0.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
4 dvgt0lem.d 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> S )
5 iccssxr 
 |-  ( A [,] B ) C_ RR*
6 simplrl 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> X e. ( A [,] B ) )
7 5 6 sselid 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> X e. RR* )
8 simplrr 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> Y e. ( A [,] B ) )
9 5 8 sselid 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> Y e. RR* )
10 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
11 1 2 10 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
12 11 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( A [,] B ) C_ RR )
13 12 6 sseldd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> X e. RR )
14 12 8 sseldd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> Y e. RR )
15 simpr 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> X < Y )
16 13 14 15 ltled 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> X <_ Y )
17 ubicc2 
 |-  ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> Y e. ( X [,] Y ) )
18 7 9 16 17 syl3anc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> Y e. ( X [,] Y ) )
19 18 fvresd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( F |` ( X [,] Y ) ) ` Y ) = ( F ` Y ) )
20 lbicc2 
 |-  ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> X e. ( X [,] Y ) )
21 7 9 16 20 syl3anc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> X e. ( X [,] Y ) )
22 21 fvresd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( F |` ( X [,] Y ) ) ` X ) = ( F ` X ) )
23 19 22 oveq12d 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) = ( ( F ` Y ) - ( F ` X ) ) )
24 23 oveq1d 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) / ( Y - X ) ) = ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) )
25 iccss2 
 |-  ( ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) -> ( X [,] Y ) C_ ( A [,] B ) )
26 25 ad2antlr 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( X [,] Y ) C_ ( A [,] B ) )
27 3 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> F e. ( ( A [,] B ) -cn-> RR ) )
28 rescncf 
 |-  ( ( X [,] Y ) C_ ( A [,] B ) -> ( F e. ( ( A [,] B ) -cn-> RR ) -> ( F |` ( X [,] Y ) ) e. ( ( X [,] Y ) -cn-> RR ) ) )
29 26 27 28 sylc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( F |` ( X [,] Y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
30 4 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( RR _D F ) : ( A (,) B ) --> S )
31 1 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> A e. RR )
32 31 rexrd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> A e. RR* )
33 2 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> B e. RR )
34 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( X e. ( A [,] B ) <-> ( X e. RR /\ A <_ X /\ X <_ B ) ) )
35 31 33 34 syl2anc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( X e. ( A [,] B ) <-> ( X e. RR /\ A <_ X /\ X <_ B ) ) )
36 6 35 mpbid 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( X e. RR /\ A <_ X /\ X <_ B ) )
37 36 simp2d 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> A <_ X )
38 iooss1 
 |-  ( ( A e. RR* /\ A <_ X ) -> ( X (,) Y ) C_ ( A (,) Y ) )
39 32 37 38 syl2anc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( X (,) Y ) C_ ( A (,) Y ) )
40 33 rexrd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> B e. RR* )
41 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( Y e. ( A [,] B ) <-> ( Y e. RR /\ A <_ Y /\ Y <_ B ) ) )
42 31 33 41 syl2anc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( Y e. ( A [,] B ) <-> ( Y e. RR /\ A <_ Y /\ Y <_ B ) ) )
43 8 42 mpbid 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( Y e. RR /\ A <_ Y /\ Y <_ B ) )
44 43 simp3d 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> Y <_ B )
45 iooss2 
 |-  ( ( B e. RR* /\ Y <_ B ) -> ( A (,) Y ) C_ ( A (,) B ) )
46 40 44 45 syl2anc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( A (,) Y ) C_ ( A (,) B ) )
47 39 46 sstrd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( X (,) Y ) C_ ( A (,) B ) )
48 30 47 fssresd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( RR _D F ) |` ( X (,) Y ) ) : ( X (,) Y ) --> S )
49 ax-resscn 
 |-  RR C_ CC
50 49 a1i 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> RR C_ CC )
51 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
52 3 51 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
53 52 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> F : ( A [,] B ) --> RR )
54 fss 
 |-  ( ( F : ( A [,] B ) --> RR /\ RR C_ CC ) -> F : ( A [,] B ) --> CC )
55 53 49 54 sylancl 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> F : ( A [,] B ) --> CC )
56 iccssre 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( X [,] Y ) C_ RR )
57 13 14 56 syl2anc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( X [,] Y ) C_ RR )
58 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
59 58 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
60 58 59 dvres 
 |-  ( ( ( RR C_ CC /\ F : ( A [,] B ) --> CC ) /\ ( ( A [,] B ) C_ RR /\ ( X [,] Y ) C_ RR ) ) -> ( RR _D ( F |` ( X [,] Y ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( X [,] Y ) ) ) )
61 50 55 12 57 60 syl22anc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( RR _D ( F |` ( X [,] Y ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( X [,] Y ) ) ) )
62 iccntr 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( X [,] Y ) ) = ( X (,) Y ) )
63 13 14 62 syl2anc 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( X [,] Y ) ) = ( X (,) Y ) )
64 63 reseq2d 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( X [,] Y ) ) ) = ( ( RR _D F ) |` ( X (,) Y ) ) )
65 61 64 eqtrd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( RR _D ( F |` ( X [,] Y ) ) ) = ( ( RR _D F ) |` ( X (,) Y ) ) )
66 65 feq1d 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( RR _D ( F |` ( X [,] Y ) ) ) : ( X (,) Y ) --> S <-> ( ( RR _D F ) |` ( X (,) Y ) ) : ( X (,) Y ) --> S ) )
67 48 66 mpbird 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( RR _D ( F |` ( X [,] Y ) ) ) : ( X (,) Y ) --> S )
68 67 fdmd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> dom ( RR _D ( F |` ( X [,] Y ) ) ) = ( X (,) Y ) )
69 13 14 15 29 68 mvth 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> E. z e. ( X (,) Y ) ( ( RR _D ( F |` ( X [,] Y ) ) ) ` z ) = ( ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) / ( Y - X ) ) )
70 67 ffvelrnda 
 |-  ( ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) /\ z e. ( X (,) Y ) ) -> ( ( RR _D ( F |` ( X [,] Y ) ) ) ` z ) e. S )
71 eleq1 
 |-  ( ( ( RR _D ( F |` ( X [,] Y ) ) ) ` z ) = ( ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) / ( Y - X ) ) -> ( ( ( RR _D ( F |` ( X [,] Y ) ) ) ` z ) e. S <-> ( ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) / ( Y - X ) ) e. S ) )
72 70 71 syl5ibcom 
 |-  ( ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) /\ z e. ( X (,) Y ) ) -> ( ( ( RR _D ( F |` ( X [,] Y ) ) ) ` z ) = ( ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) / ( Y - X ) ) -> ( ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) / ( Y - X ) ) e. S ) )
73 72 rexlimdva 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( E. z e. ( X (,) Y ) ( ( RR _D ( F |` ( X [,] Y ) ) ) ` z ) = ( ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) / ( Y - X ) ) -> ( ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) / ( Y - X ) ) e. S ) )
74 69 73 mpd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( ( ( F |` ( X [,] Y ) ) ` Y ) - ( ( F |` ( X [,] Y ) ) ` X ) ) / ( Y - X ) ) e. S )
75 24 74 eqeltrrd 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. S )