Metamath Proof Explorer

Theorem o1lo1

Description: A real function is eventually bounded iff it is eventually lower bounded and eventually upper bounded. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypothesis o1lo1.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion o1lo1 
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) )

Proof

Step Hyp Ref Expression
1 o1lo1.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 o1dm 
 |-  ( ( x e. A |-> B ) e. O(1) -> dom ( x e. A |-> B ) C_ RR )
3 2 a1i 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) -> dom ( x e. A |-> B ) C_ RR ) )
4 lo1dm 
 |-  ( ( x e. A |-> B ) e. <_O(1) -> dom ( x e. A |-> B ) C_ RR )
5 4 adantr 
 |-  ( ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) -> dom ( x e. A |-> B ) C_ RR )
6 5 a1i 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) -> dom ( x e. A |-> B ) C_ RR ) )
7 1 ralrimiva 
 |-  ( ph -> A. x e. A B e. RR )
8 dmmptg 
 |-  ( A. x e. A B e. RR -> dom ( x e. A |-> B ) = A )
9 7 8 syl 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
10 9 sseq1d 
 |-  ( ph -> ( dom ( x e. A |-> B ) C_ RR <-> A C_ RR ) )
11 simpr 
 |-  ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> m e. RR )
12 1 adantlr 
 |-  ( ( ( ph /\ A C_ RR ) /\ x e. A ) -> B e. RR )
13 12 adantlr 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> B e. RR )
14 simplr 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> m e. RR )
15 13 14 absled 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( abs ` B ) <_ m <-> ( -u m <_ B /\ B <_ m ) ) )
16 ancom 
 |-  ( ( -u m <_ B /\ B <_ m ) <-> ( B <_ m /\ -u m <_ B ) )
17 lenegcon1 
 |-  ( ( m e. RR /\ B e. RR ) -> ( -u m <_ B <-> -u B <_ m ) )
18 14 13 17 syl2anc 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( -u m <_ B <-> -u B <_ m ) )
19 18 anbi2d 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( B <_ m /\ -u m <_ B ) <-> ( B <_ m /\ -u B <_ m ) ) )
20 16 19 syl5bb 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( -u m <_ B /\ B <_ m ) <-> ( B <_ m /\ -u B <_ m ) ) )
21 15 20 bitrd 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( abs ` B ) <_ m <-> ( B <_ m /\ -u B <_ m ) ) )
22 21 imbi2d 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ m e. RR ) /\ x e. A ) -> ( ( c <_ x -> ( abs ` B ) <_ m ) <-> ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) )
23 22 ralbidva 
 |-  ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> ( A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) )
24 23 rexbidv 
 |-  ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) )
25 24 biimpd 
 |-  ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) -> E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) )
26 breq2 
 |-  ( n = m -> ( B <_ n <-> B <_ m ) )
27 26 anbi1d 
 |-  ( n = m -> ( ( B <_ n /\ -u B <_ p ) <-> ( B <_ m /\ -u B <_ p ) ) )
28 27 imbi2d 
 |-  ( n = m -> ( ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> ( c <_ x -> ( B <_ m /\ -u B <_ p ) ) ) )
29 28 rexralbidv 
 |-  ( n = m -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ p ) ) ) )
30 breq2 
 |-  ( p = m -> ( -u B <_ p <-> -u B <_ m ) )
31 30 anbi2d 
 |-  ( p = m -> ( ( B <_ m /\ -u B <_ p ) <-> ( B <_ m /\ -u B <_ m ) ) )
32 31 imbi2d 
 |-  ( p = m -> ( ( c <_ x -> ( B <_ m /\ -u B <_ p ) ) <-> ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) )
33 32 rexralbidv 
 |-  ( p = m -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ p ) ) <-> E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) )
34 29 33 rspc2ev 
 |-  ( ( m e. RR /\ m e. RR /\ E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) -> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) )
35 34 3anidm12 
 |-  ( ( m e. RR /\ E. c e. RR A. x e. A ( c <_ x -> ( B <_ m /\ -u B <_ m ) ) ) -> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) )
36 11 25 35 syl6an 
 |-  ( ( ( ph /\ A C_ RR ) /\ m e. RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) -> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) ) )
37 36 rexlimdva 
 |-  ( ( ph /\ A C_ RR ) -> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) -> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) ) )
38 simplrr 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ n <_ p ) -> p e. RR )
39 simplrl 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ -. n <_ p ) -> n e. RR )
40 38 39 ifclda 
 |-  ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) -> if ( n <_ p , p , n ) e. RR )
41 max2 
 |-  ( ( n e. RR /\ p e. RR ) -> p <_ if ( n <_ p , p , n ) )
42 41 ad2antlr 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> p <_ if ( n <_ p , p , n ) )
43 12 adantlr 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> B e. RR )
44 43 renegcld 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> -u B e. RR )
45 simplrr 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> p e. RR )
46 simplrl 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> n e. RR )
47 45 46 ifcld 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> if ( n <_ p , p , n ) e. RR )
48 letr 
 |-  ( ( -u B e. RR /\ p e. RR /\ if ( n <_ p , p , n ) e. RR ) -> ( ( -u B <_ p /\ p <_ if ( n <_ p , p , n ) ) -> -u B <_ if ( n <_ p , p , n ) ) )
49 44 45 47 48 syl3anc 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( -u B <_ p /\ p <_ if ( n <_ p , p , n ) ) -> -u B <_ if ( n <_ p , p , n ) ) )
50 42 49 mpan2d 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( -u B <_ p -> -u B <_ if ( n <_ p , p , n ) ) )
51 lenegcon1 
 |-  ( ( B e. RR /\ if ( n <_ p , p , n ) e. RR ) -> ( -u B <_ if ( n <_ p , p , n ) <-> -u if ( n <_ p , p , n ) <_ B ) )
52 43 47 51 syl2anc 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( -u B <_ if ( n <_ p , p , n ) <-> -u if ( n <_ p , p , n ) <_ B ) )
53 50 52 sylibd 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( -u B <_ p -> -u if ( n <_ p , p , n ) <_ B ) )
54 max1 
 |-  ( ( n e. RR /\ p e. RR ) -> n <_ if ( n <_ p , p , n ) )
55 54 ad2antlr 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> n <_ if ( n <_ p , p , n ) )
56 letr 
 |-  ( ( B e. RR /\ n e. RR /\ if ( n <_ p , p , n ) e. RR ) -> ( ( B <_ n /\ n <_ if ( n <_ p , p , n ) ) -> B <_ if ( n <_ p , p , n ) ) )
57 43 46 47 56 syl3anc 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( B <_ n /\ n <_ if ( n <_ p , p , n ) ) -> B <_ if ( n <_ p , p , n ) ) )
58 55 57 mpan2d 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( B <_ n -> B <_ if ( n <_ p , p , n ) ) )
59 53 58 anim12d 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( -u B <_ p /\ B <_ n ) -> ( -u if ( n <_ p , p , n ) <_ B /\ B <_ if ( n <_ p , p , n ) ) ) )
60 59 ancomsd 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( B <_ n /\ -u B <_ p ) -> ( -u if ( n <_ p , p , n ) <_ B /\ B <_ if ( n <_ p , p , n ) ) ) )
61 43 47 absled 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( abs ` B ) <_ if ( n <_ p , p , n ) <-> ( -u if ( n <_ p , p , n ) <_ B /\ B <_ if ( n <_ p , p , n ) ) ) )
62 60 61 sylibrd 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( B <_ n /\ -u B <_ p ) -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) )
63 62 imim2d 
 |-  ( ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) /\ x e. A ) -> ( ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) )
64 63 ralimdva 
 |-  ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) -> ( A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> A. x e. A ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) )
65 64 reximdv 
 |-  ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) )
66 breq2 
 |-  ( m = if ( n <_ p , p , n ) -> ( ( abs ` B ) <_ m <-> ( abs ` B ) <_ if ( n <_ p , p , n ) ) )
67 66 imbi2d 
 |-  ( m = if ( n <_ p , p , n ) -> ( ( c <_ x -> ( abs ` B ) <_ m ) <-> ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) )
68 67 rexralbidv 
 |-  ( m = if ( n <_ p , p , n ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) )
69 68 rspcev 
 |-  ( ( if ( n <_ p , p , n ) e. RR /\ E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ if ( n <_ p , p , n ) ) ) -> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) )
70 40 65 69 syl6an 
 |-  ( ( ( ph /\ A C_ RR ) /\ ( n e. RR /\ p e. RR ) ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) ) )
71 70 rexlimdvva 
 |-  ( ( ph /\ A C_ RR ) -> ( E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) -> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) ) )
72 37 71 impbid 
 |-  ( ( ph /\ A C_ RR ) -> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) ) )
73 rexanre 
 |-  ( A C_ RR -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) )
74 73 adantl 
 |-  ( ( ph /\ A C_ RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) )
75 74 2rexbidv 
 |-  ( ( ph /\ A C_ RR ) -> ( E. n e. RR E. p e. RR E. c e. RR A. x e. A ( c <_ x -> ( B <_ n /\ -u B <_ p ) ) <-> E. n e. RR E. p e. RR ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) )
76 72 75 bitrd 
 |-  ( ( ph /\ A C_ RR ) -> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. n e. RR E. p e. RR ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) )
77 reeanv 
 |-  ( E. n e. RR E. p e. RR ( E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) <-> ( E. n e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. p e. RR E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) )
78 76 77 bitrdi 
 |-  ( ( ph /\ A C_ RR ) -> ( E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> ( E. n e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. p e. RR E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) )
79 rexcom 
 |-  ( E. c e. RR E. m e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> E. m e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) )
80 rexcom 
 |-  ( E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) <-> E. n e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ n ) )
81 rexcom 
 |-  ( E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) <-> E. p e. RR E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) )
82 80 81 anbi12i 
 |-  ( ( E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) <-> ( E. n e. RR E. c e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. p e. RR E. c e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) )
83 78 79 82 3bitr4g 
 |-  ( ( ph /\ A C_ RR ) -> ( E. c e. RR E. m e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) <-> ( E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) )
84 simpr 
 |-  ( ( ph /\ A C_ RR ) -> A C_ RR )
85 12 recnd 
 |-  ( ( ( ph /\ A C_ RR ) /\ x e. A ) -> B e. CC )
86 84 85 elo1mpt 
 |-  ( ( ph /\ A C_ RR ) -> ( ( x e. A |-> B ) e. O(1) <-> E. c e. RR E. m e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ m ) ) )
87 84 12 ello1mpt 
 |-  ( ( ph /\ A C_ RR ) -> ( ( x e. A |-> B ) e. <_O(1) <-> E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) ) )
88 12 renegcld 
 |-  ( ( ( ph /\ A C_ RR ) /\ x e. A ) -> -u B e. RR )
89 84 88 ello1mpt 
 |-  ( ( ph /\ A C_ RR ) -> ( ( x e. A |-> -u B ) e. <_O(1) <-> E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) )
90 87 89 anbi12d 
 |-  ( ( ph /\ A C_ RR ) -> ( ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) <-> ( E. c e. RR E. n e. RR A. x e. A ( c <_ x -> B <_ n ) /\ E. c e. RR E. p e. RR A. x e. A ( c <_ x -> -u B <_ p ) ) ) )
91 83 86 90 3bitr4d 
 |-  ( ( ph /\ A C_ RR ) -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) )
92 91 ex 
 |-  ( ph -> ( A C_ RR -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) ) )
93 10 92 sylbid 
 |-  ( ph -> ( dom ( x e. A |-> B ) C_ RR -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) ) )
94 3 6 93 pm5.21ndd 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) )