Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cxpefd | Structured version Visualization version GIF version |
Description: Value of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
Ref | Expression |
---|---|
cxp0d.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
cxpefd.2 | ⊢ (𝜑 → 𝐴 ≠ 0) |
cxpefd.3 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
Ref | Expression |
---|---|
cxpefd | ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cxp0d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | cxpefd.2 | . 2 ⊢ (𝜑 → 𝐴 ≠ 0) | |
3 | cxpefd.3 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
4 | cxpef 25848 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | |
5 | 1, 2, 3, 4 | syl3anc 1369 | 1 ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2101 ≠ wne 2938 ‘cfv 6447 (class class class)co 7295 ℂcc 10897 0cc0 10899 · cmul 10904 expce 15799 logclog 25738 ↑𝑐ccxp 25739 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-sep 5226 ax-nul 5233 ax-pr 5355 ax-1cn 10957 ax-icn 10958 ax-addcl 10959 ax-mulcl 10961 ax-i2m1 10967 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3224 df-v 3436 df-sbc 3719 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4260 df-if 4463 df-sn 4565 df-pr 4567 df-op 4571 df-uni 4842 df-br 5078 df-opab 5140 df-id 5491 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-iota 6399 df-fun 6449 df-fv 6455 df-ov 7298 df-oprab 7299 df-mpo 7300 df-cxp 25741 |
This theorem is referenced by: dvcxp1 25921 dvcxp2 25922 dvcncxp1 25924 cxpcn 25926 abscxpbnd 25934 root1eq1 25936 cxpeq 25938 cxplogb 25964 efiatan 26090 efiatan2 26095 efrlim 26147 cxp2limlem 26153 cxploglim 26155 amgmlem 26167 zetacvg 26192 gamcvg2lem 26236 bposlem9 26468 chtppilimlem1 26649 ostth2lem4 26812 ostth2 26813 ostth3 26814 iprodgam 33736 aks4d1p1p1 40097 proot1ex 41050 logcxp0 45921 |
Copyright terms: Public domain | W3C validator |