Metamath Proof Explorer


Theorem xrre3

Description: A way of proving that an extended real is real. (Contributed by FL, 29-May-2014)

Ref Expression
Assertion xrre3 A * B B A A < +∞ A

Proof

Step Hyp Ref Expression
1 mnflt B −∞ < B
2 1 adantl A * B −∞ < B
3 mnfxr −∞ *
4 rexr B B *
5 4 adantl A * B B *
6 simpl A * B A *
7 xrltletr −∞ * B * A * −∞ < B B A −∞ < A
8 3 5 6 7 mp3an2i A * B −∞ < B B A −∞ < A
9 2 8 mpand A * B B A −∞ < A
10 9 imp A * B B A −∞ < A
11 10 adantrr A * B B A A < +∞ −∞ < A
12 simprr A * B B A A < +∞ A < +∞
13 xrrebnd A * A −∞ < A A < +∞
14 13 ad2antrr A * B B A A < +∞ A −∞ < A A < +∞
15 11 12 14 mpbir2and A * B B A A < +∞ A