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

Theorem relogcl 19928
Description: Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
Assertion
Ref Expression
relogcl  |-  ( A  e.  RR+  ->  ( log `  A )  e.  RR )

Proof of Theorem relogcl
StepHypRef Expression
1 fvres 5503 . 2  |-  ( A  e.  RR+  ->  ( ( log  |`  RR+ ) `  A )  =  ( log `  A ) )
2 relogf1o 19920 . . . 4  |-  ( log  |`  RR+ ) : RR+ -1-1-onto-> RR
3 f1of 5438 . . . 4  |-  ( ( log  |`  RR+ ) :
RR+
-1-1-onto-> RR  ->  ( log  |`  RR+ ) : RR+ --> RR )
42, 3ax-mp 8 . . 3  |-  ( log  |`  RR+ ) : RR+ --> RR
54ffvelrni 5626 . 2  |-  ( A  e.  RR+  ->  ( ( log  |`  RR+ ) `  A )  e.  RR )
61, 5eqeltrrd 2359 1  |-  ( A  e.  RR+  ->  ( log `  A )  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1685    |` cres 4690   -->wf 5217   -1-1-onto->wf1o 5220   ` cfv 5221   RRcr 8732   RR+crp 10350   logclog 19908
This theorem is referenced by:  logneg  19937  lognegb  19939  relogoprlem  19940  reexplog  19944  relogexp  19945  logfac  19950  logleb  19953  rplogcl  19954  logdivlti  19967  logdivlt  19968  logdivle  19969  relogcld  19970  advlog  19997  advlogexp  19998  logccv  20006  logcxp  20012  rpcxpcl  20019  cxpmul  20031  abscxp  20035  cxple2  20040  logsqr  20047  dvcxp1  20078  dvcxp2  20079  loglesqr  20094  log2ub  20241  birthday  20245  cxploglim  20268  cxploglim2  20269  amgmlem  20280  logdifbnd  20284  emcllem7  20291  emre  20295  emgt0  20296  harmonicbnd3  20297  harmoniclbnd  20298  harmonicbnd4  20300  cht2  20406  chtleppi  20445  chtublem  20446  chtub  20447  logfacubnd  20456  logfaclbnd  20457  logfacbnd3  20458  logfacrlim  20459  logexprlim  20460  efexple  20516  bposlem6  20524  bposlem7  20525  bposlem8  20526  bposlem9  20527  chebbnd1lem3  20616  chebbnd1  20617  chto1ub  20621  vmadivsum  20627  rpvmasumlem  20632  dchrvmasumlem2  20643  dchrvmasumlema  20645  dchrvmasumiflem1  20646  dchrvmasumiflem2  20647  dchrisum0fno1  20656  rpvmasum2  20657  dchrisum0re  20658  rpvmasum  20671  rplogsum  20672  dirith2  20673  logdivsum  20678  mulog2sumlem2  20680  mulog2sumlem3  20681  logsqvma  20687  log2sumbnd  20689  selberglem1  20690  selberglem2  20691  selberglem3  20692  selberg  20693  selberg2lem  20695  selberg2  20696  pntrsumo1  20710  selbergr  20713  pntrlog2bndlem4  20725  pntibndlem3  20737  reglogcl  26386  reglogltb  26387  reglogleb  26388  reglogmul  26389  reglogexp  26390  reglogbas  26391  reglog1  26392  stirlinglem12  27245  stirlinglem13  27246  stirlinglem14  27247
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-inf2 7338  ax-cnex 8789  ax-resscn 8790  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-mulcom 8797  ax-addass 8798  ax-mulass 8799  ax-distr 8800  ax-i2m1 8801  ax-1ne0 8802  ax-1rid 8803  ax-rnegex 8804  ax-rrecex 8805  ax-cnre 8806  ax-pre-lttri 8807  ax-pre-lttrn 8808  ax-pre-ltadd 8809  ax-pre-mulgt0 8810  ax-pre-sup 8811  ax-addf 8812  ax-mulf 8813
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 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rmo 2552  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-int 3864  df-iun 3908  df-iin 3909  df-br 4025  df-opab 4079  df-mpt 4080  df-tr 4115  df-eprel 4304  df-id 4308  df-po 4313  df-so 4314  df-fr 4351  df-se 4352  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-isom 5230  df-ov 5823  df-oprab 5824  df-mpt2 5825  df-of 6040  df-1st 6084  df-2nd 6085  df-iota 6253  df-riota 6300  df-recs 6384  df-rdg 6419  df-1o 6475  df-2o 6476  df-oadd 6479  df-er 6656  df-map 6770  df-pm 6771  df-ixp 6814  df-en 6860  df-dom 6861  df-sdom 6862  df-fin 6863  df-fi 7161  df-sup 7190  df-oi 7221  df-card 7568  df-cda 7790  df-pnf 8865  df-mnf 8866  df-xr 8867  df-ltxr 8868  df-le 8869  df-sub 9035  df-neg 9036  df-div 9420  df-nn 9743  df-2 9800  df-3 9801  df-4 9802  df-5 9803  df-6 9804  df-7 9805  df-8 9806  df-9 9807  df-10 9808  df-n0 9962  df-z 10021  df-dec 10121  df-uz 10227  df-q 10313  df-rp 10351  df-xneg 10448  df-xadd 10449  df-xmul 10450  df-ioo 10656  df-ioc 10657  df-ico 10658  df-icc 10659  df-fz 10779  df-fzo 10867  df-fl 10921  df-mod 10970  df-seq 11043  df-exp 11101  df-fac 11285  df-bc 11312  df-hash 11334  df-shft 11558  df-cj 11580  df-re 11581  df-im 11582  df-sqr 11716  df-abs 11717  df-limsup 11941  df-clim 11958  df-rlim 11959  df-sum 12155  df-ef 12345  df-sin 12347  df-cos 12348  df-pi 12350  df-struct 13146  df-ndx 13147  df-slot 13148  df-base 13149  df-sets 13150  df-ress 13151  df-plusg 13217  df-mulr 13218  df-starv 13219  df-sca 13220  df-vsca 13221  df-tset 13223  df-ple 13224  df-ds 13226  df-hom 13228  df-cco 13229  df-rest 13323  df-topn 13324  df-topgen 13340  df-pt 13341  df-prds 13344  df-xrs 13399  df-0g 13400  df-gsum 13401  df-qtop 13406  df-imas 13407  df-xps 13409  df-mre 13484  df-mrc 13485  df-acs 13487  df-mnd 14363  df-submnd 14412  df-mulg 14488  df-cntz 14789  df-cmn 15087  df-xmet 16369  df-met 16370  df-bl 16371  df-mopn 16372  df-cnfld 16374  df-top 16632  df-bases 16634  df-topon 16635  df-topsp 16636  df-cld 16752  df-ntr 16753  df-cls 16754  df-nei 16831  df-lp 16864  df-perf 16865  df-cn 16953  df-cnp 16954  df-haus 17039  df-tx 17253  df-hmeo 17442  df-fbas 17516  df-fg 17517  df-fil 17537  df-fm 17629  df-flim 17630  df-flf 17631  df-xms 17881  df-ms 17882  df-tms 17883  df-cncf 18378  df-limc 19212  df-dv 19213  df-log 19910
  Copyright terms: Public domain W3C validator