Theorem exp0d 14093

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  0cc0 11029  1c1 11030  ↑cexp 14014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-neg 11371  df-z 12516  df-seq 13955  df-exp 14015

This theorem is referenced by:  faclbnd4lem3  14248  faclbnd4lem4  14249  faclbnd6  14252  hashmap  14388  absexp  15257  binom  15786  geoser  15823  pwdif  15824  cvgrat  15839  efexp  16059  pwp1fsum  16351  nn0rppwr  16521  nn0expgcd  16524  prmdvdsexpr  16678  rpexp1i  16684  phiprm  16738  odzdvds  16757  pclem  16800  pcpre1  16804  pcexp  16821  dvdsprmpweqnn  16847  prmpwdvds  16866  pgp0  19562  sylow2alem2  19584  ablfac1eu  20041  pgpfac1lem3a  20044  plyeq0lem  26185  plyco  26216  vieta1  26289  abelthlem9  26418  advlogexp  26632  cxpmul2  26666  nnlogbexp  26758  ftalem5  27054  0sgm  27121  1sgmprm  27176  dchrptlem2  27242  bposlem5  27265  lgsval2lem  27284  lgsmod  27300  lgsdilem2  27310  lgsne0  27312  chebbnd1lem1  27446  dchrisum0flblem1  27485  qabvexp  27603  ostth2lem2  27611  ostth3  27615  rusgrnumwwlk  30061  nexple  32932  cos9thpiminplylem3  33944  faclim  35944  faclim2  35946  knoppndvlem14  36801  lcmineqlem12  42493  aks4d1p8  42540  aks6d1c1p8  42568  aks6d1c4  42577  aks6d1c7lem1  42633  aks5lem8  42654  abvexp  42991  flt0  43084  fltnltalem  43109  mzpexpmpt  43191  pell14qrexpclnn0  43312  pellfund14  43344  rmxy0  43369  jm2.17a  43406  jm2.17b  43407  jm2.18  43434  jm2.23  43442  expdioph  43469  cnsrexpcl  43611  binomcxplemnotnn0  44801  dvnxpaek  46388  wallispilem2  46512  etransclem24  46704  etransclem25  46705  etransclem35  46715  lighneallem3  48082  lighneallem4  48085  altgsumbcALT  48841  expnegico01  49006  digexp  49095  dig1  49096