![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > logcld | Structured version Visualization version GIF version |
Description: The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 25924. (Contributed by David Moews, 28-Feb-2017.) |
Ref | Expression |
---|---|
logcld.1 | ⊢ (𝜑 → 𝑋 ∈ ℂ) |
logcld.2 | ⊢ (𝜑 → 𝑋 ≠ 0) |
Ref | Expression |
---|---|
logcld | ⊢ (𝜑 → (log‘𝑋) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | logcld.1 | . 2 ⊢ (𝜑 → 𝑋 ∈ ℂ) | |
2 | logcld.2 | . 2 ⊢ (𝜑 → 𝑋 ≠ 0) | |
3 | logcl 25924 | . 2 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (log‘𝑋) ∈ ℂ) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (log‘𝑋) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ≠ wne 2943 ‘cfv 6496 ℂcc 11049 0cc0 11051 logclog 25910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129 ax-addf 11130 ax-mulf 11131 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-supp 8093 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-2o 8413 df-er 8648 df-map 8767 df-pm 8768 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9306 df-fi 9347 df-sup 9378 df-inf 9379 df-oi 9446 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-5 12219 df-6 12220 df-7 12221 df-8 12222 df-9 12223 df-n0 12414 df-z 12500 df-dec 12619 df-uz 12764 df-q 12874 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13268 df-ioc 13269 df-ico 13270 df-icc 13271 df-fz 13425 df-fzo 13568 df-fl 13697 df-mod 13775 df-seq 13907 df-exp 13968 df-fac 14174 df-bc 14203 df-hash 14231 df-shft 14952 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-limsup 15353 df-clim 15370 df-rlim 15371 df-sum 15571 df-ef 15950 df-sin 15952 df-cos 15953 df-pi 15955 df-struct 17019 df-sets 17036 df-slot 17054 df-ndx 17066 df-base 17084 df-ress 17113 df-plusg 17146 df-mulr 17147 df-starv 17148 df-sca 17149 df-vsca 17150 df-ip 17151 df-tset 17152 df-ple 17153 df-ds 17155 df-unif 17156 df-hom 17157 df-cco 17158 df-rest 17304 df-topn 17305 df-0g 17323 df-gsum 17324 df-topgen 17325 df-pt 17326 df-prds 17329 df-xrs 17384 df-qtop 17389 df-imas 17390 df-xps 17392 df-mre 17466 df-mrc 17467 df-acs 17469 df-mgm 18497 df-sgrp 18546 df-mnd 18557 df-submnd 18602 df-mulg 18873 df-cntz 19097 df-cmn 19564 df-psmet 20788 df-xmet 20789 df-met 20790 df-bl 20791 df-mopn 20792 df-fbas 20793 df-fg 20794 df-cnfld 20797 df-top 22243 df-topon 22260 df-topsp 22282 df-bases 22296 df-cld 22370 df-ntr 22371 df-cls 22372 df-nei 22449 df-lp 22487 df-perf 22488 df-cn 22578 df-cnp 22579 df-haus 22666 df-tx 22913 df-hmeo 23106 df-fil 23197 df-fm 23289 df-flim 23290 df-flf 23291 df-xms 23673 df-ms 23674 df-tms 23675 df-cncf 24241 df-limc 25230 df-dv 25231 df-log 25912 |
This theorem is referenced by: logimclad 25928 eflogeq 25957 cosargd 25963 logcnlem3 25999 logcnlem4 26000 logcnlem5 26001 logcn 26002 dvloglem 26003 logf1o2 26005 logtayl 26015 logtayl2 26017 mulcxp 26040 dvcncxp1 26096 cxpeq 26110 logrec 26113 logbcl 26117 logb1 26119 relogbreexp 26125 nnlogbexp 26131 logbrec 26132 ang180lem1 26159 ang180lem2 26160 ang180lem3 26161 ang180lem4 26162 lawcos 26166 isosctrlem1 26168 isosctrlem2 26169 asinf 26222 atanf 26230 asinneg 26236 efiasin 26238 asinbnd 26249 atanneg 26257 atancj 26260 efiatan 26262 atanlogaddlem 26263 atanlogadd 26264 atanlogsublem 26265 atanlogsub 26266 efiatan2 26267 2efiatan 26268 atantan 26273 atanbndlem 26275 dvatan 26285 atantayl 26287 efrlim 26319 lgamgulmlem2 26379 lgamgulmlem3 26380 lgamgulmlem5 26382 lgamgulmlem6 26383 lgamgulm2 26385 lgambdd 26386 lgamcvg2 26404 gamcvg 26405 gamp1 26407 gamcvg2lem 26408 hgt750lemd 33261 logdivsqrle 33263 hgt750lemb 33269 iprodgam 34315 dvasin 36162 aks4d1p1p1 40520 dvrelog2 40521 dvrelog3 40522 dvrelog2b 40523 dvrelogpow2b 40525 aks4d1p1p6 40530 aks4d1p1p7 40531 aks4d1p1p5 40532 isosctrlem1ALT 43206 stirlinglem4 44308 stirlinglem5 44309 stirlinglem7 44311 stirlinglem12 44316 stirlinglem14 44318 |
Copyright terms: Public domain | W3C validator |