This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem o1lo12

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

Ref Expression
Hypotheses o1lo1.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
o1lo12.2 
|- ( ph -> M e. RR )
o1lo12.3 
|- ( ( ph /\ x e. A ) -> M <_ B )
Assertion o1lo12 
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> B ) e. <_O(1) ) )

Proof

Step Hyp Ref Expression
1 o1lo1.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 o1lo12.2 
 |-  ( ph -> M e. RR )
3 o1lo12.3 
 |-  ( ( ph /\ x e. A ) -> M <_ B )
4 o1dm 
 |-  ( ( x e. A |-> B ) e. O(1) -> dom ( x e. A |-> B ) C_ RR )
5 4 a1i 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) -> dom ( x e. A |-> B ) C_ RR ) )
6 lo1dm 
 |-  ( ( x e. A |-> B ) e. <_O(1) -> dom ( x e. A |-> B ) C_ RR )
7 6 a1i 
 |-  ( ph -> ( ( x e. A |-> B ) e. <_O(1) -> dom ( x e. A |-> B ) C_ RR ) )
8 1 ralrimiva 
 |-  ( ph -> A. x e. A B e. RR )
9 dmmptg 
 |-  ( A. x e. A B e. RR -> dom ( x e. A |-> B ) = A )
10 8 9 syl 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
11 10 sseq1d 
 |-  ( ph -> ( dom ( x e. A |-> B ) C_ RR <-> A C_ RR ) )
12 simpr 
 |-  ( ( ph /\ A C_ RR ) -> A C_ RR )
13 1 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
14 13 adantlr 
 |-  ( ( ( ph /\ A C_ RR ) /\ x e. A ) -> -u B e. RR )
15 2 adantr 
 |-  ( ( ph /\ A C_ RR ) -> M e. RR )
16 15 renegcld 
 |-  ( ( ph /\ A C_ RR ) -> -u M e. RR )
17 2 adantr 
 |-  ( ( ph /\ x e. A ) -> M e. RR )
18 17 1 lenegd 
 |-  ( ( ph /\ x e. A ) -> ( M <_ B <-> -u B <_ -u M ) )
19 3 18 mpbid 
 |-  ( ( ph /\ x e. A ) -> -u B <_ -u M )
20 19 ad2ant2r 
 |-  ( ( ( ph /\ A C_ RR ) /\ ( x e. A /\ M <_ x ) ) -> -u B <_ -u M )
21 12 14 15 16 20 ello1d 
 |-  ( ( ph /\ A C_ RR ) -> ( x e. A |-> -u B ) e. <_O(1) )
22 1 o1lo1 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) )
23 22 rbaibd 
 |-  ( ( ph /\ ( x e. A |-> -u B ) e. <_O(1) ) -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> B ) e. <_O(1) ) )
24 21 23 syldan 
 |-  ( ( ph /\ A C_ RR ) -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> B ) e. <_O(1) ) )
25 24 ex 
 |-  ( ph -> ( A C_ RR -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> B ) e. <_O(1) ) ) )
26 11 25 sylbid 
 |-  ( ph -> ( dom ( x e. A |-> B ) C_ RR -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> B ) e. <_O(1) ) ) )
27 5 7 26 pm5.21ndd 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> B ) e. <_O(1) ) )