Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xrge0mulc1cn Unicode version

Theorem xrge0mulc1cn 23325
Description: The operation multiplying a non-negative real numbers by a non-negative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017.)
Hypotheses
Ref Expression
xrge0mulc1cn.k  |-  J  =  ( (ordTop `  <_  )t  ( 0 [,]  +oo )
)
xrge0mulc1cn.f  |-  F  =  ( x  e.  ( 0 [,]  +oo )  |->  ( x x e C ) )
xrge0mulc1cn.c  |-  ( ph  ->  C  e.  ( 0 [,)  +oo ) )
Assertion
Ref Expression
xrge0mulc1cn  |-  ( ph  ->  F  e.  ( J  Cn  J ) )
Distinct variable group:    x, C
Allowed substitution hints:    ph( x)    F( x)    J( x)

Proof of Theorem xrge0mulc1cn
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 xrge0mulc1cn.k . . . . . 6  |-  J  =  ( (ordTop `  <_  )t  ( 0 [,]  +oo )
)
2 letopon 16937 . . . . . . 7  |-  (ordTop `  <_  )  e.  (TopOn `  RR* )
3 iccssxr 10734 . . . . . . 7  |-  ( 0 [,]  +oo )  C_  RR*
4 resttopon 16894 . . . . . . 7  |-  ( ( (ordTop `  <_  )  e.  (TopOn `  RR* )  /\  ( 0 [,]  +oo )  C_  RR* )  ->  (
(ordTop `  <_  )t  ( 0 [,]  +oo ) )  e.  (TopOn `  ( 0 [,]  +oo ) ) )
52, 3, 4mp2an 653 . . . . . 6  |-  ( (ordTop `  <_  )t  ( 0 [,] 
+oo ) )  e.  (TopOn `  ( 0 [,]  +oo ) )
61, 5eqeltri 2355 . . . . 5  |-  J  e.  (TopOn `  ( 0 [,]  +oo ) )
76a1i 10 . . . 4  |-  ( C  =  0  ->  J  e.  (TopOn `  ( 0 [,]  +oo ) ) )
8 0xr 8880 . . . . . 6  |-  0  e.  RR*
9 pnfxr 10457 . . . . . 6  |-  +oo  e.  RR*
10 pnfge 10471 . . . . . . 7  |-  ( 0  e.  RR*  ->  0  <_  +oo )
118, 10ax-mp 8 . . . . . 6  |-  0  <_  +oo
12 lbicc2 10754 . . . . . 6  |-  ( ( 0  e.  RR*  /\  +oo  e.  RR*  /\  0  <_  +oo )  ->  0  e.  ( 0 [,]  +oo ) )
138, 9, 11, 12mp3an 1277 . . . . 5  |-  0  e.  ( 0 [,]  +oo )
1413a1i 10 . . . 4  |-  ( C  =  0  ->  0  e.  ( 0 [,]  +oo ) )
15 xrge0mulc1cn.f . . . . . . 7  |-  F  =  ( x  e.  ( 0 [,]  +oo )  |->  ( x x e C ) )
16 simpl 443 . . . . . . . . . . 11  |-  ( ( C  =  0  /\  x  e.  ( 0 [,]  +oo ) )  ->  C  =  0 )
1716oveq2d 5876 . . . . . . . . . 10  |-  ( ( C  =  0  /\  x  e.  ( 0 [,]  +oo ) )  -> 
( x x e C )  =  ( x x e 0 ) )
18 simpr 447 . . . . . . . . . . . 12  |-  ( ( C  =  0  /\  x  e.  ( 0 [,]  +oo ) )  ->  x  e.  ( 0 [,]  +oo ) )
193, 18sseldi 3180 . . . . . . . . . . 11  |-  ( ( C  =  0  /\  x  e.  ( 0 [,]  +oo ) )  ->  x  e.  RR* )
20 xmul01 10589 . . . . . . . . . . 11  |-  ( x  e.  RR*  ->  ( x x e 0 )  =  0 )
2119, 20syl 15 . . . . . . . . . 10  |-  ( ( C  =  0  /\  x  e.  ( 0 [,]  +oo ) )  -> 
( x x e 0 )  =  0 )
2217, 21eqtrd 2317 . . . . . . . . 9  |-  ( ( C  =  0  /\  x  e.  ( 0 [,]  +oo ) )  -> 
( x x e C )  =  0 )
2322ralrimiva 2628 . . . . . . . 8  |-  ( C  =  0  ->  A. x  e.  ( 0 [,]  +oo ) ( x x e C )  =  0 )
24 ovex 5885 . . . . . . . . . 10  |-  ( x x e C )  e.  _V
2524rgenw 2612 . . . . . . . . 9  |-  A. x  e.  ( 0 [,]  +oo ) ( x x e C )  e. 
_V
26 mpteqb 5616 . . . . . . . . 9  |-  ( A. x  e.  ( 0 [,]  +oo ) ( x x e C )  e.  _V  ->  (
( x  e.  ( 0 [,]  +oo )  |->  ( x x e C ) )  =  ( x  e.  ( 0 [,]  +oo )  |->  0 )  <->  A. x  e.  ( 0 [,]  +oo ) ( x x e C )  =  0 ) )
2725, 26ax-mp 8 . . . . . . . 8  |-  ( ( x  e.  ( 0 [,]  +oo )  |->  ( x x e C ) )  =  ( x  e.  ( 0 [,] 
+oo )  |->  0 )  <->  A. x  e.  (
0 [,]  +oo ) ( x x e C )  =  0 )
2823, 27sylibr 203 . . . . . . 7  |-  ( C  =  0  ->  (
x  e.  ( 0 [,]  +oo )  |->  ( x x e C ) )  =  ( x  e.  ( 0 [,] 
+oo )  |->  0 ) )
2915, 28syl5eq 2329 . . . . . 6  |-  ( C  =  0  ->  F  =  ( x  e.  ( 0 [,]  +oo )  |->  0 ) )
30 fconstmpt 4734 . . . . . 6  |-  ( ( 0 [,]  +oo )  X.  { 0 } )  =  ( x  e.  ( 0 [,]  +oo )  |->  0 )
3129, 30syl6eqr 2335 . . . . 5  |-  ( C  =  0  ->  F  =  ( ( 0 [,]  +oo )  X.  {
0 } ) )
328elexi 2799 . . . . . 6  |-  0  e.  _V
3332fconst2 5732 . . . . 5  |-  ( F : ( 0 [,] 
+oo ) --> { 0 }  <->  F  =  (
( 0 [,]  +oo )  X.  { 0 } ) )
3431, 33sylibr 203 . . . 4  |-  ( C  =  0  ->  F : ( 0 [,] 
+oo ) --> { 0 } )
35 cnconst 17014 . . . 4  |-  ( ( ( J  e.  (TopOn `  ( 0 [,]  +oo ) )  /\  J  e.  (TopOn `  ( 0 [,]  +oo ) ) )  /\  ( 0  e.  ( 0 [,]  +oo )  /\  F : ( 0 [,]  +oo ) --> { 0 } ) )  ->  F  e.  ( J  Cn  J
) )
367, 7, 14, 34, 35syl22anc 1183 . . 3  |-  ( C  =  0  ->  F  e.  ( J  Cn  J
) )
3736adantl 452 . 2  |-  ( (
ph  /\  C  = 
0 )  ->  F  e.  ( J  Cn  J
) )
38 eqid 2285 . . . . . . . . 9  |-  (ordTop `  <_  )  =  (ordTop `  <_  )
39 nfcv 2421 . . . . . . . . . 10  |-  F/_ y
( x x e C )
40 nfcv 2421 . . . . . . . . . 10  |-  F/_ x
( y x e C )
41 oveq1 5867 . . . . . . . . . 10  |-  ( x  =  y  ->  (
x x e C )  =  ( y x e C ) )
4239, 40, 41cbvmpt 4112 . . . . . . . . 9  |-  ( x  e.  RR*  |->  ( x x e C ) )  =  ( y  e.  RR*  |->  ( y x e C ) )
43 id 19 . . . . . . . . 9  |-  ( C  e.  RR+  ->  C  e.  RR+ )
4438, 42, 43xrmulc1cn 23305 . . . . . . . 8  |-  ( C  e.  RR+  ->  ( x  e.  RR*  |->  ( x x e C ) )  e.  ( (ordTop `  <_  )  Cn  (ordTop ` 
<_  ) ) )
452toponunii 16672 . . . . . . . . 9  |-  RR*  =  U. (ordTop `  <_  )
4645cnrest 17015 . . . . . . . 8  |-  ( ( ( x  e.  RR*  |->  ( x x e C ) )  e.  ( (ordTop `  <_  )  Cn  (ordTop `  <_  ) )  /\  ( 0 [,]  +oo )  C_  RR* )  ->  ( ( x  e. 
RR*  |->  ( x x e C ) )  |`  ( 0 [,]  +oo ) )  e.  ( ( (ordTop `  <_  )t  ( 0 [,]  +oo )
)  Cn  (ordTop `  <_  ) ) )
4744, 3, 46sylancl 643 . . . . . . 7  |-  ( C  e.  RR+  ->  ( ( x  e.  RR*  |->  ( x x e C ) )  |`  ( 0 [,]  +oo ) )  e.  ( ( (ordTop `  <_  )t  ( 0 [,]  +oo ) )  Cn  (ordTop ` 
<_  ) ) )
48 resmpt 5002 . . . . . . . . . 10  |-  ( ( 0 [,]  +oo )  C_ 
RR*  ->  ( ( x  e.  RR*  |->  ( x x e C ) )  |`  ( 0 [,]  +oo ) )  =  ( x  e.  ( 0 [,]  +oo )  |->  ( x x e C ) ) )
493, 48ax-mp 8 . . . . . . . . 9  |-  ( ( x  e.  RR*  |->  ( x x e C ) )  |`  ( 0 [,]  +oo ) )  =  ( x  e.  ( 0 [,]  +oo )  |->  ( x x e C ) )
5049, 15eqtr4i 2308 . . . . . . . 8  |-  ( ( x  e.  RR*  |->  ( x x e C ) )  |`  ( 0 [,]  +oo ) )  =  F
511eqcomi 2289 . . . . . . . . 9  |-  ( (ordTop `  <_  )t  ( 0 [,] 
+oo ) )  =  J
5251oveq1i 5870 . . . . . . . 8  |-  ( ( (ordTop `  <_  )t  ( 0 [,]  +oo ) )  Cn  (ordTop `  <_  ) )  =  ( J  Cn  (ordTop `  <_  ) )
5350, 52eleq12i 2350 . . . . . . 7  |-  ( ( ( x  e.  RR*  |->  ( x x e C ) )  |`  ( 0 [,]  +oo ) )  e.  ( ( (ordTop `  <_  )t  ( 0 [,]  +oo )
)  Cn  (ordTop `  <_  ) )  <->  F  e.  ( J  Cn  (ordTop ` 
<_  ) ) )
5447, 53sylib 188 . . . . . 6  |-  ( C  e.  RR+  ->  F  e.  ( J  Cn  (ordTop ` 
<_  ) ) )
552a1i 10 . . . . . . 7  |-  ( C  e.  RR+  ->  (ordTop `  <_  )  e.  (TopOn `  RR* ) )
56 simpr 447 . . . . . . . . . . 11  |-  ( ( C  e.  RR+  /\  x  e.  ( 0 [,]  +oo ) )  ->  x  e.  ( 0 [,]  +oo ) )
57 ioorp 10729 . . . . . . . . . . . . 13  |-  ( 0 (,)  +oo )  =  RR+
58 ioossicc 10737 . . . . . . . . . . . . 13  |-  ( 0 (,)  +oo )  C_  (
0 [,]  +oo )
5957, 58eqsstr3i 3211 . . . . . . . . . . . 12  |-  RR+  C_  (
0 [,]  +oo )
60 simpl 443 . . . . . . . . . . . 12  |-  ( ( C  e.  RR+  /\  x  e.  ( 0 [,]  +oo ) )  ->  C  e.  RR+ )
6159, 60sseldi 3180 . . . . . . . . . . 11  |-  ( ( C  e.  RR+  /\  x  e.  ( 0 [,]  +oo ) )  ->  C  e.  ( 0 [,]  +oo ) )
62 ge0xmulcl 10753 . . . . . . . . . . 11  |-  ( ( x  e.  ( 0 [,]  +oo )  /\  C  e.  ( 0 [,]  +oo ) )  ->  (
x x e C )  e.  ( 0 [,]  +oo ) )
6356, 61, 62syl2anc 642 . . . . . . . . . 10  |-  ( ( C  e.  RR+  /\  x  e.  ( 0 [,]  +oo ) )  ->  (
x x e C )  e.  ( 0 [,]  +oo ) )
6463ralrimiva 2628 . . . . . . . . 9  |-  ( C  e.  RR+  ->  A. x  e.  ( 0 [,]  +oo ) ( x x e C )  e.  ( 0 [,]  +oo ) )
6515fmpt 5683 . . . . . . . . 9  |-  ( A. x  e.  ( 0 [,]  +oo ) ( x x e C )  e.  ( 0 [,] 
+oo )  <->  F :
( 0 [,]  +oo )
--> ( 0 [,]  +oo ) )
6664, 65sylib 188 . . . . . . . 8  |-  ( C  e.  RR+  ->  F :
( 0 [,]  +oo )
--> ( 0 [,]  +oo ) )
67 frn 5397 . . . . . . . 8  |-  ( F : ( 0 [,] 
+oo ) --> ( 0 [,]  +oo )  ->  ran  F 
C_  ( 0 [,] 
+oo ) )
6866, 67syl 15 . . . . . . 7  |-  ( C  e.  RR+  ->  ran  F  C_  ( 0 [,]  +oo ) )
693a1i 10 . . . . . . 7  |-  ( C  e.  RR+  ->  ( 0 [,]  +oo )  C_  RR* )
70 cnrest2 17016 . . . . . . 7  |-  ( ( (ordTop `  <_  )  e.  (TopOn `  RR* )  /\  ran  F  C_  ( 0 [,]  +oo )  /\  (
0 [,]  +oo )  C_  RR* )  ->  ( F  e.  ( J  Cn  (ordTop ` 
<_  ) )  <->  F  e.  ( J  Cn  (
(ordTop `  <_  )t  ( 0 [,]  +oo ) ) ) ) )
7155, 68, 69, 70syl3anc 1182 . . . . . 6  |-  ( C  e.  RR+  ->  ( F  e.  ( J  Cn  (ordTop `  <_  ) )  <->  F  e.  ( J  Cn  ( (ordTop `  <_  )t  ( 0 [,]  +oo ) ) ) ) )
7254, 71mpbid 201 . . . . 5  |-  ( C  e.  RR+  ->  F  e.  ( J  Cn  (
(ordTop `  <_  )t  ( 0 [,]  +oo ) ) ) )
731oveq2i 5871 . . . . 5  |-  ( J  Cn  J )  =  ( J  Cn  (
(ordTop `  <_  )t  ( 0 [,]  +oo ) ) )
7472, 73syl6eleqr 2376 . . . 4  |-  ( C  e.  RR+  ->  F  e.  ( J  Cn  J
) )
7574, 57eleq2s 2377 . . 3  |-  ( C  e.  ( 0 (,) 
+oo )  ->  F  e.  ( J  Cn  J
) )
7675adantl 452 . 2  |-  ( (
ph  /\  C  e.  ( 0 (,)  +oo ) )  ->  F  e.  ( J  Cn  J
) )
77 xrge0mulc1cn.c . . 3  |-  ( ph  ->  C  e.  ( 0 [,)  +oo ) )
78 0re 8840 . . . . 5  |-  0  e.  RR
79 ltpnf 10465 . . . . 5  |-  ( 0  e.  RR  ->  0  <  +oo )
8078, 79ax-mp 8 . . . 4  |-  0  <  +oo
81 elicoelioo 23273 . . . 4  |-  ( ( 0  e.  RR*  /\  +oo  e.  RR*  /\  0  <  +oo )  ->  ( C  e.  ( 0 [,) 
+oo )  <->  ( C  =  0  \/  C  e.  ( 0 (,)  +oo ) ) ) )
828, 9, 80, 81mp3an 1277 . . 3  |-  ( C  e.  ( 0 [,) 
+oo )  <->  ( C  =  0  \/  C  e.  ( 0 (,)  +oo ) ) )
8377, 82sylib 188 . 2  |-  ( ph  ->  ( C  =  0  \/  C  e.  ( 0 (,)  +oo )
) )
8437, 76, 83mpjaodan 761 1  |-  ( ph  ->  F  e.  ( J  Cn  J ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1625    e. wcel 1686   A.wral 2545   _Vcvv 2790    C_ wss 3154   {csn 3642   class class class wbr 4025    e. cmpt 4079    X. cxp 4689   ran crn 4692    |` cres 4693   -->wf 5253   ` cfv 5257  (class class class)co 5860   RRcr 8738   0cc0 8739    +oocpnf 8866   RR*cxr 8868    < clt 8869    <_ cle 8870   RR+crp 10356   x ecxmu 10453   (,)cioo 10658   [,)cico 10660   [,]cicc 10661   ↾t crest 13327  ordTopcordt 13400  TopOnctopon 16634    Cn ccn 16956
This theorem is referenced by:  esummulc1  23451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-cnex 8795  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rmo 2553  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-iin 3910  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-isom 5266  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-riota 6306  df-recs 6390  df-rdg 6425  df-1o 6481  df-oadd 6485  df-er 6662  df-map 6776  df-en 6866  df-dom 6867  df-sdom 6868  df-fin 6869  df-fi 7167  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-div 9426  df-rp 10357  df-xneg 10454  df-xmul 10456  df-ioo 10662  df-ico 10664  df-icc 10665  df-rest 13329  df-topgen 13346  df-ordt 13404  df-ps 14308  df-tsr 14309  df-top 16638  df-bases 16640  df-topon 16641  df-cn 16959  df-cnp 16960
  Copyright terms: Public domain W3C validator