Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  blocnilem Structured version   Visualization version   Unicode version

Theorem blocnilem 26457
 Description: Lemma for blocni 26458 and lnocni 26459. If a linear operator is continuous at any point, it is bounded. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
blocni.8
blocni.d
blocni.j
blocni.k
blocni.4
blocni.5
blocni.u
blocni.w
blocni.l
blocnilem.1
Assertion
Ref Expression
blocnilem

Proof of Theorem blocnilem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 blocni.u . . . . . 6
2 blocnilem.1 . . . . . . 7
3 blocni.8 . . . . . . 7
42, 3imsxmet 26336 . . . . . 6
51, 4ax-mp 5 . . . . 5
6 blocni.w . . . . . 6
7 eqid 2453 . . . . . . 7
8 blocni.d . . . . . . 7
97, 8imsxmet 26336 . . . . . 6
106, 9ax-mp 5 . . . . 5
11 1rp 11313 . . . . . 6
12 blocni.j . . . . . . 7
13 blocni.k . . . . . . 7
1412, 13metcnpi3 21573 . . . . . 6
1511, 14mpanr2 691 . . . . 5
165, 10, 15mpanl12 689 . . . 4
17 rpreccl 11333 . . . . . . . . 9
1817rpred 11348 . . . . . . . 8
1918ad2antlr 734 . . . . . . 7
20 eqid 2453 . . . . . . . . . . . . . . . 16
21 eqid 2453 . . . . . . . . . . . . . . . 16 CV CV
222, 20, 21, 3imsdval 26330 . . . . . . . . . . . . . . 15 CV
231, 22mp3an1 1353 . . . . . . . . . . . . . 14 CV
2423breq1d 4415 . . . . . . . . . . . . 13 CV
25 blocni.l . . . . . . . . . . . . . . . . . 18
26 blocni.4 . . . . . . . . . . . . . . . . . . 19
272, 7, 26lnof 26408 . . . . . . . . . . . . . . . . . 18
281, 6, 25, 27mp3an 1366 . . . . . . . . . . . . . . . . 17
2928ffvelrni 6026 . . . . . . . . . . . . . . . 16
3028ffvelrni 6026 . . . . . . . . . . . . . . . 16
31 eqid 2453 . . . . . . . . . . . . . . . . . 18
32 eqid 2453 . . . . . . . . . . . . . . . . . 18 CV CV
337, 31, 32, 8imsdval 26330 . . . . . . . . . . . . . . . . 17 CV
346, 33mp3an1 1353 . . . . . . . . . . . . . . . 16 CV
3529, 30, 34syl2an 480 . . . . . . . . . . . . . . 15 CV
361, 6, 253pm3.2i 1187 . . . . . . . . . . . . . . . . 17
372, 20, 31, 26lnosub 26412 . . . . . . . . . . . . . . . . 17
3836, 37mpan 677 . . . . . . . . . . . . . . . 16
3938fveq2d 5874 . . . . . . . . . . . . . . 15 CV CV
4035, 39eqtr4d 2490 . . . . . . . . . . . . . 14 CV
4140breq1d 4415 . . . . . . . . . . . . 13 CV
4224, 41imbi12d 322 . . . . . . . . . . . 12 CV CV
4342ancoms 455 . . . . . . . . . . 11 CV CV
4443adantlr 722 . . . . . . . . . 10 CV CV
4544ralbidva 2826 . . . . . . . . 9 CV CV
46 fveq2 5870 . . . . . . . . . . . . . 14
4746fveq2d 5874 . . . . . . . . . . . . 13 CV CV
48 fveq2 5870 . . . . . . . . . . . . . 14 CV CV
4948oveq2d 6311 . . . . . . . . . . . . 13 CV CV
5047, 49breq12d 4418 . . . . . . . . . . . 12 CV CV CV CV
511a1i 11 . . . . . . . . . . . . . . . . . . . . 21
52 simpll 761 . . . . . . . . . . . . . . . . . . . . 21
53 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . 24
542, 21nvcl 26300 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 CV
551, 54mpan 677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 CV
5655adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 CV
57 eqid 2453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
582, 57, 21nvgt0 26316 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 CV
591, 58mpan 677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 CV
6059biimpa 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 CV
6156, 60elrpd 11345 . . . . . . . . . . . . . . . . . . . . . . . 24 CV
62 rpdivcl 11332 . . . . . . . . . . . . . . . . . . . . . . . 24 CV CV
6353, 61, 62syl2an 480 . . . . . . . . . . . . . . . . . . . . . . 23 CV
6463rpcnd 11350 . . . . . . . . . . . . . . . . . . . . . 22 CV
65 simprl 765 . . . . . . . . . . . . . . . . . . . . . 22
66 eqid 2453 . . . . . . . . . . . . . . . . . . . . . . 23
672, 66nvscl 26259 . . . . . . . . . . . . . . . . . . . . . 22 CV CV
6851, 64, 65, 67syl3anc 1269 . . . . . . . . . . . . . . . . . . . . 21 CV
69 eqid 2453 . . . . . . . . . . . . . . . . . . . . . 22
702, 69, 20nvpncan2 26289 . . . . . . . . . . . . . . . . . . . . 21 CV CV CV
7151, 52, 68, 70syl3anc 1269 . . . . . . . . . . . . . . . . . . . 20 CV CV
7271fveq2d 5874 . . . . . . . . . . . . . . . . . . 19 CV CV CV CV
7363rprege0d 11355 . . . . . . . . . . . . . . . . . . . 20 CV CV
742, 66, 21nvsge0 26304 . . . . . . . . . . . . . . . . . . . 20 CV CV CV CV CV CV
7551, 73, 65, 74syl3anc 1269 . . . . . . . . . . . . . . . . . . 19 CV CV CV CV
76 rpcn 11317 . . . . . . . . . . . . . . . . . . . . 21
7776ad2antlr 734 . . . . . . . . . . . . . . . . . . . 20
7855ad2antrl 735 . . . . . . . . . . . . . . . . . . . . 21 CV
7978recnd 9674 . . . . . . . . . . . . . . . . . . . 20 CV
802, 57, 21nvz 26310 . . . . . . . . . . . . . . . . . . . . . . . 24 CV
811, 80mpan 677 . . . . . . . . . . . . . . . . . . . . . . 23 CV
8281necon3bid 2670 . . . . . . . . . . . . . . . . . . . . . 22 CV
8382biimpar 488 . . . . . . . . . . . . . . . . . . . . 21 CV
8483adantl 468 . . . . . . . . . . . . . . . . . . . 20 CV
8577, 79, 84divcan1d 10391 . . . . . . . . . . . . . . . . . . 19 CV CV
8672, 75, 853eqtrd 2491 . . . . . . . . . . . . . . . . . 18 CV CV
87 rpre 11315 . . . . . . . . . . . . . . . . . . . 20
8887leidd 10187 . . . . . . . . . . . . . . . . . . 19
8988ad2antlr 734 . . . . . . . . . . . . . . . . . 18
9086, 89eqbrtrd 4426 . . . . . . . . . . . . . . . . 17 CV CV
912, 69nvgcl 26251 . . . . . . . . . . . . . . . . . . 19 CV CV
9251, 52, 68, 91syl3anc 1269 . . . . . . . . . . . . . . . . . 18 CV
93 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . 22 CV CV
9493fveq2d 5874 . . . . . . . . . . . . . . . . . . . . 21 CV CV CV CV
9594breq1d 4415 . . . . . . . . . . . . . . . . . . . 20 CV CV CV CV
9693fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . 22 CV CV
9796fveq2d 5874 . . . . . . . . . . . . . . . . . . . . 21 CV CV CV CV
9897breq1d 4415 . . . . . . . . . . . . . . . . . . . 20 CV CV CV CV
9995, 98imbi12d 322 . . . . . . . . . . . . . . . . . . 19 CV CV CV CV CV CV CV
10099rspcv 3148 . . . . . . . . . . . . . . . . . 18 CV CV CV CV CV CV CV
10192, 100syl 17 . . . . . . . . . . . . . . . . 17 CV CV CV CV CV CV
10290, 101mpid 42 . . . . . . . . . . . . . . . 16 CV CV CV CV
10328ffvelrni 6026 . . . . . . . . . . . . . . . . . . . 20
1047, 32nvcl 26300 . . . . . . . . . . . . . . . . . . . 20 CV
1056, 103, 104sylancr 670 . . . . . . . . . . . . . . . . . . 19 CV
106105ad2antrl 735 . . . . . . . . . . . . . . . . . 18 CV
107 1red 9663 . . . . . . . . . . . . . . . . . 18
108106, 107, 63lemuldiv2d 11395 . . . . . . . . . . . . . . . . 17 CV CV CV CV
10971fveq2d 5874 . . . . . . . . . . . . . . . . . . . . 21 CV CV
110 eqid 2453 . . . . . . . . . . . . . . . . . . . . . . . 24
1112, 66, 110, 26lnomul 26413 . . . . . . . . . . . . . . . . . . . . . . 23 CV CV CV
11236, 111mpan 677 . . . . . . . . . . . . . . . . . . . . . 22 CV CV CV
11364, 65, 112syl2anc 667 . . . . . . . . . . . . . . . . . . . . 21 CV CV
114109, 113eqtrd 2487 . . . . . . . . . . . . . . . . . . . 20 CV CV
115114fveq2d 5874 . . . . . . . . . . . . . . . . . . 19 CV CV CV CV
1166a1i 11 . . . . . . . . . . . . . . . . . . . 20
117103ad2antrl 735 . . . . . . . . . . . . . . . . . . . 20
1187, 110, 32nvsge0 26304 . . . . . . . . . . . . . . . . . . . 20 CV CV CV CV CV CV
119116, 73, 117, 118syl3anc 1269 . . . . . . . . . . . . . . . . . . 19 CV CV CV CV
120115, 119eqtrd 2487 . . . . . . . . . . . . . . . . . 18 CV CV CV CV
121120breq1d 4415 . . . . . . . . . . . . . . . . 17 CV CV CV CV
122 rpcnne0 11326 . . . . . . . . . . . . . . . . . . . . 21
123 rpcnne0 11326 . . . . . . . . . . . . . . . . . . . . 21 CV CV CV
124 recdiv 10320 . . . . . . . . . . . . . . . . . . . . 21 CV CV CV CV
125122, 123, 124syl2an 480 . . . . . . . . . . . . . . . . . . . 20 CV CV CV
12653, 61, 125syl2an 480 . . . . . . . . . . . . . . . . . . 19 CV CV
127 rpne0 11324 . . . . . . . . . . . . . . . . . . . . 21
128127ad2antlr 734 . . . . . . . . . . . . . . . . . . . 20
12979, 77, 128divrec2d 10394 . . . . . . . . . . . . . . . . . . 19 CV CV
130126, 129eqtr2d 2488 . . . . . . . . . . . . . . . . . 18 CV CV
131130breq2d 4417 . . . . . . . . . . . . . . . . 17 CV CV CV CV
132108, 121, 1313bitr4d 289 . . . . . . . . . . . . . . . 16 CV CV CV CV
133102, 132sylibd 218 . . . . . . . . . . . . . . 15 CV CV CV CV
134133anassrs 654 . . . . . . . . . . . . . 14 CV CV CV CV
135134imp 431 . . . . . . . . . . . . 13 CV CV CV CV
136135an32s 814 . . . . . . . . . . . 12 CV CV CV CV
137 eqid 2453 . . . . . . . . . . . . . . . . . . 19
1382, 7, 57, 137, 26lno0 26409 . . . . . . . . . . . . . . . . . 18
1391, 6, 25, 138mp3an 1366 . . . . . . . . . . . . . . . . 17
140139fveq2i 5873 . . . . . . . . . . . . . . . 16 CV CV
141137, 32nvz0 26309 . . . . . . . . . . . . . . . . 17 CV
1426, 141ax-mp 5 . . . . . . . . . . . . . . . 16 CV
143140, 142eqtri 2475 . . . . . . . . . . . . . . 15 CV
144 0le0 10706 . . . . . . . . . . . . . . 15
145143, 144eqbrtri 4425 . . . . . . . . . . . . . 14 CV
14617rpcnd 11350 . . . . . . . . . . . . . . 15
14757, 21nvz0 26309 . . . . . . . . . . . . . . . . . 18 CV
1481, 147ax-mp 5 . . . . . . . . . . . . . . . . 17 CV
149148oveq2i 6306 . . . . . . . . . . . . . . . 16 CV
150 mul01 9817 . . . . . . . . . . . . . . . 16
151149, 150syl5eq 2499 . . . . . . . . . . . . . . 15 CV
152146, 151syl 17 . . . . . . . . . . . . . 14 CV
153145, 152syl5breqr 4442 . . . . . . . . . . . . 13 CV CV
154153ad3antlr 738 . . . . . . . . . . . 12 CV CV CV CV
15550, 136, 154pm2.61ne 2711 . . . . . . . . . . 11 CV CV CV CV
156155ex 436 . . . . . . . . . 10 CV CV CV CV
157156ralrimdva 2808 . . . . . . . . 9 CV CV CV CV
15845, 157sylbid 219 . . . . . . . 8 CV CV
159158imp 431 . . . . . . 7 CV CV
160 oveq1 6302 . . . . . . . . . 10 CV CV
161160breq2d 4417 . . . . . . . . 9 CV CV CV CV
162161ralbidv 2829 . . . . . . . 8 CV CV CV CV
163162rspcev 3152 . . . . . . 7 CV CV CV CV
16419, 159, 163syl2anc 667 . . . . . 6 CV CV
165164ex 436 . . . . 5 CV CV
166165rexlimdva 2881 . . . 4 CV CV
16716, 166syl5 33 . . 3 CV CV
168167imp 431 . 2 CV CV
169 blocni.5 . . . 4
1702, 21, 32, 26, 169, 1, 6isblo3i 26454 . . 3 CV CV
17125, 170mpbiran 930 . 2 CV CV
172168, 171sylibr 216 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 986   wceq 1446   wcel 1889   wne 2624  wral 2739  wrex 2740   class class class wbr 4405  wf 5581  cfv 5585  (class class class)co 6295  cc 9542  cr 9543  cc0 9544  c1 9545   cmul 9549   clt 9680   cle 9681   cdiv 10276  crp 11309  cxmt 18967  cmopn 18972   ccnp 20253  cnv 26215  cpv 26216  cba 26217  cns 26218  cn0v 26219  cnsb 26220  CVcnmcv 26221  cims 26222   clno 26393   cblo 26395 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-cnex 9600  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621  ax-pre-sup 9622  ax-addf 9623  ax-mulf 9624 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-er 7368  df-map 7479  df-en 7575  df-dom 7576  df-sdom 7577  df-sup 7961  df-inf 7962  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-n0 10877  df-z 10945  df-uz 11167  df-q 11272  df-rp 11310  df-xneg 11416  df-xadd 11417  df-xmul 11418  df-seq 12221  df-exp 12280  df-cj 13174  df-re 13175  df-im 13176  df-sqrt 13310  df-abs 13311  df-topgen 15354  df-psmet 18974  df-xmet 18975  df-met 18976  df-bl 18977  df-mopn 18978  df-top 19933  df-bases 19934  df-topon 19935  df-cnp 20256  df-grpo 25931  df-gid 25932  df-ginv 25933  df-gdiv 25934  df-ablo 26022  df-vc 26177  df-nv 26223  df-va 26226  df-ba 26227  df-sm 26228  df-0v 26229  df-vs 26230  df-nmcv 26231  df-ims 26232  df-lno 26397  df-nmoo 26398  df-blo 26399  df-0o 26400 This theorem is referenced by:  blocni  26458  lnocni  26459
 Copyright terms: Public domain W3C validator