Theorem exp0d 14047

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  0cc0 11006  1c1 11007  ↑cexp 13968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-1cn 11064  ax-addrcl 11067  ax-rnegex 11077  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-neg 11347  df-z 12469  df-seq 13909  df-exp 13969

This theorem is referenced by:  faclbnd4lem3  14202  faclbnd4lem4  14203  faclbnd6  14206  hashmap  14342  absexp  15211  binom  15737  geoser  15774  pwdif  15775  cvgrat  15790  efexp  16010  pwp1fsum  16302  nn0rppwr  16472  nn0expgcd  16475  prmdvdsexpr  16628  rpexp1i  16634  phiprm  16688  odzdvds  16707  pclem  16750  pcpre1  16754  pcexp  16771  dvdsprmpweqnn  16797  prmpwdvds  16816  pgp0  19509  sylow2alem2  19531  ablfac1eu  19988  pgpfac1lem3a  19991  plyeq0lem  26143  plyco  26174  vieta1  26248  abelthlem9  26378  advlogexp  26592  cxpmul2  26626  nnlogbexp  26719  ftalem5  27015  0sgm  27082  1sgmprm  27138  dchrptlem2  27204  bposlem5  27227  lgsval2lem  27246  lgsmod  27262  lgsdilem2  27272  lgsne0  27274  chebbnd1lem1  27408  dchrisum0flblem1  27447  qabvexp  27565  ostth2lem2  27573  ostth3  27577  rusgrnumwwlk  29954  nexple  32825  cos9thpiminplylem3  33795  faclim  35788  faclim2  35790  knoppndvlem14  36565  lcmineqlem12  42079  aks4d1p8  42126  aks6d1c1p8  42154  aks6d1c4  42163  aks6d1c7lem1  42219  aks5lem8  42240  abvexp  42571  flt0  42676  fltnltalem  42701  mzpexpmpt  42784  pell14qrexpclnn0  42905  pellfund14  42937  rmxy0  42962  jm2.17a  42999  jm2.17b  43000  jm2.18  43027  jm2.23  43035  expdioph  43062  cnsrexpcl  43204  binomcxplemnotnn0  44395  dvnxpaek  45986  wallispilem2  46110  etransclem24  46302  etransclem25  46303  etransclem35  46313  lighneallem3  47644  lighneallem4  47647  altgsumbcALT  48390  expnegico01  48556  digexp  48645  dig1  48646