Theorem exp0d 14146

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 14071	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴↑0) = 1)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7390  ℂcc 11064  0cc0 11066  1c1 11067  ↑cexp 14067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-1cn 11124  ax-addrcl 11127  ax-rnegex 11137  ax-cnre 11139

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-iota 6471  df-fun 6517  df-fv 6523  df-ov 7393  df-oprab 7394  df-mpo 7395  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-neg 11410  df-z 12562  df-seq 14008  df-exp 14068

This theorem is referenced by:  faclbnd4lem3  14301  faclbnd4lem4  14302  faclbnd6  14305  hashmap  14441  absexp  15321  binom  15850  geoser  15887  pwdif  15888  cvgrat  15903  efexp  16123  pwp1fsum  16415  nn0rppwr  16585  nn0expgcd  16588  prmdvdsexpr  16742  rpexp1i  16748  phiprm  16802  odzdvds  16821  pclem  16864  pcpre1  16868  pcexp  16885  dvdsprmpweqnn  16911  prmpwdvds  16930  pgp0  19626  sylow2alem2  19648  ablfac1eu  20105  pgpfac1lem3a  20108  plyeq0lem  26257  plyco  26288  vieta1  26363  abelthlem9  26490  advlogexp  26707  cxpmul2  26741  nnlogbexp  26833  ftalem5  27128  0sgm  27195  1sgmprm  27250  dchrptlem2  27316  bposlem5  27339  lgsval2lem  27358  lgsmod  27374  lgsdilem2  27384  lgsne0  27386  chebbnd1lem1  27520  dchrisum0flblem1  27559  qabvexp  27677  ostth2lem2  27685  ostth3  27689  rusgrnumwwlk  30134  nexple  32995  cos9thpiminplylem3  34041  faclim  36056  faclim2  36058  knoppndvlem14  36923  lcmineqlem12  42617  aks4d1p8  42664  aks6d1c1p8  42692  aks6d1c4  42701  aks6d1c7lem1  42757  aks5lem8  42778  abvexp  43110  flt0  43179  fltnltalem  43204  mzpexpmpt  43286  pell14qrexpclnn0  43403  pellfund14  43435  rmxy0  43460  jm2.17a  43497  jm2.17b  43498  jm2.18  43525  jm2.23  43533  expdioph  43560  cnsrexpcl  43702  binomcxplemnotnn0  44892  dvnxpaek  46476  wallispilem2  46600  etransclem24  46792  etransclem25  46793  etransclem35  46803  lighneallem3  48176  lighneallem4  48179  altgsumbcALT  48935  expnegico01  49100  digexp  49189  dig1  49190