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 )