HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem nmo0 16707
Description: The operator norm of the zero operator.
Hypotheses
Ref Expression
nmo0.3
nmo0.0
Assertion
Ref Expression
nmo0

Proof of Theorem nmo0
StepHypRef Expression
1 eqid 2090 . . . . 5
2 eqid 2090 . . . . 5
3 nmo0.0 . . . . 5
41, 2, 30oo 16705 . . . 4
5 eqid 2090 . . . . 5
6 eqid 2090 . . . . 5
7 nmo0.3 . . . . 5
81, 2, 5, 6, 7nmoval 16679 . . . 4
94, 8mpd3an3 1241 . . 3
10 df-sn 3274 . . . . 5
11 eqid 2090 . . . . . . . . . . 11
121, 11nvzcl 16526 . . . . . . . . . 10
1311, 5nvz0 16568 . . . . . . . . . . 11
14 0re 8173 . . . . . . . . . . . 12
15 1re 8172 . . . . . . . . . . . 12
16 0lt1 8516 . . . . . . . . . . . 12
1714, 15, 16ltleii 8242 . . . . . . . . . . 11
1813, 17syl6eqbr 3628 . . . . . . . . . 10
19 fveq2 4992 . . . . . . . . . . . 12
2019breq1d 3601 . . . . . . . . . . 11
2120rcla4ev 2586 . . . . . . . . . 10
2212, 18, 21syl2anc 637 . . . . . . . . 9
2322biantrurd 489 . . . . . . . 8
2423adantr 444 . . . . . . 7
25 eqid 2090 . . . . . . . . . . . . . . 15
261, 25, 30oval 16704 . . . . . . . . . . . . . 14
27263expa 1115 . . . . . . . . . . . . 13
2827fveq2d 4996 . . . . . . . . . . . 12
2925, 6nvz0 16568 . . . . . . . . . . . . 13
3029ad2antlr 702 . . . . . . . . . . . 12
3128, 30eqtrd 2122 . . . . . . . . . . 11
3231eqeq2d 2101 . . . . . . . . . 10
3332anbi2d 678 . . . . . . . . 9
3433rexbidva 2314 . . . . . . . 8
35 r19.41v 2437 . . . . . . . 8
3634, 35syl6rbb 251 . . . . . . 7
3724, 36bitrd 242 . . . . . 6
3837abbidv 2198 . . . . 5
3910, 38syl5req 2135 . . . 4
4039supeq1d 6612 . . 3
419, 40eqtrd 2122 . 2
42 0xr 8188 . . 3
43 xrltso 9362 . . . 4
4443supsn 6636 . . 3
4542, 44ax-mp 8 . 2
4641, 45syl6eq 2138 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 174   wa 357   wceq 1531   wcel 1533  cab 2077  wrex 2300  csn 3268   class class class wbr 3591  wf 4257  cfv 4261  (class class class)co 5296  csup 6606  cc0 8061  c1 8062   cle 8174  cxr 8177   clt 8178  cnv 16474  cba 16476  cn0v 16478  cnm 16480  cnmo 16657   c0o 16659
This theorem is referenced by:  0blo  16708  nmlno0lem  16709
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-rep 3677  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049  ax-cnex 8116  ax-resscn 8117  ax-1cn 8118  ax-icn 8119  ax-addcl 8120  ax-addrcl 8121  ax-mulcl 8122  ax-mulrcl 8123  ax-mulcom 8124  ax-addass 8125  ax-mulass 8126  ax-distr 8127  ax-i2m1 8128  ax-1ne0 8129  ax-1rid 8130  ax-rnegex 8131  ax-rrecex 8132  ax-cnre 8133  ax-pre-lttri 8134  ax-pre-lttrn 8135  ax-pre-ltadd 8136  ax-pre-mulgt0 8137  ax-pre-sup 8138
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1264  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-nel 2210  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-csb 2751  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-tp 3276  df-op 3277  df-uni 3435  df-iun 3511  df-br 3592  df-opab 3645  df-tr 3660  df-eprel 3844  df-id 3848  df-po 3853  df-so 3854  df-fr 3891  df-we 3893  df-ord 3934  df-on 3935  df-lim 3936  df-suc 3937  df-om 4216  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-ov 5298  df-oprab 5299  df-mpt 5461  df-mpt2 5462  df-1st 5613  df-2nd 5614  df-iota 5740  df-recs 5814  df-rdg 5849  df-er 6076  df-map 6171  df-en 6249  df-dom 6250  df-sdom 6251  df-riota 6415  df-sup 6607  df-pnf 8179  df-mnf 8180  df-xr 8181  df-ltxr 8182  df-le 8183  df-sub 8314  df-neg 8316  df-div 8542  df-n 8782  df-2 8829  df-3 8830  df-n0 8975  df-z 9026  df-uz 9222  df-rp 9440  df-seq 9775  df-exp 9830  df-cj 10086  df-re 10087  df-im 10088  df-sqr 10184  df-abs 10185  df-grpo 16192  df-gid 16193  df-ginv 16194  df-ablo 16283  df-vc 16436  df-nv 16482  df-va 16485  df-ba 16486  df-sm 16487  df-0v 16488  df-nm 16490  df-nmo 16661  df-0o 16663
Copyright terms: Public domain