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 φxAB
o1lo12.2 φM
o1lo12.3 φxAMB
Assertion o1lo12 φxAB𝑂1xAB𝑂1

Proof

Step Hyp Ref Expression
1 o1lo1.1 φxAB
2 o1lo12.2 φM
3 o1lo12.3 φxAMB
4 o1dm xAB𝑂1domxAB
5 4 a1i φxAB𝑂1domxAB
6 lo1dm xAB𝑂1domxAB
7 6 a1i φxAB𝑂1domxAB
8 1 ralrimiva φxAB
9 dmmptg xABdomxAB=A
10 8 9 syl φdomxAB=A
11 10 sseq1d φdomxABA
12 simpr φAA
13 1 renegcld φxAB
14 13 adantlr φAxAB
15 2 adantr φAM
16 15 renegcld φAM
17 2 adantr φxAM
18 17 1 lenegd φxAMBBM
19 3 18 mpbid φxABM
20 19 ad2ant2r φAxAMxBM
21 12 14 15 16 20 ello1d φAxAB𝑂1
22 1 o1lo1 φxAB𝑂1xAB𝑂1xAB𝑂1
23 22 rbaibd φxAB𝑂1xAB𝑂1xAB𝑂1
24 21 23 syldan φAxAB𝑂1xAB𝑂1
25 24 ex φAxAB𝑂1xAB𝑂1
26 11 25 sylbid φdomxABxAB𝑂1xAB𝑂1
27 5 7 26 pm5.21ndd φxAB𝑂1xAB𝑂1