Theorem exp0d 13498

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110  (class class class)co 7150  ℂcc 10529  0cc0 10531  1c1 10532  ↑cexp 13423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321  ax-1cn 10589  ax-addrcl 10592  ax-rnegex 10602  ax-cnre 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-iota 6308  df-fun 6351  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-neg 10867  df-z 11976  df-seq 13364  df-exp 13424

This theorem is referenced by:  faclbnd4lem3  13649  faclbnd4lem4  13650  faclbnd6  13653  hashmap  13790  absexp  14658  binom  15179  geoser  15216  pwdif  15217  cvgrat  15233  efexp  15448  pwp1fsum  15736  prmdvdsexpr  16055  rpexp1i  16059  phiprm  16108  odzdvds  16126  pclem  16169  pcpre1  16173  pcexp  16190  dvdsprmpweqnn  16215  prmpwdvds  16234  pgp0  18715  sylow2alem2  18737  ablfac1eu  19189  pgpfac1lem3a  19192  plyeq0lem  24794  plyco  24825  vieta1  24895  abelthlem9  25022  advlogexp  25232  cxpmul2  25266  nnlogbexp  25353  ftalem5  25648  0sgm  25715  1sgmprm  25769  dchrptlem2  25835  bposlem5  25858  lgsval2lem  25877  lgsmod  25893  lgsdilem2  25903  lgsne0  25905  chebbnd1lem1  26039  dchrisum0flblem1  26078  qabvexp  26196  ostth2lem2  26204  ostth3  26208  rusgrnumwwlk  27748  nexple  31263  faclim  32973  faclim2  32975  knoppndvlem14  33859  nn0rppwr  39175  nn0expgcd  39177  fltnltalem  39267  mzpexpmpt  39335  pell14qrexpclnn0  39456  pellfund14  39488  rmxy0  39513  jm2.17a  39550  jm2.17b  39551  jm2.18  39578  jm2.23  39586  expdioph  39613  cnsrexpcl  39758  binomcxplemnotnn0  40681  dvnxpaek  42220  wallispilem2  42345  etransclem24  42537  etransclem25  42538  etransclem35  42548  lighneallem3  43766  lighneallem4  43769  altgsumbcALT  44395  expnegico01  44567  digexp  44661  dig1  44662