Metamath Proof Explorer


Theorem elicopnf

Description: Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Assertion elicopnf A B A +∞ B A B

Proof

Step Hyp Ref Expression
1 pnfxr +∞ *
2 elico2 A +∞ * B A +∞ B A B B < +∞
3 1 2 mpan2 A B A +∞ B A B B < +∞
4 ltpnf B B < +∞
5 4 adantr B A B B < +∞
6 5 pm4.71i B A B B A B B < +∞
7 df-3an B A B B < +∞ B A B B < +∞
8 6 7 bitr4i B A B B A B B < +∞
9 3 8 bitr4di A B A +∞ B A B