Theorem exp0d 14208

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126  0cc0 11128  1c1 11129  ↑cexp 14129

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-1cn 11186  ax-addrcl 11189  ax-rnegex 11199  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-neg 11472  df-z 12620  df-seq 14070  df-exp 14130

This theorem is used by:  faclbnd4lem3  14363  faclbnd4lem4  14364  faclbnd6  14367  hashmap  14504  absexp  15395  binom  15923  geoser  15960  pwdif  15961  cvgrat  15976  efexp  16195  pwp1fsum  16487  nn0rppwr  16657  nn0expgcd  16660  prmdvdsexpr  16814  rpexp1i  16820  phiprm  16874  odzdvds  16893  pclem  16936  pcpre1  16940  pcexp  16957  dvdsprmpweqnn  16983  prmpwdvds  17002  pgp0  19729  sylow2alem2  19751  ablfac1eu  20208  pgpfac1lem3a  20211  plyeq0lem  26443  plyco  26474  vieta1  26551  abelthlem9  26683  advlogexp  26900  cxpmul2  26934  nnlogbexp  27026  ftalem5  27321  0sgm  27388  1sgmprm  27443  dchrptlem2  27509  bposlem5  27532  lgsval2lem  27551  lgsmod  27567  lgsdilem2  27577  lgsne0  27579  chebbnd1lem1  27713  dchrisum0flblem1  27752  qabvexp  27870  ostth2lem2  27878  ostth3  27882  rusgrnumwwlk  30454  nexple  33311  cos9thpiminplylem3  34302  faclim  36333  faclim2  36335  knoppndvlem14  37230  lcmineqlem12  42914  aks4d1p8  42961  aks6d1c1p8  42989  aks6d1c4  42998  aks6d1c7lem1  43054  aks5lem8  43075  abvexp  43422  flt0  43491  fltnltalem  43516  mzpexpmpt  43598  pell14qrexpclnn0  43715  pellfund14  43747  rmxy0  43772  jm2.17a  43809  jm2.17b  43810  jm2.18  43837  jm2.23  43845  expdioph  43872  cnsrexpcl  44014  binomcxplemnotnn0  45188  dvnxpaek  46778  wallispilem2  46902  etransclem24  47094  etransclem25  47095  etransclem35  47105  lighneallem3  48518  lighneallem4  48521  altgsumbcALT  49291  expnegico01  49456  digexp  49545  dig1  49546