# Metamath Proof Explorer

## 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}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{op}}\left({T}\right)<\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 nmoprepnf ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{op}}\left({T}\right)\ne \mathrm{+\infty }\right)$
2 nmopxr ${⊢}{T}:ℋ⟶ℋ\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 }↔¬{norm}_{\mathrm{op}}\left({T}\right)<\mathrm{+\infty }\right)$
4 2 3 syl ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }↔¬{norm}_{\mathrm{op}}\left({T}\right)<\mathrm{+\infty }\right)$
5 4 necon2abid ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)<\mathrm{+\infty }↔{norm}_{\mathrm{op}}\left({T}\right)\ne \mathrm{+\infty }\right)$
6 1 5 bitr4d ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{op}}\left({T}\right)<\mathrm{+\infty }\right)$