MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp1d Structured version   Visualization version   GIF version

Theorem exp1d 13744
Description: Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
expcld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
exp1d (𝜑 → (𝐴↑1) = 𝐴)

Proof of Theorem exp1d
StepHypRef Expression
1 expcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 exp1 13673 . 2 (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴↑1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2112  (class class class)co 7235  cc 10757  1c1 10760  cexp 13667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545  ax-cnex 10815  ax-resscn 10816  ax-1cn 10817  ax-icn 10818  ax-addcl 10819  ax-addrcl 10820  ax-mulcl 10821  ax-mulrcl 10822  ax-mulcom 10823  ax-addass 10824  ax-mulass 10825  ax-distr 10826  ax-i2m1 10827  ax-1ne0 10828  ax-1rid 10829  ax-rnegex 10830  ax-rrecex 10831  ax-cnre 10832  ax-pre-lttri 10833  ax-pre-lttrn 10834  ax-pre-ltadd 10835  ax-pre-mulgt0 10836
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-pred 6179  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-riota 7192  df-ov 7238  df-oprab 7239  df-mpo 7240  df-om 7667  df-2nd 7784  df-wrecs 8071  df-recs 8132  df-rdg 8170  df-er 8415  df-en 8651  df-dom 8652  df-sdom 8653  df-pnf 10899  df-mnf 10900  df-xr 10901  df-ltxr 10902  df-le 10903  df-sub 11094  df-neg 11095  df-nn 11861  df-n0 12121  df-z 12207  df-uz 12469  df-seq 13607  df-exp 13668
This theorem is referenced by:  faclbnd4lem1  13892  fsumcube  15655  sin01gt0  15784  rplpwr  16152  prmdvdsexp  16305  phiprm  16363  eulerthlem2  16368  pcelnn  16456  expnprm  16488  prmpwdvds  16490  pockthg  16492  odcau  19026  plyco  25167  dgrcolem1  25199  vieta1  25237  taylthlem1  25297  ftalem2  25988  vmaprm  26031  vma1  26080  1sgmprm  26112  chtublem  26124  fsumvma2  26127  chpchtsum  26132  logfacrlim2  26139  bposlem2  26198  bposlem6  26202  lgsval2lem  26220  2sqblem  26344  chebbnd1lem1  26382  rplogsumlem2  26398  rpvmasumlem  26400  ostth3  26551  nn0prpwlem  34282  nn0prpw  34283  bfplem1  35754  dvrelogpow2b  39846  aks4d1p1p4  39849  aks4d1p1p7  39852  aks4d1p1p5  39853  aks4d1p1  39854  aks4d1p3  39856  2ap1caineq  39865  fltnltalem  40250  fltnlta  40251  3cubeslem3r  40260  rmxy1  40495  jm2.18  40561  jm2.23  40569  jm3.1lem2  40591  areaquad  40798  radcnvrat  41653  stoweidlem3  43265  wallispilem2  43328  stirlinglem1  43336  stirlinglem7  43342  stirlinglem10  43345  lighneal  44782  blenpw2m1  45644
  Copyright terms: Public domain W3C validator