Theorem exp0d 14075

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  0cc0 11038  1c1 11039  ↑cexp 13996

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 5243  ax-nul 5253  ax-pr 5379  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

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 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-neg 11379  df-z 12501  df-seq 13937  df-exp 13997

This theorem is referenced by:  faclbnd4lem3  14230  faclbnd4lem4  14231  faclbnd6  14234  hashmap  14370  absexp  15239  binom  15765  geoser  15802  pwdif  15803  cvgrat  15818  efexp  16038  pwp1fsum  16330  nn0rppwr  16500  nn0expgcd  16503  prmdvdsexpr  16656  rpexp1i  16662  phiprm  16716  odzdvds  16735  pclem  16778  pcpre1  16782  pcexp  16799  dvdsprmpweqnn  16825  prmpwdvds  16844  pgp0  19537  sylow2alem2  19559  ablfac1eu  20016  pgpfac1lem3a  20019  plyeq0lem  26183  plyco  26214  vieta1  26288  abelthlem9  26418  advlogexp  26632  cxpmul2  26666  nnlogbexp  26759  ftalem5  27055  0sgm  27122  1sgmprm  27178  dchrptlem2  27244  bposlem5  27267  lgsval2lem  27286  lgsmod  27302  lgsdilem2  27312  lgsne0  27314  chebbnd1lem1  27448  dchrisum0flblem1  27487  qabvexp  27605  ostth2lem2  27613  ostth3  27617  rusgrnumwwlk  30063  nexple  32935  cos9thpiminplylem3  33961  faclim  35959  faclim2  35961  knoppndvlem14  36744  lcmineqlem12  42407  aks4d1p8  42454  aks6d1c1p8  42482  aks6d1c4  42491  aks6d1c7lem1  42547  aks5lem8  42568  abvexp  42899  flt0  42992  fltnltalem  43017  mzpexpmpt  43099  pell14qrexpclnn0  43220  pellfund14  43252  rmxy0  43277  jm2.17a  43314  jm2.17b  43315  jm2.18  43342  jm2.23  43350  expdioph  43377  cnsrexpcl  43519  binomcxplemnotnn0  44709  dvnxpaek  46297  wallispilem2  46421  etransclem24  46613  etransclem25  46614  etransclem35  46624  lighneallem3  47964  lighneallem4  47967  altgsumbcALT  48710  expnegico01  48875  digexp  48964  dig1  48965