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) ) ) )