![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cxpcl | Structured version Visualization version GIF version |
Description: Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
Ref | Expression |
---|---|
cxpcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cxpval 26015 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = if(𝐴 = 0, if(𝐵 = 0, 1, 0), (exp‘(𝐵 · (log‘𝐴))))) | |
2 | ax-1cn 11106 | . . . . 5 ⊢ 1 ∈ ℂ | |
3 | 0cn 11144 | . . . . 5 ⊢ 0 ∈ ℂ | |
4 | 2, 3 | ifcli 4532 | . . . 4 ⊢ if(𝐵 = 0, 1, 0) ∈ ℂ |
5 | 4 | a1i 11 | . . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 = 0) → if(𝐵 = 0, 1, 0) ∈ ℂ) |
6 | df-ne 2943 | . . . 4 ⊢ (𝐴 ≠ 0 ↔ ¬ 𝐴 = 0) | |
7 | id 22 | . . . . . . 7 ⊢ (𝐵 ∈ ℂ → 𝐵 ∈ ℂ) | |
8 | logcl 25920 | . . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ) | |
9 | mulcl 11132 | . . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ (log‘𝐴) ∈ ℂ) → (𝐵 · (log‘𝐴)) ∈ ℂ) | |
10 | 7, 8, 9 | syl2anr 597 | . . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℂ) → (𝐵 · (log‘𝐴)) ∈ ℂ) |
11 | 10 | an32s 650 | . . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (𝐵 · (log‘𝐴)) ∈ ℂ) |
12 | efcl 15962 | . . . . 5 ⊢ ((𝐵 · (log‘𝐴)) ∈ ℂ → (exp‘(𝐵 · (log‘𝐴))) ∈ ℂ) | |
13 | 11, 12 | syl 17 | . . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐴 ≠ 0) → (exp‘(𝐵 · (log‘𝐴))) ∈ ℂ) |
14 | 6, 13 | sylan2br 595 | . . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ¬ 𝐴 = 0) → (exp‘(𝐵 · (log‘𝐴))) ∈ ℂ) |
15 | 5, 14 | ifclda 4520 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → if(𝐴 = 0, if(𝐵 = 0, 1, 0), (exp‘(𝐵 · (log‘𝐴)))) ∈ ℂ) |
16 | 1, 15 | eqeltrd 2838 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2942 ifcif 4485 ‘cfv 6494 (class class class)co 7354 ℂcc 11046 0cc0 11048 1c1 11049 · cmul 11053 expce 15941 logclog 25906 ↑𝑐ccxp 25907 |
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 5241 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7669 ax-inf2 9574 ax-cnex 11104 ax-resscn 11105 ax-1cn 11106 ax-icn 11107 ax-addcl 11108 ax-addrcl 11109 ax-mulcl 11110 ax-mulrcl 11111 ax-mulcom 11112 ax-addass 11113 ax-mulass 11114 ax-distr 11115 ax-i2m1 11116 ax-1ne0 11117 ax-1rid 11118 ax-rnegex 11119 ax-rrecex 11120 ax-cnre 11121 ax-pre-lttri 11122 ax-pre-lttrn 11123 ax-pre-ltadd 11124 ax-pre-mulgt0 11125 ax-pre-sup 11126 ax-addf 11127 ax-mulf 11128 |
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 2888 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-rmo 3352 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-pss 3928 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4865 df-int 4907 df-iun 4955 df-iin 4956 df-br 5105 df-opab 5167 df-mpt 5188 df-tr 5222 df-id 5530 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5587 df-se 5588 df-we 5589 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6252 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6446 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-isom 6503 df-riota 7310 df-ov 7357 df-oprab 7358 df-mpo 7359 df-of 7614 df-om 7800 df-1st 7918 df-2nd 7919 df-supp 8090 df-frecs 8209 df-wrecs 8240 df-recs 8314 df-rdg 8353 df-1o 8409 df-2o 8410 df-er 8645 df-map 8764 df-pm 8765 df-ixp 8833 df-en 8881 df-dom 8882 df-sdom 8883 df-fin 8884 df-fsupp 9303 df-fi 9344 df-sup 9375 df-inf 9376 df-oi 9443 df-card 9872 df-pnf 11188 df-mnf 11189 df-xr 11190 df-ltxr 11191 df-le 11192 df-sub 11384 df-neg 11385 df-div 11810 df-nn 12151 df-2 12213 df-3 12214 df-4 12215 df-5 12216 df-6 12217 df-7 12218 df-8 12219 df-9 12220 df-n0 12411 df-z 12497 df-dec 12616 df-uz 12761 df-q 12871 df-rp 12913 df-xneg 13030 df-xadd 13031 df-xmul 13032 df-ioo 13265 df-ioc 13266 df-ico 13267 df-icc 13268 df-fz 13422 df-fzo 13565 df-fl 13694 df-mod 13772 df-seq 13904 df-exp 13965 df-fac 14171 df-bc 14200 df-hash 14228 df-shft 14949 df-cj 14981 df-re 14982 df-im 14983 df-sqrt 15117 df-abs 15118 df-limsup 15350 df-clim 15367 df-rlim 15368 df-sum 15568 df-ef 15947 df-sin 15949 df-cos 15950 df-pi 15952 df-struct 17016 df-sets 17033 df-slot 17051 df-ndx 17063 df-base 17081 df-ress 17110 df-plusg 17143 df-mulr 17144 df-starv 17145 df-sca 17146 df-vsca 17147 df-ip 17148 df-tset 17149 df-ple 17150 df-ds 17152 df-unif 17153 df-hom 17154 df-cco 17155 df-rest 17301 df-topn 17302 df-0g 17320 df-gsum 17321 df-topgen 17322 df-pt 17323 df-prds 17326 df-xrs 17381 df-qtop 17386 df-imas 17387 df-xps 17389 df-mre 17463 df-mrc 17464 df-acs 17466 df-mgm 18494 df-sgrp 18543 df-mnd 18554 df-submnd 18599 df-mulg 18869 df-cntz 19093 df-cmn 19560 df-psmet 20784 df-xmet 20785 df-met 20786 df-bl 20787 df-mopn 20788 df-fbas 20789 df-fg 20790 df-cnfld 20793 df-top 22239 df-topon 22256 df-topsp 22278 df-bases 22292 df-cld 22366 df-ntr 22367 df-cls 22368 df-nei 22445 df-lp 22483 df-perf 22484 df-cn 22574 df-cnp 22575 df-haus 22662 df-tx 22909 df-hmeo 23102 df-fil 23193 df-fm 23285 df-flim 23286 df-flf 23287 df-xms 23669 df-ms 23670 df-tms 23671 df-cncf 24237 df-limc 25226 df-dv 25227 df-log 25908 df-cxp 25909 |
This theorem is referenced by: cxpneg 26032 cxpsub 26033 mulcxplem 26035 mulcxp 26036 cxprec 26037 divcxp 26038 cxpmul 26039 cxpmul2 26040 cxpmul2z 26042 cxpsqrt 26054 cxpcld 26059 cxpcn3 26097 root1cj 26105 cxpeq 26106 relogbcxp 26131 sqrt2cxp2logb9e3 26145 1cubrlem 26187 1cubr 26188 cubic 26195 quartlem3 26205 sgmf 26490 sgmppw 26541 dchrptlem1 26608 dchrptlem2 26609 proot1ex 41504 |
Copyright terms: Public domain | W3C validator |