Theorem exp0d 13964

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7342  ℂcc 10975  0cc0 10977  1c1 10978  ↑cexp 13888

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5248  ax-nul 5255  ax-pr 5377  ax-1cn 11035  ax-addrcl 11038  ax-rnegex 11048  ax-cnre 11050

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3732  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-br 5098  df-opab 5160  df-mpt 5181  df-id 5523  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-iota 6436  df-fun 6486  df-fv 6492  df-ov 7345  df-oprab 7346  df-mpo 7347  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-neg 11314  df-z 12426  df-seq 13828  df-exp 13889

This theorem is referenced by:  faclbnd4lem3  14115  faclbnd4lem4  14116  faclbnd6  14119  hashmap  14255  absexp  15116  binom  15642  geoser  15679  pwdif  15680  cvgrat  15695  efexp  15910  pwp1fsum  16200  prmdvdsexpr  16520  rpexp1i  16526  phiprm  16576  odzdvds  16594  pclem  16637  pcpre1  16641  pcexp  16658  dvdsprmpweqnn  16684  prmpwdvds  16703  pgp0  19298  sylow2alem2  19320  ablfac1eu  19771  pgpfac1lem3a  19774  plyeq0lem  25477  plyco  25508  vieta1  25578  abelthlem9  25705  advlogexp  25916  cxpmul2  25950  nnlogbexp  26037  ftalem5  26332  0sgm  26399  1sgmprm  26453  dchrptlem2  26519  bposlem5  26542  lgsval2lem  26561  lgsmod  26577  lgsdilem2  26587  lgsne0  26589  chebbnd1lem1  26723  dchrisum0flblem1  26762  qabvexp  26880  ostth2lem2  26888  ostth3  26892  rusgrnumwwlk  28628  nexple  32273  faclim  34002  faclim2  34004  knoppndvlem14  34842  lcmineqlem12  40351  aks4d1p8  40398  nn0rppwr  40642  nn0expgcd  40644  flt0  40785  fltnltalem  40810  mzpexpmpt  40878  pell14qrexpclnn0  40999  pellfund14  41031  rmxy0  41057  jm2.17a  41094  jm2.17b  41095  jm2.18  41122  jm2.23  41130  expdioph  41157  cnsrexpcl  41302  binomcxplemnotnn0  42345  dvnxpaek  43869  wallispilem2  43993  etransclem24  44185  etransclem25  44186  etransclem35  44196  lighneallem3  45475  lighneallem4  45478  altgsumbcALT  46105  expnegico01  46275  digexp  46369  dig1  46370