Theorem exp0d 14105

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  0cc0 11068  1c1 11069  ↑cexp 14026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-1cn 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-neg 11408  df-z 12530  df-seq 13967  df-exp 14027

This theorem is referenced by:  faclbnd4lem3  14260  faclbnd4lem4  14261  faclbnd6  14264  hashmap  14400  absexp  15270  binom  15796  geoser  15833  pwdif  15834  cvgrat  15849  efexp  16069  pwp1fsum  16361  nn0rppwr  16531  nn0expgcd  16534  prmdvdsexpr  16687  rpexp1i  16693  phiprm  16747  odzdvds  16766  pclem  16809  pcpre1  16813  pcexp  16830  dvdsprmpweqnn  16856  prmpwdvds  16875  pgp0  19526  sylow2alem2  19548  ablfac1eu  20005  pgpfac1lem3a  20008  plyeq0lem  26115  plyco  26146  vieta1  26220  abelthlem9  26350  advlogexp  26564  cxpmul2  26598  nnlogbexp  26691  ftalem5  26987  0sgm  27054  1sgmprm  27110  dchrptlem2  27176  bposlem5  27199  lgsval2lem  27218  lgsmod  27234  lgsdilem2  27244  lgsne0  27246  chebbnd1lem1  27380  dchrisum0flblem1  27419  qabvexp  27537  ostth2lem2  27545  ostth3  27549  rusgrnumwwlk  29905  nexple  32769  cos9thpiminplylem3  33774  faclim  35733  faclim2  35735  knoppndvlem14  36513  lcmineqlem12  42028  aks4d1p8  42075  aks6d1c1p8  42103  aks6d1c4  42112  aks6d1c7lem1  42168  aks5lem8  42189  abvexp  42520  flt0  42625  fltnltalem  42650  mzpexpmpt  42733  pell14qrexpclnn0  42854  pellfund14  42886  rmxy0  42912  jm2.17a  42949  jm2.17b  42950  jm2.18  42977  jm2.23  42985  expdioph  43012  cnsrexpcl  43154  binomcxplemnotnn0  44345  dvnxpaek  45940  wallispilem2  46064  etransclem24  46256  etransclem25  46257  etransclem35  46267  lighneallem3  47608  lighneallem4  47611  altgsumbcALT  48341  expnegico01  48507  digexp  48596  dig1  48597