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 φ x A B
o1bdd2.4 φ x A B 𝑂1
o1bdd2.5 φ y C y M
o1bdd2.6 φ x A y C y x < y B M
Assertion o1bddrp φ m + x A B m

Proof

Step Hyp Ref Expression
1 o1bdd2.1 φ A
2 o1bdd2.2 φ C
3 o1bdd2.3 φ x A B
4 o1bdd2.4 φ x A B 𝑂1
5 o1bdd2.5 φ y C y M
6 o1bdd2.6 φ x A y C y x < y B M
7 3 abscld φ x A B
8 3 lo1o12 φ x A B 𝑂1 x A B 𝑂1
9 4 8 mpbid φ x A B 𝑂1
10 1 2 7 9 5 6 lo1bddrp φ m + x A B m