Description: The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | nmopre | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bdopf | |
|
2 | nmopgtmnf | |
|
3 | 1 2 | syl | |
4 | elbdop | |
|
5 | 4 | simprbi | |
6 | nmopxr | |
|
7 | xrrebnd | |
|
8 | 1 6 7 | 3syl | |
9 | 3 5 8 | mpbir2and | |