Theorem exp0d 14051

Description: Value of a complex number raised to the zeroth power. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
expcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
exp0d	⊢ (𝜑 → (𝐴↑0) = 1)

Proof of Theorem exp0d

Step	Hyp	Ref	Expression
1		expcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		exp0 13976	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴↑0) = 1)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7354  ℂcc 11013  0cc0 11015  1c1 11016  ↑cexp 13972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-1cn 11073  ax-addrcl 11076  ax-rnegex 11086  ax-cnre 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6255  df-iota 6444  df-fun 6490  df-fv 6496  df-ov 7357  df-oprab 7358  df-mpo 7359  df-frecs 8219  df-wrecs 8250  df-recs 8299  df-rdg 8337  df-neg 11356  df-z 12478  df-seq 13913  df-exp 13973

This theorem is referenced by:  faclbnd4lem3  14206  faclbnd4lem4  14207  faclbnd6  14210  hashmap  14346  absexp  15215  binom  15741  geoser  15778  pwdif  15779  cvgrat  15794  efexp  16014  pwp1fsum  16306  nn0rppwr  16476  nn0expgcd  16479  prmdvdsexpr  16632  rpexp1i  16638  phiprm  16692  odzdvds  16711  pclem  16754  pcpre1  16758  pcexp  16775  dvdsprmpweqnn  16801  prmpwdvds  16820  pgp0  19512  sylow2alem2  19534  ablfac1eu  19991  pgpfac1lem3a  19994  plyeq0lem  26145  plyco  26176  vieta1  26250  abelthlem9  26380  advlogexp  26594  cxpmul2  26628  nnlogbexp  26721  ftalem5  27017  0sgm  27084  1sgmprm  27140  dchrptlem2  27206  bposlem5  27229  lgsval2lem  27248  lgsmod  27264  lgsdilem2  27274  lgsne0  27276  chebbnd1lem1  27410  dchrisum0flblem1  27449  qabvexp  27567  ostth2lem2  27575  ostth3  27579  rusgrnumwwlk  29960  nexple  32834  cos9thpiminplylem3  33820  faclim  35813  faclim2  35815  knoppndvlem14  36592  lcmineqlem12  42156  aks4d1p8  42203  aks6d1c1p8  42231  aks6d1c4  42240  aks6d1c7lem1  42296  aks5lem8  42317  abvexp  42653  flt0  42758  fltnltalem  42783  mzpexpmpt  42865  pell14qrexpclnn0  42986  pellfund14  43018  rmxy0  43043  jm2.17a  43080  jm2.17b  43081  jm2.18  43108  jm2.23  43116  expdioph  43143  cnsrexpcl  43285  binomcxplemnotnn0  44476  dvnxpaek  46067  wallispilem2  46191  etransclem24  46383  etransclem25  46384  etransclem35  46394  lighneallem3  47734  lighneallem4  47737  altgsumbcALT  48480  expnegico01  48646  digexp  48735  dig1  48736