Metamath Proof Explorer


Theorem elioomnf

Description: Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion elioomnf A * B −∞ A B B < A

Proof

Step Hyp Ref Expression
1 mnfxr −∞ *
2 elioo2 −∞ * A * B −∞ A B −∞ < B B < A
3 1 2 mpan A * B −∞ A B −∞ < B B < A
4 an32 B −∞ < B B < A B B < A −∞ < B
5 df-3an B −∞ < B B < A B −∞ < B B < A
6 mnflt B −∞ < B
7 6 adantr B B < A −∞ < B
8 7 pm4.71i B B < A B B < A −∞ < B
9 4 5 8 3bitr4i B −∞ < B B < A B B < A
10 3 9 bitrdi A * B −∞ A B B < A