Theorem exp0d 13786

Description: Value of a complex number raised to the 0th 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 13714	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴↑0) = 1)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  0cc0 10802  1c1 10803  ↑cexp 13710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-1cn 10860  ax-addrcl 10863  ax-rnegex 10873  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-neg 11138  df-z 12250  df-seq 13650  df-exp 13711

This theorem is referenced by:  faclbnd4lem3  13937  faclbnd4lem4  13938  faclbnd6  13941  hashmap  14078  absexp  14944  binom  15470  geoser  15507  pwdif  15508  cvgrat  15523  efexp  15738  pwp1fsum  16028  prmdvdsexpr  16350  rpexp1i  16356  phiprm  16406  odzdvds  16424  pclem  16467  pcpre1  16471  pcexp  16488  dvdsprmpweqnn  16514  prmpwdvds  16533  pgp0  19116  sylow2alem2  19138  ablfac1eu  19591  pgpfac1lem3a  19594  plyeq0lem  25276  plyco  25307  vieta1  25377  abelthlem9  25504  advlogexp  25715  cxpmul2  25749  nnlogbexp  25836  ftalem5  26131  0sgm  26198  1sgmprm  26252  dchrptlem2  26318  bposlem5  26341  lgsval2lem  26360  lgsmod  26376  lgsdilem2  26386  lgsne0  26388  chebbnd1lem1  26522  dchrisum0flblem1  26561  qabvexp  26679  ostth2lem2  26687  ostth3  26691  rusgrnumwwlk  28241  nexple  31877  faclim  33618  faclim2  33620  knoppndvlem14  34632  lcmineqlem12  39976  aks4d1p8  40023  nn0rppwr  40254  nn0expgcd  40256  flt0  40390  fltnltalem  40415  mzpexpmpt  40483  pell14qrexpclnn0  40604  pellfund14  40636  rmxy0  40661  jm2.17a  40698  jm2.17b  40699  jm2.18  40726  jm2.23  40734  expdioph  40761  cnsrexpcl  40906  binomcxplemnotnn0  41863  dvnxpaek  43373  wallispilem2  43497  etransclem24  43689  etransclem25  43690  etransclem35  43700  lighneallem3  44947  lighneallem4  44950  altgsumbcALT  45577  expnegico01  45747  digexp  45841  dig1  45842