Theorem exp0d 14100

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  0cc0 11036  1c1 11037  ↑cexp 14021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-1cn 11094  ax-addrcl 11097  ax-rnegex 11107  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  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 6259  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-neg 11378  df-z 12523  df-seq 13962  df-exp 14022

This theorem is referenced by:  faclbnd4lem3  14255  faclbnd4lem4  14256  faclbnd6  14259  hashmap  14395  absexp  15264  binom  15793  geoser  15830  pwdif  15831  cvgrat  15846  efexp  16066  pwp1fsum  16358  nn0rppwr  16528  nn0expgcd  16531  prmdvdsexpr  16685  rpexp1i  16691  phiprm  16745  odzdvds  16764  pclem  16807  pcpre1  16811  pcexp  16828  dvdsprmpweqnn  16854  prmpwdvds  16873  pgp0  19569  sylow2alem2  19591  ablfac1eu  20048  pgpfac1lem3a  20051  plyeq0lem  26200  plyco  26231  vieta1  26303  abelthlem9  26430  advlogexp  26644  cxpmul2  26678  nnlogbexp  26770  ftalem5  27065  0sgm  27132  1sgmprm  27187  dchrptlem2  27253  bposlem5  27276  lgsval2lem  27295  lgsmod  27311  lgsdilem2  27321  lgsne0  27323  chebbnd1lem1  27457  dchrisum0flblem1  27496  qabvexp  27614  ostth2lem2  27622  ostth3  27626  rusgrnumwwlk  30071  nexple  32943  cos9thpiminplylem3  33975  faclim  35981  faclim2  35983  knoppndvlem14  36838  lcmineqlem12  42532  aks4d1p8  42579  aks6d1c1p8  42607  aks6d1c4  42616  aks6d1c7lem1  42672  aks5lem8  42693  abvexp  43025  flt0  43094  fltnltalem  43119  mzpexpmpt  43201  pell14qrexpclnn0  43318  pellfund14  43350  rmxy0  43375  jm2.17a  43412  jm2.17b  43413  jm2.18  43440  jm2.23  43448  expdioph  43475  cnsrexpcl  43617  binomcxplemnotnn0  44807  dvnxpaek  46392  wallispilem2  46516  etransclem24  46708  etransclem25  46709  etransclem35  46719  lighneallem3  48092  lighneallem4  48095  altgsumbcALT  48851  expnegico01  49016  digexp  49105  dig1  49106