Theorem exp0d 14158

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127  0cc0 11129  1c1 11130  ↑cexp 14079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-1cn 11187  ax-addrcl 11190  ax-rnegex 11200  ax-cnre 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-iota 6484  df-fun 6533  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-neg 11469  df-z 12589  df-seq 14020  df-exp 14080

This theorem is referenced by:  faclbnd4lem3  14313  faclbnd4lem4  14314  faclbnd6  14317  hashmap  14453  absexp  15323  binom  15846  geoser  15883  pwdif  15884  cvgrat  15899  efexp  16119  pwp1fsum  16410  nn0rppwr  16580  nn0expgcd  16583  prmdvdsexpr  16736  rpexp1i  16742  phiprm  16796  odzdvds  16815  pclem  16858  pcpre1  16862  pcexp  16879  dvdsprmpweqnn  16905  prmpwdvds  16924  pgp0  19577  sylow2alem2  19599  ablfac1eu  20056  pgpfac1lem3a  20059  plyeq0lem  26167  plyco  26198  vieta1  26272  abelthlem9  26402  advlogexp  26616  cxpmul2  26650  nnlogbexp  26743  ftalem5  27039  0sgm  27106  1sgmprm  27162  dchrptlem2  27228  bposlem5  27251  lgsval2lem  27270  lgsmod  27286  lgsdilem2  27296  lgsne0  27298  chebbnd1lem1  27432  dchrisum0flblem1  27471  qabvexp  27589  ostth2lem2  27597  ostth3  27601  rusgrnumwwlk  29957  nexple  32823  cos9thpiminplylem3  33818  faclim  35763  faclim2  35765  knoppndvlem14  36543  lcmineqlem12  42053  aks4d1p8  42100  aks6d1c1p8  42128  aks6d1c4  42137  aks6d1c7lem1  42193  aks5lem8  42214  abvexp  42555  flt0  42660  fltnltalem  42685  mzpexpmpt  42768  pell14qrexpclnn0  42889  pellfund14  42921  rmxy0  42947  jm2.17a  42984  jm2.17b  42985  jm2.18  43012  jm2.23  43020  expdioph  43047  cnsrexpcl  43189  binomcxplemnotnn0  44380  dvnxpaek  45971  wallispilem2  46095  etransclem24  46287  etransclem25  46288  etransclem35  46298  lighneallem3  47621  lighneallem4  47624  altgsumbcALT  48328  expnegico01  48494  digexp  48587  dig1  48588