Metamath Proof Explorer

Theorem rollelem

Description: Lemma for rolle . (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.r 
|- ( ph -> A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` U ) )
rolle.u 
|- ( ph -> U e. ( A [,] B ) )
rolle.n 
|- ( ph -> -. U e. { A , B } )
Assertion rollelem 
|- ( 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.r 
 |-  ( ph -> A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` U ) )
7 rolle.u 
 |-  ( ph -> U e. ( A [,] B ) )
8 rolle.n 
 |-  ( ph -> -. U e. { A , B } )
9 1 rexrd 
 |-  ( ph -> A e. RR* )
10 2 rexrd 
 |-  ( ph -> B e. RR* )
11 1 2 3 ltled 
 |-  ( ph -> A <_ B )
12 prunioo 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
13 9 10 11 12 syl3anc 
 |-  ( ph -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
14 7 13 eleqtrrd 
 |-  ( ph -> U e. ( ( A (,) B ) u. { A , B } ) )
15 elun 
 |-  ( U e. ( ( A (,) B ) u. { A , B } ) <-> ( U e. ( A (,) B ) \/ U e. { A , B } ) )
16 14 15 sylib 
 |-  ( ph -> ( U e. ( A (,) B ) \/ U e. { A , B } ) )
17 16 ord 
 |-  ( ph -> ( -. U e. ( A (,) B ) -> U e. { A , B } ) )
18 8 17 mt3d 
 |-  ( ph -> U e. ( A (,) B ) )
19 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
20 4 19 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
21 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
22 1 2 21 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
23 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
24 23 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
25 18 5 eleqtrrd 
 |-  ( ph -> U e. dom ( RR _D F ) )
26 ssralv 
 |-  ( ( A (,) B ) C_ ( A [,] B ) -> ( A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` U ) -> A. y e. ( A (,) B ) ( F ` y ) <_ ( F ` U ) ) )
27 24 6 26 sylc 
 |-  ( ph -> A. y e. ( A (,) B ) ( F ` y ) <_ ( F ` U ) )
28 20 22 18 24 25 27 dvferm 
 |-  ( ph -> ( ( RR _D F ) ` U ) = 0 )
29 fveqeq2 
 |-  ( x = U -> ( ( ( RR _D F ) ` x ) = 0 <-> ( ( RR _D F ) ` U ) = 0 ) )
30 29 rspcev 
 |-  ( ( U e. ( A (,) B ) /\ ( ( RR _D F ) ` U ) = 0 ) -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )
31 18 28 30 syl2anc 
 |-  ( ph -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = 0 )