Metamath Proof Explorer

Theorem cniccbdd

Description: A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Assertion cniccbdd 
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 ral0 
 |-  A. y e. (/) ( abs ` ( F ` y ) ) <_ 0
3 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> A e. RR )
4 3 rexrd 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> A e. RR* )
5 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> B e. RR )
6 5 rexrd 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> B e. RR* )
7 icc0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )
8 4 6 7 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( A [,] B ) = (/) <-> B < A ) )
9 8 biimpar 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ B < A ) -> ( A [,] B ) = (/) )
10 9 raleqdv 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ B < A ) -> ( A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ 0 <-> A. y e. (/) ( abs ` ( F ` y ) ) <_ 0 ) )
11 2 10 mpbiri 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ B < A ) -> A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ 0 )
12 brralrspcev 
 |-  ( ( 0 e. RR /\ A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ 0 ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x )
13 1 11 12 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ B < A ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x )
14 3 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> A e. RR )
15 5 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> B e. RR )
16 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> A <_ B )
17 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. ( ( A [,] B ) -cn-> CC ) )
18 abscncf 
 |-  abs e. ( CC -cn-> RR )
19 18 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> abs e. ( CC -cn-> RR ) )
20 17 19 cncfco 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( abs o. F ) e. ( ( A [,] B ) -cn-> RR ) )
21 20 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> ( abs o. F ) e. ( ( A [,] B ) -cn-> RR ) )
22 14 15 16 21 evthicc 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> ( E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) /\ E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` z ) <_ ( ( abs o. F ) ` y ) ) )
23 22 simpld 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) )
24 cncff 
 |-  ( ( abs o. F ) e. ( ( A [,] B ) -cn-> RR ) -> ( abs o. F ) : ( A [,] B ) --> RR )
25 20 24 syl 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( abs o. F ) : ( A [,] B ) --> RR )
26 25 ffvelrnda 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> ( ( abs o. F ) ` z ) e. RR )
27 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
28 17 27 syl 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F : ( A [,] B ) --> CC )
29 28 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> F : ( A [,] B ) --> CC )
30 fvco3 
 |-  ( ( F : ( A [,] B ) --> CC /\ y e. ( A [,] B ) ) -> ( ( abs o. F ) ` y ) = ( abs ` ( F ` y ) ) )
31 29 30 sylan 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) /\ y e. ( A [,] B ) ) -> ( ( abs o. F ) ` y ) = ( abs ` ( F ` y ) ) )
32 31 breq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) /\ y e. ( A [,] B ) ) -> ( ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) <-> ( abs ` ( F ` y ) ) <_ ( ( abs o. F ) ` z ) ) )
33 32 ralbidva 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> ( A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) <-> A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ ( ( abs o. F ) ` z ) ) )
34 33 biimpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> ( A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) -> A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ ( ( abs o. F ) ` z ) ) )
35 brralrspcev 
 |-  ( ( ( ( abs o. F ) ` z ) e. RR /\ A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ ( ( abs o. F ) ` z ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x )
36 26 34 35 syl6an 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> ( A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) )
37 36 rexlimdva 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) )
38 37 imp 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x )
39 23 38 syldan 
 |-  ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x )
40 13 39 5 3 ltlecasei 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x )