HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem exp0 8876
Description: Value of a complex number raised to the 0th power. Note that under our definition, , following the convention used by Gleason. Part of Definition 10-4.1 of [Gleason] p. 134. (Revised by Mario Carneiro, 2-Jul-2013.)
Assertion
Ref Expression
exp0

Proof of Theorem exp0
StepHypRef Expression
1 0z 8159 . . 3
2 expval 8874 . . 3
31, 2mpan2 647 . 2
4 eqid 1918 . . 3
5 iftrue 3017 . . 3
64, 5ax-mp 8 . 2
73, 6syl6eq 1966 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1414   wcel 1416  cif 3011  csn 3083   class class class wbr 3383   cxp 4019  cfv 4033  (class class class)co 5002  cc 7210  cc0 7212  c1 7213   cmul 7217   clt 7324  cneg 7437   cdiv 7438  cn 7439  cz 7441   cseq 8818  cexp 8872
This theorem is referenced by:  expp1 8878  expneg 8879  expcllem 8882  mulexp 8906  expadd 8909  expmul 8912  expmwordi 8924  exple1 8925  bernneq 8984  modexp 8993  faclbnd 9019  faclbnd3 9021  faclbnd4lem1 9022  faclbnd4lem3 9024  faclbnd4lem4 9025  faclbnd6 9028  hashmap 9084  cjexp 9175  absexp 9307  binom 9642  climcndslem1 9659  geoser 9671  cvgrat 9683  ef0lem 9704  ege2le3 9714  efexp 9724  eft0val 9734  demoivreALT 9816  prmdvdsexpr 10044  phiprm 10063  odzdvds 10077  pclem 10107  pcpre1 10111  prmpwdvds 10154  4001lem1 10295  expcn 12693  iblcnlem1 13637  itgcnlem 13639  dvexp 13770  dvexp2 13771  plyconst 13857  plyeq0lem 13861  plyco 13891  0dgr 13895  0dgrb 13896  coefv0 13897  dgreq0 13914  vieta1 13953  abelthlem9 14024  cxpexp 14192  cxp0 14194  cxpmul2 14212  ftalem5 14397  basellem2 14402  basellem5 14405  bposlem5 14424  chebbnd1lem1 14430  qabvexp 14450  ostth2lem2 14458  ostth3 14462  pgp0 16055  sylow2alem2 16074  subfacval2 16111  lgsval2lem 16147  lgsmod 16162  lgsdilem2 16172  lgsne0 16174  bpoly0 17423  mzpexpmpt 19779  pell14qrexpclnn0 19935  pellfund14 19969  rmxy0 19994  jm2.17a 20033  jm2.17b 20034  rpexp1i 20066  jm2.18 20069  jm2.23 20077  expdioph 20104  aaliou3lem2 20348  cnsrexpcl 20654
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-rep 3469  ax-sep 3479  ax-nul 3488  ax-pow 3524  ax-pr 3548  ax-un 3823  ax-resscn 7266  ax-1cn 7267  ax-icn 7268  ax-addcl 7269  ax-addrcl 7270  ax-mulcl 7271  ax-mulrcl 7272  ax-mulcom 7273  ax-addass 7274  ax-mulass 7275  ax-distr 7276  ax-i2m1 7277  ax-1ne0 7278  ax-1rid 7279  ax-rnegex 7280  ax-rrecex 7281  ax-cnre 7282  ax-pre-lttri 7283  ax-pre-lttrn 7284  ax-pre-ltadd 7285  ax-pre-mulgt0 7286
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1309  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-nel 2038  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2328  df-sbc 2495  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-pss 2649  df-nul 2905  df-if 3012  df-pw 3072  df-sn 3089  df-pr 3090  df-tp 3091  df-op 3092  df-uni 3234  df-iun 3307  df-br 3384  df-opab 3438  df-tr 3453  df-eprel 3634  df-id 3637  df-po 3642  df-so 3656  df-fr 3676  df-we 3692  df-ord 3708  df-on 3709  df-lim 3710  df-suc 3711  df-om 3988  df-xp 4035  df-rel 4036  df-cnv 4037  df-co 4038  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fun 4043  df-fn 4044  df-f 4045  df-f1 4046  df-fo 4047  df-f1o 4048  df-fv 4049  df-ov 5004  df-oprab 5005  df-mpt 5165  df-mpt2 5166  df-iota 5407  df-rdg 5498  df-er 5673  df-en 5830  df-dom 5831  df-sdom 5832  df-riota 5987  df-pnf 7325  df-mnf 7326  df-xr 7327  df-ltxr 7328  df-le 7329  df-sub 7455  df-neg 7457  df-n 7921  df-z 8150  df-seq 8819  df-exp 8873
Copyright terms: Public domain