Metamath Proof Explorer

Theorem lo1bdd2

Description: If an eventually bounded function is bounded on every interval A i^i ( -oo , y ) by a function M ( y ) , then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016)

Ref Expression
Hypotheses lo1bdd2.1 
|- ( ph -> A C_ RR )
lo1bdd2.2 
|- ( ph -> C e. RR )
lo1bdd2.3 
|- ( ( ph /\ x e. A ) -> B e. RR )
lo1bdd2.4 
|- ( ph -> ( x e. A |-> B ) e. <_O(1) )
lo1bdd2.5 
|- ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )
lo1bdd2.6 
|- ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> B <_ M )
Assertion lo1bdd2 
|- ( ph -> E. m e. RR A. x e. A B <_ m )

Proof

Step Hyp Ref Expression
1 lo1bdd2.1 
 |-  ( ph -> A C_ RR )
2 lo1bdd2.2 
 |-  ( ph -> C e. RR )
3 lo1bdd2.3 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
4 lo1bdd2.4 
 |-  ( ph -> ( x e. A |-> B ) e. <_O(1) )
5 lo1bdd2.5 
 |-  ( ( ph /\ ( y e. RR /\ C <_ y ) ) -> M e. RR )
6 lo1bdd2.6 
 |-  ( ( ( ph /\ x e. A ) /\ ( ( y e. RR /\ C <_ y ) /\ x < y ) ) -> B <_ M )
7 1 3 2 ello1mpt2 
 |-  ( ph -> ( ( x e. A |-> B ) e. <_O(1) <-> E. y e. ( C [,) +oo ) E. n e. RR A. x e. A ( y <_ x -> B <_ n ) ) )
8 4 7 mpbid 
 |-  ( ph -> E. y e. ( C [,) +oo ) E. n e. RR A. x e. A ( y <_ x -> B <_ n ) )
9 elicopnf 
 |-  ( C e. RR -> ( y e. ( C [,) +oo ) <-> ( y e. RR /\ C <_ y ) ) )
10 2 9 syl 
 |-  ( ph -> ( y e. ( C [,) +oo ) <-> ( y e. RR /\ C <_ y ) ) )
11 10 biimpa 
 |-  ( ( ph /\ y e. ( C [,) +oo ) ) -> ( y e. RR /\ C <_ y ) )
12 11 5 syldan 
 |-  ( ( ph /\ y e. ( C [,) +oo ) ) -> M e. RR )
13 12 ad2antrr 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ ( n e. RR /\ A. x e. A ( y <_ x -> B <_ n ) ) ) /\ n <_ M ) -> M e. RR )
14 simplrl 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ ( n e. RR /\ A. x e. A ( y <_ x -> B <_ n ) ) ) /\ -. n <_ M ) -> n e. RR )
15 13 14 ifclda 
 |-  ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ ( n e. RR /\ A. x e. A ( y <_ x -> B <_ n ) ) ) -> if ( n <_ M , M , n ) e. RR )
16 1 ad2antrr 
 |-  ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) -> A C_ RR )
17 16 sselda 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> x e. RR )
18 11 simpld 
 |-  ( ( ph /\ y e. ( C [,) +oo ) ) -> y e. RR )
19 18 ad2antrr 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> y e. RR )
20 17 19 ltnled 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> ( x < y <-> -. y <_ x ) )
21 6 expr 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. RR /\ C <_ y ) ) -> ( x < y -> B <_ M ) )
22 21 an32s 
 |-  ( ( ( ph /\ ( y e. RR /\ C <_ y ) ) /\ x e. A ) -> ( x < y -> B <_ M ) )
23 11 22 syldanl 
 |-  ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ x e. A ) -> ( x < y -> B <_ M ) )
24 23 adantlr 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> ( x < y -> B <_ M ) )
25 simplr 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> n e. RR )
26 12 ad2antrr 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> M e. RR )
27 max2 
 |-  ( ( n e. RR /\ M e. RR ) -> M <_ if ( n <_ M , M , n ) )
28 25 26 27 syl2anc 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> M <_ if ( n <_ M , M , n ) )
29 3 ad4ant14 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> B e. RR )
30 12 ad5ant12 
 |-  ( ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) /\ n <_ M ) -> M e. RR )
31 simpllr 
 |-  ( ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) /\ -. n <_ M ) -> n e. RR )
32 30 31 ifclda 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> if ( n <_ M , M , n ) e. RR )
33 letr 
 |-  ( ( B e. RR /\ M e. RR /\ if ( n <_ M , M , n ) e. RR ) -> ( ( B <_ M /\ M <_ if ( n <_ M , M , n ) ) -> B <_ if ( n <_ M , M , n ) ) )
34 29 26 32 33 syl3anc 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> ( ( B <_ M /\ M <_ if ( n <_ M , M , n ) ) -> B <_ if ( n <_ M , M , n ) ) )
35 28 34 mpan2d 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> ( B <_ M -> B <_ if ( n <_ M , M , n ) ) )
36 24 35 syld 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> ( x < y -> B <_ if ( n <_ M , M , n ) ) )
37 20 36 sylbird 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> ( -. y <_ x -> B <_ if ( n <_ M , M , n ) ) )
38 max1 
 |-  ( ( n e. RR /\ M e. RR ) -> n <_ if ( n <_ M , M , n ) )
39 25 26 38 syl2anc 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> n <_ if ( n <_ M , M , n ) )
40 letr 
 |-  ( ( B e. RR /\ n e. RR /\ if ( n <_ M , M , n ) e. RR ) -> ( ( B <_ n /\ n <_ if ( n <_ M , M , n ) ) -> B <_ if ( n <_ M , M , n ) ) )
41 29 25 32 40 syl3anc 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> ( ( B <_ n /\ n <_ if ( n <_ M , M , n ) ) -> B <_ if ( n <_ M , M , n ) ) )
42 39 41 mpan2d 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> ( B <_ n -> B <_ if ( n <_ M , M , n ) ) )
43 37 42 jad 
 |-  ( ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) /\ x e. A ) -> ( ( y <_ x -> B <_ n ) -> B <_ if ( n <_ M , M , n ) ) )
44 43 ralimdva 
 |-  ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) -> ( A. x e. A ( y <_ x -> B <_ n ) -> A. x e. A B <_ if ( n <_ M , M , n ) ) )
45 44 impr 
 |-  ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ ( n e. RR /\ A. x e. A ( y <_ x -> B <_ n ) ) ) -> A. x e. A B <_ if ( n <_ M , M , n ) )
46 brralrspcev 
 |-  ( ( if ( n <_ M , M , n ) e. RR /\ A. x e. A B <_ if ( n <_ M , M , n ) ) -> E. m e. RR A. x e. A B <_ m )
47 15 45 46 syl2anc 
 |-  ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ ( n e. RR /\ A. x e. A ( y <_ x -> B <_ n ) ) ) -> E. m e. RR A. x e. A B <_ m )
48 47 expr 
 |-  ( ( ( ph /\ y e. ( C [,) +oo ) ) /\ n e. RR ) -> ( A. x e. A ( y <_ x -> B <_ n ) -> E. m e. RR A. x e. A B <_ m ) )
49 48 rexlimdva 
 |-  ( ( ph /\ y e. ( C [,) +oo ) ) -> ( E. n e. RR A. x e. A ( y <_ x -> B <_ n ) -> E. m e. RR A. x e. A B <_ m ) )
50 49 rexlimdva 
 |-  ( ph -> ( E. y e. ( C [,) +oo ) E. n e. RR A. x e. A ( y <_ x -> B <_ n ) -> E. m e. RR A. x e. A B <_ m ) )
51 8 50 mpd 
 |-  ( ph -> E. m e. RR A. x e. A B <_ m )