Theorem logcld 25276

Description: The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 25274. (Contributed by David Moews, 28-Feb-2017.)

Hypotheses

Ref	Expression
logcld.1	⊢ (𝜑 → 𝑋 ∈ ℂ)
logcld.2	⊢ (𝜑 → 𝑋 ≠ 0)

Assertion

Ref	Expression
logcld	⊢ (𝜑 → (log‘𝑋) ∈ ℂ)

Proof of Theorem logcld

Step	Hyp	Ref	Expression
1		logcld.1	. 2 ⊢ (𝜑 → 𝑋 ∈ ℂ)
2		logcld.2	. 2 ⊢ (𝜑 → 𝑋 ≠ 0)
3		logcl 25274	. 2 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (log‘𝑋) ∈ ℂ)
4	1, 2, 3	syl2anc 587	1 ⊢ (𝜑 → (log‘𝑋) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2112   ≠ wne 2952  ‘cfv 6341  ℂcc 10587  0cc0 10589  logclog 25260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-inf2 9151  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666  ax-pre-sup 10667  ax-addf 10668  ax-mulf 10669

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-int 4843  df-iun 4889  df-iin 4890  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-se 5489  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-isom 6350  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-of 7412  df-om 7587  df-1st 7700  df-2nd 7701  df-supp 7843  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-1o 8119  df-2o 8120  df-er 8306  df-map 8425  df-pm 8426  df-ixp 8494  df-en 8542  df-dom 8543  df-sdom 8544  df-fin 8545  df-fsupp 8881  df-fi 8922  df-sup 8953  df-inf 8954  df-oi 9021  df-card 9415  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-div 11350  df-nn 11689  df-2 11751  df-3 11752  df-4 11753  df-5 11754  df-6 11755  df-7 11756  df-8 11757  df-9 11758  df-n0 11949  df-z 12035  df-dec 12152  df-uz 12297  df-q 12403  df-rp 12445  df-xneg 12562  df-xadd 12563  df-xmul 12564  df-ioo 12797  df-ioc 12798  df-ico 12799  df-icc 12800  df-fz 12954  df-fzo 13097  df-fl 13225  df-mod 13301  df-seq 13433  df-exp 13494  df-fac 13698  df-bc 13727  df-hash 13755  df-shft 14488  df-cj 14520  df-re 14521  df-im 14522  df-sqrt 14656  df-abs 14657  df-limsup 14890  df-clim 14907  df-rlim 14908  df-sum 15105  df-ef 15483  df-sin 15485  df-cos 15486  df-pi 15488  df-struct 16558  df-ndx 16559  df-slot 16560  df-base 16562  df-sets 16563  df-ress 16564  df-plusg 16651  df-mulr 16652  df-starv 16653  df-sca 16654  df-vsca 16655  df-ip 16656  df-tset 16657  df-ple 16658  df-ds 16660  df-unif 16661  df-hom 16662  df-cco 16663  df-rest 16769  df-topn 16770  df-0g 16788  df-gsum 16789  df-topgen 16790  df-pt 16791  df-prds 16794  df-xrs 16848  df-qtop 16853  df-imas 16854  df-xps 16856  df-mre 16930  df-mrc 16931  df-acs 16933  df-mgm 17933  df-sgrp 17982  df-mnd 17993  df-submnd 18038  df-mulg 18307  df-cntz 18529  df-cmn 18990  df-psmet 20173  df-xmet 20174  df-met 20175  df-bl 20176  df-mopn 20177  df-fbas 20178  df-fg 20179  df-cnfld 20182  df-top 21609  df-topon 21626  df-topsp 21648  df-bases 21661  df-cld 21734  df-ntr 21735  df-cls 21736  df-nei 21813  df-lp 21851  df-perf 21852  df-cn 21942  df-cnp 21943  df-haus 22030  df-tx 22277  df-hmeo 22470  df-fil 22561  df-fm 22653  df-flim 22654  df-flf 22655  df-xms 23037  df-ms 23038  df-tms 23039  df-cncf 23594  df-limc 24580  df-dv 24581  df-log 25262

This theorem is referenced by:  logimclad  25278  eflogeq  25307  cosargd  25313  logcnlem3  25349  logcnlem4  25350  logcnlem5  25351  logcn  25352  dvloglem  25353  logf1o2  25355  logtayl  25365  logtayl2  25367  mulcxp  25390  dvcncxp1  25446  cxpeq  25460  logrec  25463  logbcl  25467  logb1  25469  relogbreexp  25475  nnlogbexp  25481  logbrec  25482  ang180lem1  25509  ang180lem2  25510  ang180lem3  25511  ang180lem4  25512  lawcos  25516  isosctrlem1  25518  isosctrlem2  25519  asinf  25572  atanf  25580  asinneg  25586  efiasin  25588  asinbnd  25599  atanneg  25607  atancj  25610  efiatan  25612  atanlogaddlem  25613  atanlogadd  25614  atanlogsublem  25615  atanlogsub  25616  efiatan2  25617  2efiatan  25618  atantan  25623  atanbndlem  25625  dvatan  25635  atantayl  25637  efrlim  25669  lgamgulmlem2  25729  lgamgulmlem3  25730  lgamgulmlem5  25732  lgamgulmlem6  25733  lgamgulm2  25735  lgambdd  25736  lgamcvg2  25754  gamcvg  25755  gamp1  25757  gamcvg2lem  25758  hgt750lemd  32161  logdivsqrle  32163  hgt750lemb  32169  iprodgam  33237  dvasin  35457  aks4d1p1p1  39665  dvrelog2  39666  dvrelog3  39667  dvrelog2b  39668  dvrelogpow2b  39670  aks4d1p1p6  39675  aks4d1p1p7  39676  aks4d1p1p5  39677  isosctrlem1ALT  42059  stirlinglem4  43131  stirlinglem5  43132  stirlinglem7  43134  stirlinglem12  43139  stirlinglem14  43141