Theorem exp0d 14190

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  0cc0 11184  1c1 11185  ↑cexp 14112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-1cn 11242  ax-addrcl 11245  ax-rnegex 11255  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-iota 6525  df-fun 6575  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-neg 11523  df-z 12640  df-seq 14053  df-exp 14113

This theorem is referenced by:  faclbnd4lem3  14344  faclbnd4lem4  14345  faclbnd6  14348  hashmap  14484  absexp  15353  binom  15878  geoser  15915  pwdif  15916  cvgrat  15931  efexp  16149  pwp1fsum  16439  nn0rppwr  16608  nn0expgcd  16611  prmdvdsexpr  16764  rpexp1i  16770  phiprm  16824  odzdvds  16842  pclem  16885  pcpre1  16889  pcexp  16906  dvdsprmpweqnn  16932  prmpwdvds  16951  pgp0  19638  sylow2alem2  19660  ablfac1eu  20117  pgpfac1lem3a  20120  plyeq0lem  26269  plyco  26300  vieta1  26372  abelthlem9  26502  advlogexp  26715  cxpmul2  26749  nnlogbexp  26842  ftalem5  27138  0sgm  27205  1sgmprm  27261  dchrptlem2  27327  bposlem5  27350  lgsval2lem  27369  lgsmod  27385  lgsdilem2  27395  lgsne0  27397  chebbnd1lem1  27531  dchrisum0flblem1  27570  qabvexp  27688  ostth2lem2  27696  ostth3  27700  rusgrnumwwlk  30008  nexple  33973  faclim  35708  faclim2  35710  knoppndvlem14  36491  lcmineqlem12  41997  aks4d1p8  42044  aks6d1c1p8  42072  aks6d1c4  42081  aks6d1c7lem1  42137  aks5lem8  42158  abvexp  42487  flt0  42592  fltnltalem  42617  mzpexpmpt  42701  pell14qrexpclnn0  42822  pellfund14  42854  rmxy0  42880  jm2.17a  42917  jm2.17b  42918  jm2.18  42945  jm2.23  42953  expdioph  42980  cnsrexpcl  43122  binomcxplemnotnn0  44325  dvnxpaek  45863  wallispilem2  45987  etransclem24  46179  etransclem25  46180  etransclem35  46190  lighneallem3  47481  lighneallem4  47484  altgsumbcALT  48078  expnegico01  48247  digexp  48341  dig1  48342