Metamath Proof Explorer


Theorem xrrebnd

Description: An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006)

Ref Expression
Assertion xrrebnd A * A −∞ < A A < +∞

Proof

Step Hyp Ref Expression
1 mnflt A −∞ < A
2 ltpnf A A < +∞
3 1 2 jca A −∞ < A A < +∞
4 nltpnft A * A = +∞ ¬ A < +∞
5 ngtmnft A * A = −∞ ¬ −∞ < A
6 4 5 orbi12d A * A = +∞ A = −∞ ¬ A < +∞ ¬ −∞ < A
7 ianor ¬ −∞ < A A < +∞ ¬ −∞ < A ¬ A < +∞
8 orcom ¬ −∞ < A ¬ A < +∞ ¬ A < +∞ ¬ −∞ < A
9 7 8 bitr2i ¬ A < +∞ ¬ −∞ < A ¬ −∞ < A A < +∞
10 6 9 bitrdi A * A = +∞ A = −∞ ¬ −∞ < A A < +∞
11 10 con2bid A * −∞ < A A < +∞ ¬ A = +∞ A = −∞
12 elxr A * A A = +∞ A = −∞
13 3orass A A = +∞ A = −∞ A A = +∞ A = −∞
14 orcom A A = +∞ A = −∞ A = +∞ A = −∞ A
15 13 14 bitri A A = +∞ A = −∞ A = +∞ A = −∞ A
16 12 15 sylbb A * A = +∞ A = −∞ A
17 16 ord A * ¬ A = +∞ A = −∞ A
18 11 17 sylbid A * −∞ < A A < +∞ A
19 3 18 impbid2 A * A −∞ < A A < +∞