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

Theorem exp0 8810
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 8103 . . 3
2 expval 8808 . . 3
31, 2mpan2 647 . 2
4 eqid 1918 . . 3
5 iftrue 3014 . . 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 3008  csn 3079   class class class wbr 3370   cxp 4005  cfv 4019  (class class class)co 4979  cc 7168  cc0 7170  c1 7171   cmul 7175   clt 7282  cneg 7394   cdiv 7395  cn 7396  cz 7398   cseq 8753  cexp 8806
This theorem is referenced by:  expp1 8812  expneg 8813  expcllem 8816  mulexp 8840  expadd 8843  expmul 8846  expmwordi 8858  exple1 8859  bernneq 8918  modexp 8926  faclbnd 8952  faclbnd3 8954  faclbnd4lem1 8955  faclbnd4lem3 8957  faclbnd4lem4 8958  faclbnd6 8961  hashmap 9015  cjexp 9104  absexp 9235  binom 9558  climcndslem1 9575  geoser 9587  cvgrat 9598  ef0lem 9619  ege2le3 9629  efexp 9639  eft0val 9649  demoivreALT 9719  prmdvdsexpr 9946  phiprm 9965  odzdvds 9979  pclem 10008  pcpre1 10012  prmpwdvds 10055  4001lem1 10196  expcn 12256  iblcnlem1 13153  itgcnlem 13155  dvexp 13285  dvexp2 13286  plyconst 13348  plyeq0lem 13352  plyco 13382  0dgr 13386  0dgrb 13387  coefv0 13388  dgreq0 13405  vieta1 13444  cxpexp 13589  cxp0 13591  cxpmul2 13609  ftalem5 13705  basellem2 13710  basellem5 13713  bposlem5 13732  chebbnd1lem1 13738  qabvexp 13758  ostth2lem2 13766  ostth3 13770  pgp0 15363  sylow2alem2 15382  subfacval2 15419  lgsval2lem 15455  lgsmod 15470  lgsdilem2 15480  lgsne0 15482  bpoly0 16662  mzpexpmpt 19065  pell14qrexpclnn0 19221  pellfund14 19255  rmxy0 19280  jm2.17a 19319  jm2.17b 19320  rpexp1i 19353  jm2.18 19356  jm2.23 19364  expdioph 19391  aaliou3lem2 19639  cnsrexpcl 19948
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 3456  ax-sep 3466  ax-nul 3475  ax-pow 3511  ax-pr 3535  ax-un 3809  ax-resscn 7224  ax-1cn 7225  ax-icn 7226  ax-addcl 7227  ax-addrcl 7228  ax-mulcl 7229  ax-mulrcl 7230  ax-mulcom 7231  ax-addass 7232  ax-mulass 7233  ax-distr 7234  ax-i2m1 7235  ax-1ne0 7236  ax-1rid 7237  ax-rnegex 7238  ax-rrecex 7239  ax-cnre 7240  ax-pre-lttri 7241  ax-pre-lttrn 7242  ax-pre-ltadd 7243  ax-pre-mulgt0 7244
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 2326  df-sbc 2493  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-pss 2647  df-nul 2903  df-if 3009  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3224  df-iun 3297  df-br 3371  df-opab 3425  df-tr 3440  df-eprel 3620  df-id 3623  df-po 3628  df-so 3642  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3974  df-xp 4021  df-rel 4022  df-cnv 4023  df-co 4024  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fun 4029  df-fn 4030  df-f 4031  df-f1 4032  df-fo 4033  df-f1o 4034  df-fv 4035  df-ov 4981  df-oprab 4982  df-mpt 5142  df-mpt2 5143  df-iota 5377  df-rdg 5468  df-er 5643  df-en 5800  df-dom 5801  df-sdom 5802  df-riota 5951  df-pnf 7283  df-mnf 7284  df-xr 7285  df-ltxr 7286  df-le 7287  df-sub 7412  df-neg 7414  df-n 7877  df-z 8094  df-seq 8754  df-exp 8807
Copyright terms: Public domain