Theorem exp0d 13710

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2110  (class class class)co 7213  ℂcc 10727  0cc0 10729  1c1 10730  ↑cexp 13635

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 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-1cn 10787  ax-addrcl 10790  ax-rnegex 10800  ax-cnre 10802

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 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-iota 6338  df-fun 6382  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-neg 11065  df-z 12177  df-seq 13575  df-exp 13636

This theorem is referenced by:  faclbnd4lem3  13861  faclbnd4lem4  13862  faclbnd6  13865  hashmap  14002  absexp  14868  binom  15394  geoser  15431  pwdif  15432  cvgrat  15447  efexp  15662  pwp1fsum  15952  prmdvdsexpr  16274  rpexp1i  16280  phiprm  16330  odzdvds  16348  pclem  16391  pcpre1  16395  pcexp  16412  dvdsprmpweqnn  16438  prmpwdvds  16457  pgp0  18985  sylow2alem2  19007  ablfac1eu  19460  pgpfac1lem3a  19463  plyeq0lem  25104  plyco  25135  vieta1  25205  abelthlem9  25332  advlogexp  25543  cxpmul2  25577  nnlogbexp  25664  ftalem5  25959  0sgm  26026  1sgmprm  26080  dchrptlem2  26146  bposlem5  26169  lgsval2lem  26188  lgsmod  26204  lgsdilem2  26214  lgsne0  26216  chebbnd1lem1  26350  dchrisum0flblem1  26389  qabvexp  26507  ostth2lem2  26515  ostth3  26519  rusgrnumwwlk  28059  nexple  31689  faclim  33430  faclim2  33432  knoppndvlem14  34442  lcmineqlem12  39782  nn0rppwr  40041  nn0expgcd  40043  flt0  40177  fltnltalem  40202  mzpexpmpt  40270  pell14qrexpclnn0  40391  pellfund14  40423  rmxy0  40448  jm2.17a  40485  jm2.17b  40486  jm2.18  40513  jm2.23  40521  expdioph  40548  cnsrexpcl  40693  binomcxplemnotnn0  41647  dvnxpaek  43158  wallispilem2  43282  etransclem24  43474  etransclem25  43475  etransclem35  43485  lighneallem3  44732  lighneallem4  44735  altgsumbcALT  45362  expnegico01  45532  digexp  45626  dig1  45627