Metamath Proof Explorer


Theorem infmrgelbi

Description: Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013) (Revised by AV, 17-Sep-2020)

Ref Expression
Assertion infmrgelbi A A B x A B x B sup A <

Proof

Step Hyp Ref Expression
1 simpr A A B x A B x x A B x
2 simpl1 A A B x A B x A
3 simpl2 A A B x A B x A
4 breq1 z = B z x B x
5 4 ralbidv z = B x A z x x A B x
6 5 rspcev B x A B x z x A z x
7 6 3ad2antl3 A A B x A B x z x A z x
8 simpl3 A A B x A B x B
9 infregelb A A z x A z x B B sup A < x A B x
10 2 3 7 8 9 syl31anc A A B x A B x B sup A < x A B x
11 1 10 mpbird A A B x A B x B sup A <