Theorem relogcld 26690

Description: Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.)

Hypothesis

Ref	Expression
relogcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
relogcld	⊢ (𝜑 → (log‘𝐴) ∈ ℝ)

Proof of Theorem relogcld

Step	Hyp	Ref	Expression
1		relogcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		relogcl 26642	. 2 ⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2144  ‘cfv 6523  ℝcr 11074  ℝ⁺crp 12995  logclog 26621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-inf2 9598  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153  ax-addf 11154

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-se 5603  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-isom 6532  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-of 7662  df-om 7849  df-1st 7972  df-2nd 7973  df-supp 8143  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-1o 8439  df-2o 8440  df-er 8680  df-map 8812  df-pm 8813  df-ixp 8882  df-en 8930  df-dom 8931  df-sdom 8932  df-fin 8933  df-fsupp 9310  df-fi 9359  df-sup 9390  df-inf 9391  df-oi 9460  df-card 9899  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847  df-nn 12213  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12484  df-z 12571  df-dec 12691  df-uz 12842  df-q 12952  df-rp 12996  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13355  df-ioc 13356  df-ico 13357  df-icc 13358  df-fz 13515  df-fzo 13662  df-fl 13804  df-mod 13882  df-seq 14017  df-exp 14077  df-fac 14289  df-bc 14318  df-hash 14346  df-shft 15082  df-cj 15128  df-re 15129  df-im 15130  df-sqrt 15264  df-abs 15265  df-limsup 15500  df-clim 15517  df-rlim 15518  df-sum 15716  df-ef 16099  df-sin 16101  df-cos 16102  df-pi 16104  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17248  df-ress 17269  df-plusg 17301  df-mulr 17302  df-starv 17303  df-sca 17304  df-vsca 17305  df-ip 17306  df-tset 17307  df-ple 17308  df-ds 17310  df-unif 17311  df-hom 17312  df-cco 17313  df-rest 17453  df-topn 17454  df-0g 17472  df-gsum 17473  df-topgen 17474  df-pt 17475  df-prds 17478  df-xrs 17534  df-qtop 17539  df-imas 17540  df-xps 17542  df-mre 17616  df-mrc 17617  df-acs 17619  df-mgm 18676  df-sgrp 18755  df-mnd 18771  df-submnd 18820  df-mulg 19112  df-cntz 19359  df-cmn 19824  df-psmet 21418  df-xmet 21419  df-met 21420  df-bl 21421  df-mopn 21422  df-fbas 21423  df-fg 21424  df-cnfld 21427  df-top 22956  df-topon 22973  df-topsp 22995  df-bases 23008  df-cld 23081  df-ntr 23082  df-cls 23083  df-nei 23160  df-lp 23198  df-perf 23199  df-cn 23289  df-cnp 23290  df-haus 23377  df-tx 23624  df-hmeo 23817  df-fil 23908  df-fm 24000  df-flim 24001  df-flf 24002  df-xms 24382  df-ms 24383  df-tms 24384  df-cncf 24942  df-limc 25930  df-dv 25931  df-log 26623

This theorem is referenced by:  logcnlem3  26711  advlogexp  26722  logccv  26730  recxpcl  26742  cxpsqrt  26770  loglesqrt  26828  logbrec  26849  logbleb  26850  logblt  26851  ang180lem2  26877  isosctrlem2  26886  atanlogaddlem  26980  atantan  26990  birthdaylem2  27019  birthdaylem3  27020  amgmlem  27056  emcllem1  27062  emcllem2  27063  emcllem3  27064  emcllem4  27065  emcllem5  27066  emcllem6  27067  harmonicubnd  27076  fsumharmonic  27078  zetacvg  27081  lgamgulmlem3  27097  lgamgulmlem4  27098  lgamgulmlem5  27099  lgamgulmlem6  27100  lgamgulm2  27102  lgambdd  27103  lgamcvg2  27121  gamcvg  27122  gamcvg2lem  27125  relgamcl  27128  lgam1  27130  chtf  27174  efchtcl  27177  chtge0  27178  vmacl  27184  chtprm  27219  chtdif  27224  efchtdvds  27225  prmorcht  27244  vmalelog  27271  chtleppi  27276  chtublem  27277  fsumvma2  27280  pclogsum  27281  vmasum  27282  chpval2  27284  chpchtsum  27285  chpub  27286  logfacubnd  27287  logfaclbnd  27288  logexprlim  27291  logfacrlim2  27292  bposlem1  27350  bposlem9  27358  chebbnd1lem1  27535  chebbnd1lem2  27536  chebbnd1lem3  27537  chtppilimlem1  27539  chpchtlim  27545  vmadivsum  27548  vmadivsumb  27549  rplogsumlem1  27550  rplogsumlem2  27551  rpvmasumlem  27553  dchrvmasumlem1  27561  dchrvmasum2lem  27562  dchrvmasum2if  27563  dchrvmasumlem2  27564  dchrvmasumiflem1  27567  dchrvmasumiflem2  27568  rplogsum  27593  mulogsumlem  27597  mulogsum  27598  mulog2sumlem1  27600  mulog2sumlem2  27601  mulog2sumlem3  27602  vmalogdivsum2  27604  vmalogdivsum  27605  2vmadivsumlem  27606  logsqvma  27608  logsqvma2  27609  log2sumbnd  27610  selberglem2  27612  selbergb  27615  selberg2lem  27616  selberg2b  27618  chpdifbndlem1  27619  chpdifbndlem2  27620  logdivbnd  27622  selberg3lem1  27623  selberg3lem2  27624  selberg3  27625  selberg4lem1  27626  selberg4  27627  selberg3r  27635  selberg4r  27636  selberg34r  27637  pntsf  27639  pntsval2  27642  pntrlog2bndlem1  27643  pntrlog2bndlem2  27644  pntrlog2bndlem3  27645  pntrlog2bndlem4  27646  pntrlog2bndlem5  27647  pntrlog2bndlem6  27649  pntrlog2bnd  27650  pntpbnd1a  27651  pntpbnd2  27653  pntibndlem2  27657  pntlemb  27663  pntlemg  27664  pntlemh  27665  pntlemn  27666  pntlemr  27668  pntlemj  27669  pntlemf  27671  pntlemk  27672  pntlemo  27673  ostth2lem4  27702  ostth2  27703  ostth3  27704  argcj  32952  xrge0iifcnv  34232  xrge0iifiso  34234  xrge0iifhom  34236  hgt750lemd  34944  logdivsqrle  34946  hgt750lem  34947  hgt750lemb  34952  hgt750leme  34954  tgoldbachgtde  34956  dvrelogpow2b  42690  aks4d1p1p6  42695  aks4d1p1p7  42696  aks4d1p1p5  42697  aks4d1p6  42703  rxp112d  42959  rxp11d  42962  stirlinglem4  46656  stirlinglem11  46663  stirlinglem12  46664  stirlinglem13  46665  lighneallem2  48220  rege1logbrege0  49185  amgmwlem  50428