This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evthicc

Description: Specialization of the Extreme Value Theorem to a closed interval of RR . (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses evthicc.1 
|- ( ph -> A e. RR )
evthicc.2 
|- ( ph -> B e. RR )
evthicc.3 
|- ( ph -> A <_ B )
evthicc.4 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
Assertion evthicc 
|- ( ph -> ( E. x e. ( A [,] B ) A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` x ) /\ E. z e. ( A [,] B ) A. w e. ( A [,] B ) ( F ` z ) <_ ( F ` w ) ) )

Proof

Step Hyp Ref Expression
1 evthicc.1 
 |-  ( ph -> A e. RR )
2 evthicc.2 
 |-  ( ph -> B e. RR )
3 evthicc.3 
 |-  ( ph -> A <_ B )
4 evthicc.4 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
5 eqid 
 |-  U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) )
6 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
7 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) )
8 6 7 icccmp 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Comp )
9 1 2 8 syl2anc 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Comp )
10 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
11 1 2 10 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
12 ax-resscn 
 |-  RR C_ CC
13 11 12 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
14 eqid 
 |-  ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) = ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) )
15 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
16 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) )
17 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
18 15 17 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
19 14 15 16 18 cncfmet 
 |-  ( ( ( A [,] B ) C_ CC /\ RR C_ CC ) -> ( ( A [,] B ) -cn-> RR ) = ( ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) ) Cn ( topGen ` ran (,) ) ) )
20 13 12 19 sylancl 
 |-  ( ph -> ( ( A [,] B ) -cn-> RR ) = ( ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) ) Cn ( topGen ` ran (,) ) ) )
21 6 16 resubmet 
 |-  ( ( A [,] B ) C_ RR -> ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
22 11 21 syl 
 |-  ( ph -> ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
23 22 oveq1d 
 |-  ( ph -> ( ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) ) Cn ( topGen ` ran (,) ) ) = ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( topGen ` ran (,) ) ) )
24 20 23 eqtrd 
 |-  ( ph -> ( ( A [,] B ) -cn-> RR ) = ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( topGen ` ran (,) ) ) )
25 4 24 eleqtrd 
 |-  ( ph -> F e. ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( topGen ` ran (,) ) ) )
26 retop 
 |-  ( topGen ` ran (,) ) e. Top
27 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
28 27 restuni 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) C_ RR ) -> ( A [,] B ) = U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
29 26 11 28 sylancr 
 |-  ( ph -> ( A [,] B ) = U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
30 1 rexrd 
 |-  ( ph -> A e. RR* )
31 2 rexrd 
 |-  ( ph -> B e. RR* )
32 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
33 30 31 3 32 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
34 33 ne0d 
 |-  ( ph -> ( A [,] B ) =/= (/) )
35 29 34 eqnetrrd 
 |-  ( ph -> U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) =/= (/) )
36 5 6 9 25 35 evth 
 |-  ( ph -> E. x e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) A. y e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ( F ` y ) <_ ( F ` x ) )
37 29 raleqdv 
 |-  ( ph -> ( A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` x ) <-> A. y e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ( F ` y ) <_ ( F ` x ) ) )
38 29 37 rexeqbidv 
 |-  ( ph -> ( E. x e. ( A [,] B ) A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` x ) <-> E. x e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) A. y e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ( F ` y ) <_ ( F ` x ) ) )
39 36 38 mpbird 
 |-  ( ph -> E. x e. ( A [,] B ) A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` x ) )
40 5 6 9 25 35 evth2 
 |-  ( ph -> E. z e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) A. w e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ( F ` z ) <_ ( F ` w ) )
41 29 raleqdv 
 |-  ( ph -> ( A. w e. ( A [,] B ) ( F ` z ) <_ ( F ` w ) <-> A. w e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ( F ` z ) <_ ( F ` w ) ) )
42 29 41 rexeqbidv 
 |-  ( ph -> ( E. z e. ( A [,] B ) A. w e. ( A [,] B ) ( F ` z ) <_ ( F ` w ) <-> E. z e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) A. w e. U. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ( F ` z ) <_ ( F ` w ) ) )
43 40 42 mpbird 
 |-  ( ph -> E. z e. ( A [,] B ) A. w e. ( A [,] B ) ( F ` z ) <_ ( F ` w ) )
44 39 43 jca 
 |-  ( ph -> ( E. x e. ( A [,] B ) A. y e. ( A [,] B ) ( F ` y ) <_ ( F ` x ) /\ E. z e. ( A [,] B ) A. w e. ( A [,] B ) ( F ` z ) <_ ( F ` w ) ) )