Theorem exp0d 14164

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  0cc0 11088  1c1 11089  ↑cexp 14085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394  ax-1cn 11146  ax-addrcl 11149  ax-rnegex 11159  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-neg 11432  df-z 12580  df-seq 14026  df-exp 14086

This theorem is referenced by:  faclbnd4lem3  14319  faclbnd4lem4  14320  faclbnd6  14323  hashmap  14460  absexp  15343  binom  15872  geoser  15909  pwdif  15910  cvgrat  15925  efexp  16145  pwp1fsum  16437  nn0rppwr  16607  nn0expgcd  16610  prmdvdsexpr  16764  rpexp1i  16770  phiprm  16824  odzdvds  16843  pclem  16886  pcpre1  16890  pcexp  16907  dvdsprmpweqnn  16933  prmpwdvds  16952  pgp0  19654  sylow2alem2  19676  ablfac1eu  20133  pgpfac1lem3a  20136  plyeq0lem  26324  plyco  26355  vieta1  26430  abelthlem9  26557  advlogexp  26774  cxpmul2  26808  nnlogbexp  26900  ftalem5  27195  0sgm  27262  1sgmprm  27317  dchrptlem2  27383  bposlem5  27406  lgsval2lem  27425  lgsmod  27441  lgsdilem2  27451  lgsne0  27453  chebbnd1lem1  27587  dchrisum0flblem1  27626  qabvexp  27744  ostth2lem2  27752  ostth3  27756  rusgrnumwwlk  30232  nexple  33085  cos9thpiminplylem3  34086  faclim  36104  faclim2  36106  knoppndvlem14  36971  lcmineqlem12  42664  aks4d1p8  42711  aks6d1c1p8  42739  aks6d1c4  42748  aks6d1c7lem1  42804  aks5lem8  42825  abvexp  43157  flt0  43226  fltnltalem  43251  mzpexpmpt  43333  pell14qrexpclnn0  43450  pellfund14  43482  rmxy0  43507  jm2.17a  43544  jm2.17b  43545  jm2.18  43572  jm2.23  43580  expdioph  43607  cnsrexpcl  43749  binomcxplemnotnn0  44925  dvnxpaek  46515  wallispilem2  46639  etransclem24  46831  etransclem25  46832  etransclem35  46842  lighneallem3  48215  lighneallem4  48218  altgsumbcALT  48985  expnegico01  49150  digexp  49239  dig1  49240