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 e. RR* -> ( A e. RR <-> ( -oo < A /\ A < +oo ) ) )

Proof

Step	Hyp	Ref	Expression
1		mnflt	|- ( A e. RR -> -oo < A )
2		ltpnf	|- ( A e. RR -> A < +oo )
3	1 2	jca	|- ( A e. RR -> ( -oo < A /\ A < +oo ) )
4		nltpnft	|- ( A e. RR* -> ( A = +oo <-> -. A < +oo ) )
5		ngtmnft	|- ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )
6	4 5	orbi12d	|- ( A e. RR* -> ( ( A = +oo \/ A = -oo ) <-> ( -. A < +oo \/ -. -oo < A ) ) )
7		ianor	|- ( -. ( -oo < A /\ A < +oo ) <-> ( -. -oo < A \/ -. A < +oo ) )
8		orcom	|- ( ( -. -oo < A \/ -. A < +oo ) <-> ( -. A < +oo \/ -. -oo < A ) )
9	7 8	bitr2i	|- ( ( -. A < +oo \/ -. -oo < A ) <-> -. ( -oo < A /\ A < +oo ) )
10	6 9	bitrdi	|- ( A e. RR* -> ( ( A = +oo \/ A = -oo ) <-> -. ( -oo < A /\ A < +oo ) ) )
11	10	con2bid	|- ( A e. RR* -> ( ( -oo < A /\ A < +oo ) <-> -. ( A = +oo \/ A = -oo ) ) )
12		elxr	|- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
13		3orass	|- ( ( A e. RR \/ A = +oo \/ A = -oo ) <-> ( A e. RR \/ ( A = +oo \/ A = -oo ) ) )
14		orcom	|- ( ( A e. RR \/ ( A = +oo \/ A = -oo ) ) <-> ( ( A = +oo \/ A = -oo ) \/ A e. RR ) )
15	13 14	bitri	|- ( ( A e. RR \/ A = +oo \/ A = -oo ) <-> ( ( A = +oo \/ A = -oo ) \/ A e. RR ) )
16	12 15	sylbb	|- ( A e. RR* -> ( ( A = +oo \/ A = -oo ) \/ A e. RR ) )
17	16	ord	|- ( A e. RR* -> ( -. ( A = +oo \/ A = -oo ) -> A e. RR ) )
18	11 17	sylbid	|- ( A e. RR* -> ( ( -oo < A /\ A < +oo ) -> A e. RR ) )
19	3 18	impbid2	|- ( A e. RR* -> ( A e. RR <-> ( -oo < A /\ A < +oo ) ) )