Metamath Proof Explorer

Theorem rolle

Description: Rolle's theorem. If F is a real continuous function on [ A , B ] which is differentiable on ( A , B ) , and F ( A ) = F ( B ) , then there is some x e. ( A , B ) such that ( RR _D F )x = 0 . (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses rolle.a 
|- ( ph -> A e. RR )
rolle.b 
|- ( ph -> B e. RR )
rolle.lt 
|- ( ph -> A < B )
rolle.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
rolle.d 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
rolle.e 
|- ( ph -> ( F ` A ) = ( F ` B ) )
Assertion rolle 
|- ( ph -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )

Proof

Step Hyp Ref Expression
1 rolle.a 
 |-  ( ph -> A e. RR )
2 rolle.b 
 |-  ( ph -> B e. RR )
3 rolle.lt 
 |-  ( ph -> A < B )
4 rolle.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
5 rolle.d 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
6 rolle.e 
 |-  ( ph -> ( F ` A ) = ( F ` B ) )
7 1 2 3 ltled 
 |-  ( ph -> A <_ B )
8 1 2 7 4 evthicc 
 |-  ( ph -> ( E. u e. ( A [,] B ) A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` u ) /\ E. v e. ( A [,] B ) A. y e. ( A [,] B ) ( F ` v ) <_ ( F ` y ) ) )
9 reeanv 
 |-  ( E. u e. ( A [,] B ) E. v e. ( A [,] B ) ( A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` u ) /\ A. y e. ( A [,] B ) ( F ` v ) <_ ( F ` y ) ) <-> ( E. u e. ( A [,] B ) A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` u ) /\ E. v e. ( A [,] B ) A. y e. ( A [,] B ) ( F ` v ) <_ ( F ` y ) ) )
10 8 9 sylibr 
 |-  ( ph -> E. u e. ( A [,] B ) E. v e. ( A [,] B ) ( A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` u ) /\ A. y e. ( A [,] B ) ( F ` v ) <_ ( F ` y ) ) )
11 r19.26 
 |-  ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) <-> ( A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` u ) /\ A. y e. ( A [,] B ) ( F ` v ) <_ ( F ` y ) ) )
12 1 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. u e. { A , B } ) ) -> A e. RR )
13 2 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. u e. { A , B } ) ) -> B e. RR )
14 3 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. u e. { A , B } ) ) -> A < B )
15 4 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. u e. { A , B } ) ) -> F e. ( ( A [,] B ) -cn-> RR ) )
16 5 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. u e. { A , B } ) ) -> dom ( RR _D F ) = ( A (,) B ) )
17 simpl 
 |-  ( ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) -> ( F ` y ) <_ ( F ` u ) )
18 17 ralimi 
 |-  ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) -> A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` u ) )
19 fveq2 
 |-  ( y = t -> ( F ` y ) = ( F ` t ) )
20 19 breq1d 
 |-  ( y = t -> ( ( F ` y ) <_ ( F ` u ) <-> ( F ` t ) <_ ( F ` u ) ) )
21 20 cbvralvw 
 |-  ( A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` u ) <-> A. t e. ( A [,] B ) ( F ` t ) <_ ( F ` u ) )
22 18 21 sylib 
 |-  ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) -> A. t e. ( A [,] B ) ( F ` t ) <_ ( F ` u ) )
23 22 ad2antrl 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. u e. { A , B } ) ) -> A. t e. ( A [,] B ) ( F ` t ) <_ ( F ` u ) )
24 simplrl 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. u e. { A , B } ) ) -> u e. ( A [,] B ) )
25 simprr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. u e. { A , B } ) ) -> -. u e. { A , B } )
26 12 13 14 15 16 23 24 25 rollelem 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. u e. { A , B } ) ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )
27 26 expr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) -> ( -. u e. { A , B } -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
28 1 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> A e. RR )
29 2 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> B e. RR )
30 3 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> A < B )
31 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
32 4 31 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
33 32 ffvelrnda 
 |-  ( ( ph /\ u e. ( A [,] B ) ) -> ( F ` u ) e. RR )
34 33 renegcld 
 |-  ( ( ph /\ u e. ( A [,] B ) ) -> -u ( F ` u ) e. RR )
35 34 fmpttd 
 |-  ( ph -> ( u e. ( A [,] B ) |-> -u ( F ` u ) ) : ( A [,] B ) --> RR )
36 ax-resscn 
 |-  RR C_ CC
37 ssid 
 |-  CC C_ CC
38 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC ) )
39 36 37 38 mp2an 
 |-  ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC )
40 39 4 sselid 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
41 eqid 
 |-  ( u e. ( A [,] B ) |-> -u ( F ` u ) ) = ( u e. ( A [,] B ) |-> -u ( F ` u ) )
42 41 negfcncf 
 |-  ( F e. ( ( A [,] B ) -cn-> CC ) -> ( u e. ( A [,] B ) |-> -u ( F ` u ) ) e. ( ( A [,] B ) -cn-> CC ) )
43 40 42 syl 
 |-  ( ph -> ( u e. ( A [,] B ) |-> -u ( F ` u ) ) e. ( ( A [,] B ) -cn-> CC ) )
44 cncffvrn 
 |-  ( ( RR C_ CC /\ ( u e. ( A [,] B ) |-> -u ( F ` u ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) e. ( ( A [,] B ) -cn-> RR ) <-> ( u e. ( A [,] B ) |-> -u ( F ` u ) ) : ( A [,] B ) --> RR ) )
45 36 43 44 sylancr 
 |-  ( ph -> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) e. ( ( A [,] B ) -cn-> RR ) <-> ( u e. ( A [,] B ) |-> -u ( F ` u ) ) : ( A [,] B ) --> RR ) )
46 35 45 mpbird 
 |-  ( ph -> ( u e. ( A [,] B ) |-> -u ( F ` u ) ) e. ( ( A [,] B ) -cn-> RR ) )
47 46 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> ( u e. ( A [,] B ) |-> -u ( F ` u ) ) e. ( ( A [,] B ) -cn-> RR ) )
48 36 a1i 
 |-  ( ph -> RR C_ CC )
49 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
50 1 2 49 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
51 fss 
 |-  ( ( F : ( A [,] B ) --> RR /\ RR C_ CC ) -> F : ( A [,] B ) --> CC )
52 32 36 51 sylancl 
 |-  ( ph -> F : ( A [,] B ) --> CC )
53 52 ffvelrnda 
 |-  ( ( ph /\ u e. ( A [,] B ) ) -> ( F ` u ) e. CC )
54 53 negcld 
 |-  ( ( ph /\ u e. ( A [,] B ) ) -> -u ( F ` u ) e. CC )
55 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
56 55 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
57 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
58 1 2 57 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
59 48 50 54 56 55 58 dvmptntr 
 |-  ( ph -> ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) = ( RR _D ( u e. ( A (,) B ) |-> -u ( F ` u ) ) ) )
60 reelprrecn 
 |-  RR e. { RR , CC }
61 60 a1i 
 |-  ( ph -> RR e. { RR , CC } )
62 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
63 62 sseli 
 |-  ( u e. ( A (,) B ) -> u e. ( A [,] B ) )
64 63 53 sylan2 
 |-  ( ( ph /\ u e. ( A (,) B ) ) -> ( F ` u ) e. CC )
65 fvexd 
 |-  ( ( ph /\ u e. ( A (,) B ) ) -> ( ( RR _D F ) ` u ) e. _V )
66 32 feqmptd 
 |-  ( ph -> F = ( u e. ( A [,] B ) |-> ( F ` u ) ) )
67 66 oveq2d 
 |-  ( ph -> ( RR _D F ) = ( RR _D ( u e. ( A [,] B ) |-> ( F ` u ) ) ) )
68 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
69 5 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> CC <-> ( RR _D F ) : ( A (,) B ) --> CC ) )
70 68 69 mpbii 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
71 70 feqmptd 
 |-  ( ph -> ( RR _D F ) = ( u e. ( A (,) B ) |-> ( ( RR _D F ) ` u ) ) )
72 48 50 53 56 55 58 dvmptntr 
 |-  ( ph -> ( RR _D ( u e. ( A [,] B ) |-> ( F ` u ) ) ) = ( RR _D ( u e. ( A (,) B ) |-> ( F ` u ) ) ) )
73 67 71 72 3eqtr3rd 
 |-  ( ph -> ( RR _D ( u e. ( A (,) B ) |-> ( F ` u ) ) ) = ( u e. ( A (,) B ) |-> ( ( RR _D F ) ` u ) ) )
74 61 64 65 73 dvmptneg 
 |-  ( ph -> ( RR _D ( u e. ( A (,) B ) |-> -u ( F ` u ) ) ) = ( u e. ( A (,) B ) |-> -u ( ( RR _D F ) ` u ) ) )
75 59 74 eqtrd 
 |-  ( ph -> ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) = ( u e. ( A (,) B ) |-> -u ( ( RR _D F ) ` u ) ) )
76 75 dmeqd 
 |-  ( ph -> dom ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) = dom ( u e. ( A (,) B ) |-> -u ( ( RR _D F ) ` u ) ) )
77 dmmptg 
 |-  ( A. u e. ( A (,) B ) -u ( ( RR _D F ) ` u ) e. _V -> dom ( u e. ( A (,) B ) |-> -u ( ( RR _D F ) ` u ) ) = ( A (,) B ) )
78 negex 
 |-  -u ( ( RR _D F ) ` u ) e. _V
79 78 a1i 
 |-  ( u e. ( A (,) B ) -> -u ( ( RR _D F ) ` u ) e. _V )
80 77 79 mprg 
 |-  dom ( u e. ( A (,) B ) |-> -u ( ( RR _D F ) ` u ) ) = ( A (,) B )
81 76 80 eqtrdi 
 |-  ( ph -> dom ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) = ( A (,) B ) )
82 81 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> dom ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) = ( A (,) B ) )
83 simpr 
 |-  ( ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) -> ( F ` v ) <_ ( F ` y ) )
84 32 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> F : ( A [,] B ) --> RR )
85 simplrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> v e. ( A [,] B ) )
86 84 85 ffvelrnd 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( F ` v ) e. RR )
87 32 adantr 
 |-  ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) -> F : ( A [,] B ) --> RR )
88 87 ffvelrnda 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( F ` y ) e. RR )
89 86 88 lenegd 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( ( F ` v ) <_ ( F ` y ) <-> -u ( F ` y ) <_ -u ( F ` v ) ) )
90 fveq2 
 |-  ( u = y -> ( F ` u ) = ( F ` y ) )
91 90 negeqd 
 |-  ( u = y -> -u ( F ` u ) = -u ( F ` y ) )
92 negex 
 |-  -u ( F ` y ) e. _V
93 91 41 92 fvmpt 
 |-  ( y e. ( A [,] B ) -> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) = -u ( F ` y ) )
94 93 adantl 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) = -u ( F ` y ) )
95 fveq2 
 |-  ( u = v -> ( F ` u ) = ( F ` v ) )
96 95 negeqd 
 |-  ( u = v -> -u ( F ` u ) = -u ( F ` v ) )
97 negex 
 |-  -u ( F ` v ) e. _V
98 96 41 97 fvmpt 
 |-  ( v e. ( A [,] B ) -> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) = -u ( F ` v ) )
99 85 98 syl 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) = -u ( F ` v ) )
100 94 99 breq12d 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) <-> -u ( F ` y ) <_ -u ( F ` v ) ) )
101 89 100 bitr4d 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( ( F ` v ) <_ ( F ` y ) <-> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) ) )
102 83 101 syl5ib 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) -> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) ) )
103 102 ralimdva 
 |-  ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) -> ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) -> A. y e. ( A [,] B ) ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) ) )
104 103 imp 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) -> A. y e. ( A [,] B ) ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) )
105 fveq2 
 |-  ( y = t -> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) = ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` t ) )
106 105 breq1d 
 |-  ( y = t -> ( ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) <-> ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` t ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) ) )
107 106 cbvralvw 
 |-  ( A. y e. ( A [,] B ) ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` y ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) <-> A. t e. ( A [,] B ) ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` t ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) )
108 104 107 sylib 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) -> A. t e. ( A [,] B ) ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` t ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) )
109 108 adantrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> A. t e. ( A [,] B ) ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` t ) <_ ( ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ` v ) )
110 simplrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> v e. ( A [,] B ) )
111 simprr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> -. v e. { A , B } )
112 28 29 30 47 82 109 110 111 rollelem 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> E. x e. ( A (,) B ) ( ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) ` x ) = 0 )
113 75 fveq1d 
 |-  ( ph -> ( ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) ` x ) = ( ( u e. ( A (,) B ) |-> -u ( ( RR _D F ) ` u ) ) ` x ) )
114 fveq2 
 |-  ( u = x -> ( ( RR _D F ) ` u ) = ( ( RR _D F ) ` x ) )
115 114 negeqd 
 |-  ( u = x -> -u ( ( RR _D F ) ` u ) = -u ( ( RR _D F ) ` x ) )
116 eqid 
 |-  ( u e. ( A (,) B ) |-> -u ( ( RR _D F ) ` u ) ) = ( u e. ( A (,) B ) |-> -u ( ( RR _D F ) ` u ) )
117 negex 
 |-  -u ( ( RR _D F ) ` x ) e. _V
118 115 116 117 fvmpt 
 |-  ( x e. ( A (,) B ) -> ( ( u e. ( A (,) B ) |-> -u ( ( RR _D F ) ` u ) ) ` x ) = -u ( ( RR _D F ) ` x ) )
119 113 118 sylan9eq 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) ` x ) = -u ( ( RR _D F ) ` x ) )
120 119 eqeq1d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) ` x ) = 0 <-> -u ( ( RR _D F ) ` x ) = 0 ) )
121 5 eleq2d 
 |-  ( ph -> ( x e. dom ( RR _D F ) <-> x e. ( A (,) B ) ) )
122 121 biimpar 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. dom ( RR _D F ) )
123 68 ffvelrni 
 |-  ( x e. dom ( RR _D F ) -> ( ( RR _D F ) ` x ) e. CC )
124 122 123 syl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
125 124 negeq0d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D F ) ` x ) = 0 <-> -u ( ( RR _D F ) ` x ) = 0 ) )
126 120 125 bitr4d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) ` x ) = 0 <-> ( ( RR _D F ) ` x ) = 0 ) )
127 126 rexbidva 
 |-  ( ph -> ( E. x e. ( A (,) B ) ( ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) ` x ) = 0 <-> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
128 127 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> ( E. x e. ( A (,) B ) ( ( RR _D ( u e. ( A [,] B ) |-> -u ( F ` u ) ) ) ` x ) = 0 <-> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
129 112 128 mpbid 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) /\ -. v e. { A , B } ) ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )
130 129 expr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) -> ( -. v e. { A , B } -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
131 vex 
 |-  u e. _V
132 131 elpr 
 |-  ( u e. { A , B } <-> ( u = A \/ u = B ) )
133 fveq2 
 |-  ( u = A -> ( F ` u ) = ( F ` A ) )
134 133 a1i 
 |-  ( ph -> ( u = A -> ( F ` u ) = ( F ` A ) ) )
135 6 eqcomd 
 |-  ( ph -> ( F ` B ) = ( F ` A ) )
136 fveqeq2 
 |-  ( u = B -> ( ( F ` u ) = ( F ` A ) <-> ( F ` B ) = ( F ` A ) ) )
137 135 136 syl5ibrcom 
 |-  ( ph -> ( u = B -> ( F ` u ) = ( F ` A ) ) )
138 134 137 jaod 
 |-  ( ph -> ( ( u = A \/ u = B ) -> ( F ` u ) = ( F ` A ) ) )
139 132 138 syl5bi 
 |-  ( ph -> ( u e. { A , B } -> ( F ` u ) = ( F ` A ) ) )
140 eleq1w 
 |-  ( u = v -> ( u e. { A , B } <-> v e. { A , B } ) )
141 fveqeq2 
 |-  ( u = v -> ( ( F ` u ) = ( F ` A ) <-> ( F ` v ) = ( F ` A ) ) )
142 140 141 imbi12d 
 |-  ( u = v -> ( ( u e. { A , B } -> ( F ` u ) = ( F ` A ) ) <-> ( v e. { A , B } -> ( F ` v ) = ( F ` A ) ) ) )
143 142 imbi2d 
 |-  ( u = v -> ( ( ph -> ( u e. { A , B } -> ( F ` u ) = ( F ` A ) ) ) <-> ( ph -> ( v e. { A , B } -> ( F ` v ) = ( F ` A ) ) ) ) )
144 143 139 chvarvv 
 |-  ( ph -> ( v e. { A , B } -> ( F ` v ) = ( F ` A ) ) )
145 139 144 anim12d 
 |-  ( ph -> ( ( u e. { A , B } /\ v e. { A , B } ) -> ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) ) )
146 145 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) -> ( ( u e. { A , B } /\ v e. { A , B } ) -> ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) ) )
147 1 rexrd 
 |-  ( ph -> A e. RR* )
148 2 rexrd 
 |-  ( ph -> B e. RR* )
149 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
150 147 148 7 149 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
151 32 150 ffvelrnd 
 |-  ( ph -> ( F ` A ) e. RR )
152 151 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( F ` A ) e. RR )
153 88 152 letri3d 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( ( F ` y ) = ( F ` A ) <-> ( ( F ` y ) <_ ( F ` A ) /\ ( F ` A ) <_ ( F ` y ) ) ) )
154 breq2 
 |-  ( ( F ` u ) = ( F ` A ) -> ( ( F ` y ) <_ ( F ` u ) <-> ( F ` y ) <_ ( F ` A ) ) )
155 breq1 
 |-  ( ( F ` v ) = ( F ` A ) -> ( ( F ` v ) <_ ( F ` y ) <-> ( F ` A ) <_ ( F ` y ) ) )
156 154 155 bi2anan9 
 |-  ( ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) -> ( ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) <-> ( ( F ` y ) <_ ( F ` A ) /\ ( F ` A ) <_ ( F ` y ) ) ) )
157 156 bibi2d 
 |-  ( ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) -> ( ( ( F ` y ) = ( F ` A ) <-> ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) <-> ( ( F ` y ) = ( F ` A ) <-> ( ( F ` y ) <_ ( F ` A ) /\ ( F ` A ) <_ ( F ` y ) ) ) ) )
158 153 157 syl5ibrcom 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) -> ( ( F ` y ) = ( F ` A ) <-> ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) ) )
159 158 impancom 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) ) -> ( y e. ( A [,] B ) -> ( ( F ` y ) = ( F ` A ) <-> ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) ) )
160 159 imp 
 |-  ( ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) ) /\ y e. ( A [,] B ) ) -> ( ( F ` y ) = ( F ` A ) <-> ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) )
161 160 ralbidva 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) ) -> ( A. y e. ( A [,] B ) ( F ` y ) = ( F ` A ) <-> A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) )
162 32 ffnd 
 |-  ( ph -> F Fn ( A [,] B ) )
163 fnconstg 
 |-  ( ( F ` A ) e. RR -> ( ( A [,] B ) X. { ( F ` A ) } ) Fn ( A [,] B ) )
164 151 163 syl 
 |-  ( ph -> ( ( A [,] B ) X. { ( F ` A ) } ) Fn ( A [,] B ) )
165 eqfnfv 
 |-  ( ( F Fn ( A [,] B ) /\ ( ( A [,] B ) X. { ( F ` A ) } ) Fn ( A [,] B ) ) -> ( F = ( ( A [,] B ) X. { ( F ` A ) } ) <-> A. y e. ( A [,] B ) ( F ` y ) = ( ( ( A [,] B ) X. { ( F ` A ) } ) ` y ) ) )
166 162 164 165 syl2anc 
 |-  ( ph -> ( F = ( ( A [,] B ) X. { ( F ` A ) } ) <-> A. y e. ( A [,] B ) ( F ` y ) = ( ( ( A [,] B ) X. { ( F ` A ) } ) ` y ) ) )
167 fvex 
 |-  ( F ` A ) e. _V
168 167 fvconst2 
 |-  ( y e. ( A [,] B ) -> ( ( ( A [,] B ) X. { ( F ` A ) } ) ` y ) = ( F ` A ) )
169 168 eqeq2d 
 |-  ( y e. ( A [,] B ) -> ( ( F ` y ) = ( ( ( A [,] B ) X. { ( F ` A ) } ) ` y ) <-> ( F ` y ) = ( F ` A ) ) )
170 169 ralbiia 
 |-  ( A. y e. ( A [,] B ) ( F ` y ) = ( ( ( A [,] B ) X. { ( F ` A ) } ) ` y ) <-> A. y e. ( A [,] B ) ( F ` y ) = ( F ` A ) )
171 166 170 bitrdi 
 |-  ( ph -> ( F = ( ( A [,] B ) X. { ( F ` A ) } ) <-> A. y e. ( A [,] B ) ( F ` y ) = ( F ` A ) ) )
172 ioon0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) =/= (/) <-> A < B ) )
173 147 148 172 syl2anc 
 |-  ( ph -> ( ( A (,) B ) =/= (/) <-> A < B ) )
174 3 173 mpbird 
 |-  ( ph -> ( A (,) B ) =/= (/) )
175 fconstmpt 
 |-  ( ( A [,] B ) X. { ( F ` A ) } ) = ( u e. ( A [,] B ) |-> ( F ` A ) )
176 175 eqeq2i 
 |-  ( F = ( ( A [,] B ) X. { ( F ` A ) } ) <-> F = ( u e. ( A [,] B ) |-> ( F ` A ) ) )
177 176 biimpi 
 |-  ( F = ( ( A [,] B ) X. { ( F ` A ) } ) -> F = ( u e. ( A [,] B ) |-> ( F ` A ) ) )
178 177 oveq2d 
 |-  ( F = ( ( A [,] B ) X. { ( F ` A ) } ) -> ( RR _D F ) = ( RR _D ( u e. ( A [,] B ) |-> ( F ` A ) ) ) )
179 151 recnd 
 |-  ( ph -> ( F ` A ) e. CC )
180 179 adantr 
 |-  ( ( ph /\ u e. RR ) -> ( F ` A ) e. CC )
181 0cnd 
 |-  ( ( ph /\ u e. RR ) -> 0 e. CC )
182 61 179 dvmptc 
 |-  ( ph -> ( RR _D ( u e. RR |-> ( F ` A ) ) ) = ( u e. RR |-> 0 ) )
183 61 180 181 182 50 56 55 58 dvmptres2 
 |-  ( ph -> ( RR _D ( u e. ( A [,] B ) |-> ( F ` A ) ) ) = ( u e. ( A (,) B ) |-> 0 ) )
184 178 183 sylan9eqr 
 |-  ( ( ph /\ F = ( ( A [,] B ) X. { ( F ` A ) } ) ) -> ( RR _D F ) = ( u e. ( A (,) B ) |-> 0 ) )
185 184 fveq1d 
 |-  ( ( ph /\ F = ( ( A [,] B ) X. { ( F ` A ) } ) ) -> ( ( RR _D F ) ` x ) = ( ( u e. ( A (,) B ) |-> 0 ) ` x ) )
186 eqidd 
 |-  ( u = x -> 0 = 0 )
187 eqid 
 |-  ( u e. ( A (,) B ) |-> 0 ) = ( u e. ( A (,) B ) |-> 0 )
188 c0ex 
 |-  0 e. _V
189 186 187 188 fvmpt 
 |-  ( x e. ( A (,) B ) -> ( ( u e. ( A (,) B ) |-> 0 ) ` x ) = 0 )
190 185 189 sylan9eq 
 |-  ( ( ( ph /\ F = ( ( A [,] B ) X. { ( F ` A ) } ) ) /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) = 0 )
191 190 ralrimiva 
 |-  ( ( ph /\ F = ( ( A [,] B ) X. { ( F ` A ) } ) ) -> A. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )
192 r19.2z 
 |-  ( ( ( A (,) B ) =/= (/) /\ A. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )
193 174 191 192 syl2an2r 
 |-  ( ( ph /\ F = ( ( A [,] B ) X. { ( F ` A ) } ) ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )
194 193 ex 
 |-  ( ph -> ( F = ( ( A [,] B ) X. { ( F ` A ) } ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
195 171 194 sylbird 
 |-  ( ph -> ( A. y e. ( A [,] B ) ( F ` y ) = ( F ` A ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
196 195 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) ) -> ( A. y e. ( A [,] B ) ( F ` y ) = ( F ` A ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
197 161 196 sylbird 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) ) -> ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
198 197 impancom 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) -> ( ( ( F ` u ) = ( F ` A ) /\ ( F ` v ) = ( F ` A ) ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
199 146 198 syld 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) -> ( ( u e. { A , B } /\ v e. { A , B } ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
200 27 130 199 ecased 
 |-  ( ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) /\ A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )
201 200 ex 
 |-  ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) -> ( A. y e. ( A [,] B ) ( ( F ` y ) <_ ( F ` u ) /\ ( F ` v ) <_ ( F ` y ) ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
202 11 201 syl5bir 
 |-  ( ( ph /\ ( u e. ( A [,] B ) /\ v e. ( A [,] B ) ) ) -> ( ( A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` u ) /\ A. y e. ( A [,] B ) ( F ` v ) <_ ( F ` y ) ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
203 202 rexlimdvva 
 |-  ( ph -> ( E. u e. ( A [,] B ) E. v e. ( A [,] B ) ( A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` u ) /\ A. y e. ( A [,] B ) ( F ` v ) <_ ( F ` y ) ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 ) )
204 10 203 mpd 
 |-  ( ph -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )