Metamath Proof Explorer


Theorem o1bddrp

Description: Refine o1bdd2 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypotheses o1bdd2.1 φA
o1bdd2.2 φC
o1bdd2.3 φxAB
o1bdd2.4 φxAB𝑂1
o1bdd2.5 φyCyM
o1bdd2.6 φxAyCyx<yBM
Assertion o1bddrp φm+xABm

Proof

Step Hyp Ref Expression
1 o1bdd2.1 φA
2 o1bdd2.2 φC
3 o1bdd2.3 φxAB
4 o1bdd2.4 φxAB𝑂1
5 o1bdd2.5 φyCyM
6 o1bdd2.6 φxAyCyx<yBM
7 3 abscld φxAB
8 3 lo1o12 φxAB𝑂1xAB𝑂1
9 4 8 mpbid φxAB𝑂1
10 1 2 7 9 5 6 lo1bddrp φm+xABm