Theorem nmopreltpnf

Description: The norm of a Hilbert space operator is real iff it is less than infinity. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopreltpnf	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmoprepnf	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)\ne \mathrm{+\infty }\right)$$
2		nmopxr	$$⊢T:\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left(T\right)\in {ℝ}^{*}$$
3		nltpnft	$$⊢{norm}_{\mathrm{op}}\left(T\right)\in {ℝ}^{*}\to \left({norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\leftrightarrow \neg {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)$$
4	2 3	syl	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left({norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\leftrightarrow \neg {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)$$
5	4	necon2abid	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left({norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)\ne \mathrm{+\infty }\right)$$
6	1 5	bitr4d	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)$$