Theorem relogcld 26858

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 26810	. 2 ⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
3	1, 2	syl 18	1 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  ℝcr 11126  ℝ⁺crp 13044  logclog 26789

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-inf2 9623  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205  ax-addf 11206

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7681  df-om 7866  df-1st 7989  df-2nd 7990  df-supp 8162  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-2o 8459  df-er 8699  df-map 8831  df-pm 8832  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9335  df-fi 9384  df-sup 9415  df-inf 9416  df-oi 9485  df-card 9947  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899  df-nn 12261  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12532  df-z 12619  df-dec 12740  df-uz 12891  df-q 13001  df-rp 13045  df-xneg 13165  df-xadd 13166  df-xmul 13167  df-ioo 13404  df-ioc 13405  df-ico 13406  df-icc 13407  df-fz 13564  df-fzo 13712  df-fl 13855  df-mod 13933  df-seq 14068  df-exp 14128  df-fac 14340  df-bc 14369  df-hash 14397  df-shft 15142  df-cj 15188  df-re 15189  df-im 15190  df-sqrt 15324  df-abs 15325  df-limsup 15560  df-clim 15577  df-rlim 15578  df-sum 15776  df-ef 16157  df-sin 16159  df-cos 16160  df-pi 16162  df-struct 17243  df-sets 17260  df-slot 17278  df-ndx 17290  df-base 17306  df-ress 17327  df-plusg 17359  df-mulr 17360  df-starv 17361  df-sca 17362  df-vsca 17363  df-ip 17364  df-tset 17365  df-ple 17366  df-ds 17368  df-unif 17369  df-hom 17370  df-cco 17371  df-rest 17511  df-topn 17512  df-0g 17530  df-gsum 17531  df-topgen 17532  df-pt 17533  df-prds 17536  df-xrs 17592  df-qtop 17597  df-imas 17598  df-xps 17600  df-mre 17674  df-mrc 17675  df-acs 17677  df-mgm 18734  df-sgrp 18823  df-mnd 18839  df-submnd 18893  df-mulg 19192  df-cntz 19445  df-cmn 19910  df-psmet 21578  df-xmet 21579  df-met 21580  df-bl 21581  df-mopn 21582  df-fbas 21583  df-fg 21584  df-cnfld 21587  df-top 23120  df-topon 23137  df-topsp 23159  df-bases 23172  df-cld 23245  df-ntr 23246  df-cls 23247  df-nei 23324  df-lp 23362  df-perf 23363  df-cn 23453  df-cnp 23454  df-haus 23541  df-tx 23789  df-hmeo 23982  df-fil 24073  df-fm 24165  df-flim 24166  df-flf 24167  df-xms 24547  df-ms 24548  df-tms 24549  df-cncf 25107  df-limc 26095  df-dv 26096  df-log 26791

This theorem is used by:  logcnlem3  26879  advlogexp  26890  logccv  26898  recxpcl  26910  cxpsqrt  26938  loglesqrt  26996  logbrec  27017  logbleb  27018  logblt  27019  ang180lem2  27045  isosctrlem2  27054  atanlogaddlem  27148  atantan  27158  birthdaylem2  27187  birthdaylem3  27188  amgmlem  27224  emcllem1  27230  emcllem2  27231  emcllem3  27232  emcllem4  27233  emcllem5  27234  emcllem6  27235  harmonicubnd  27244  fsumharmonic  27246  zetacvg  27249  lgamgulmlem3  27265  lgamgulmlem4  27266  lgamgulmlem5  27267  lgamgulmlem6  27268  lgamgulm2  27270  lgambdd  27271  lgamcvg2  27289  gamcvg  27290  gamcvg2lem  27293  relgamcl  27296  lgam1  27298  chtf  27342  efchtcl  27345  chtge0  27346  vmacl  27352  chtprm  27387  chtdif  27392  efchtdvds  27393  prmorcht  27412  vmalelog  27439  chtleppi  27444  chtublem  27445  fsumvma2  27448  pclogsum  27449  vmasum  27450  chpval2  27452  chpchtsum  27453  chpub  27454  logfacubnd  27455  logfaclbnd  27456  logexprlim  27459  logfacrlim2  27460  bposlem1  27518  bposlem9  27526  chebbnd1lem1  27703  chebbnd1lem2  27704  chebbnd1lem3  27705  chtppilimlem1  27707  chpchtlim  27713  vmadivsum  27716  vmadivsumb  27717  rplogsumlem1  27718  rplogsumlem2  27719  rpvmasumlem  27721  dchrvmasumlem1  27729  dchrvmasum2lem  27730  dchrvmasum2if  27731  dchrvmasumlem2  27732  dchrvmasumiflem1  27735  dchrvmasumiflem2  27736  rplogsum  27761  mulogsumlem  27765  mulogsum  27766  mulog2sumlem1  27768  mulog2sumlem2  27769  mulog2sumlem3  27770  vmalogdivsum2  27772  vmalogdivsum  27773  2vmadivsumlem  27774  logsqvma  27776  logsqvma2  27777  log2sumbnd  27778  selberglem2  27780  selbergb  27783  selberg2lem  27784  selberg2b  27786  chpdifbndlem1  27787  chpdifbndlem2  27788  logdivbnd  27790  selberg3lem1  27791  selberg3lem2  27792  selberg3  27793  selberg4lem1  27794  selberg4  27795  selberg3r  27803  selberg4r  27804  selberg34r  27805  pntsf  27807  pntsval2  27810  pntrlog2bndlem1  27811  pntrlog2bndlem2  27812  pntrlog2bndlem3  27813  pntrlog2bndlem4  27814  pntrlog2bndlem5  27815  pntrlog2bndlem6  27817  pntrlog2bnd  27818  pntpbnd1a  27819  pntpbnd2  27821  pntibndlem2  27825  pntlemb  27831  pntlemg  27832  pntlemh  27833  pntlemn  27834  pntlemr  27836  pntlemj  27837  pntlemf  27839  pntlemk  27840  pntlemo  27841  ostth2lem4  27870  ostth2  27871  ostth3  27872  argcj  33206  xrge0iifcnv  34430  xrge0iifiso  34432  xrge0iifhom  34434  hgt750lemd  35143  logdivsqrle  35145  hgt750lem  35146  hgt750lemb  35151  hgt750leme  35153  tgoldbachgtde  35155  dvrelogpow2b  42921  aks4d1p1p6  42926  aks4d1p1p7  42927  aks4d1p1p5  42928  aks4d1p6  42934  rxp112d  43207  rxp11d  43210  stirlinglem4  46892  stirlinglem11  46899  stirlinglem12  46900  stirlinglem13  46901  lighneallem2  48496  rege1logbrege0  49475  amgmwlem  50807