MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cxpefd Structured version   Unicode version

Theorem cxpefd 23261
Description: Value of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
Hypotheses
Ref Expression
cxp0d.1  |-  ( ph  ->  A  e.  CC )
cxpefd.2  |-  ( ph  ->  A  =/=  0 )
cxpefd.3  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
cxpefd  |-  ( ph  ->  ( A  ^c  B )  =  ( exp `  ( B  x.  ( log `  A
) ) ) )

Proof of Theorem cxpefd
StepHypRef Expression
1 cxp0d.1 . 2  |-  ( ph  ->  A  e.  CC )
2 cxpefd.2 . 2  |-  ( ph  ->  A  =/=  0 )
3 cxpefd.3 . 2  |-  ( ph  ->  B  e.  CC )
4 cxpef 23214 . 2  |-  ( ( A  e.  CC  /\  A  =/=  0  /\  B  e.  CC )  ->  ( A  ^c  B )  =  ( exp `  ( B  x.  ( log `  A ) ) ) )
51, 2, 3, 4syl3anc 1226 1  |-  ( ph  ->  ( A  ^c  B )  =  ( exp `  ( B  x.  ( log `  A
) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    e. wcel 1823    =/= wne 2649   ` cfv 5570  (class class class)co 6270   CCcc 9479   0cc0 9481    x. cmul 9486   expce 13879   logclog 23108    ^c ccxp 23109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-mulcl 9543  ax-i2m1 9549
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-iota 5534  df-fun 5572  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-cxp 23111
This theorem is referenced by:  dvcxp1  23284  dvcxp2  23285  cxpcn  23287  abscxpbnd  23295  root1eq1  23297  cxpeq  23299  cxplogb  23325  efiatan  23440  efiatan2  23445  efrlim  23497  cxp2limlem  23503  cxploglim  23505  amgmlem  23517  bposlem9  23765  chtppilimlem1  23856  ostth2lem4  24019  ostth2  24020  ostth3  24021  zetacvg  28821  gamcvg2lem  28865  iprodgam  29366  dvcncxp1  30340  proot1ex  31402  logcxp0  33410
  Copyright terms: Public domain W3C validator