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

Theorem exp0 9833
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 9036 . . 3
2 expval 9831 . . 3
31, 2mpan2 647 . 2
4 eqid 2090 . . 3
5 iftrue 3200 . . 3
64, 5ax-mp 8 . 2
73, 6syl6eq 2138 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1531   wcel 1533  cif 3194  csn 3268   class class class wbr 3591   cxp 4247  cfv 4261  (class class class)co 5296  cc 8059  cc0 8061  c1 8062   cmul 8066   clt 8178  cneg 8296   cdiv 8297  cn 8298  cz 8300   cseq 9774  cexp 9829
This theorem is referenced by:  expp1  9835  expneg  9836  expcllem  9839  mulexp  9866  expadd  9869  expmul  9872  expmwordi  9884  exple1  9885  bernneq  9945  modexp  9954  faclbnd  9981  faclbnd3  9983  faclbnd4lem1  9984  faclbnd4lem3  9986  faclbnd4lem4  9987  faclbnd6  9990  hashmap  10048  cjexp  10143  absexp  10275  binom  10614  climcndslem1  10631  geoser  10646  cvgrat  10658  ef0lem  10679  ege2le3  10689  efexp  10699  eft0val  10709  demoivreALT  10792  prmdvdsexpr  11024  phiprm  11044  odzdvds  11059  pclem  11090  pcpre1  11094  pcexp  11110  prmpwdvds  11149  numexp0  11289  decsplit0b  11293  pgp0  12183  sylow2alem2  12202  cnfldexp  13354  expmhm  13381  expcn  14419  iblcnlem1  14970  itgcnlem  14972  dvexp  15104  dvexp2  15105  plyconst  15358  plyeq0lem  15362  plyco  15393  0dgr  15397  0dgrb  15398  coefv0  15399  dgreq0  15416  vieta1  15455  abelthlem9  15531  cxpexp  15714  cxp0  15716  cxpmul2  15735  1cubr  15759  log2ublem3  15865  ftalem5  15918  basellem2  15923  basellem5  15926  0sgm  15967  musum  16004  bposlem5  16028  lgsval2lem  16046  lgsmod  16061  lgsdilem2  16071  lgsne0  16073  lgsquad2lem2  16093  chebbnd1lem1  16112  qabvexp  16132  ostth2lem2  16140  ostth3  16144  subfacval2  18398  bpoly0  19478  mzpexpmpt  21567  pell14qrexpclnn0  21724  pellfund14  21758  rmxy0  21783  jm2.17a  21822  jm2.17b  21823  rpexp1i  21855  jm2.18  21858  jm2.23  21866  expdioph  21893  aaliou3lem2  21971  cnsrexpcl  22192
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049  ax-resscn 8117  ax-1cn 8118  ax-icn 8119  ax-addcl 8120  ax-addrcl 8121  ax-mulcl 8122  ax-mulrcl 8123  ax-mulcom 8124  ax-addass 8125  ax-mulass 8126  ax-distr 8127  ax-i2m1 8128  ax-1ne0 8129  ax-1rid 8130  ax-rnegex 8131  ax-rrecex 8132  ax-cnre 8133  ax-pre-lttri 8134  ax-pre-lttrn 8135  ax-pre-ltadd 8136  ax-pre-mulgt0 8137
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1264  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-nel 2210  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-csb 2751  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-tp 3276  df-op 3277  df-uni 3435  df-iun 3511  df-br 3592  df-opab 3645  df-tr 3660  df-eprel 3844  df-id 3848  df-po 3853  df-so 3854  df-fr 3891  df-we 3893  df-ord 3934  df-on 3935  df-lim 3936  df-suc 3937  df-om 4216  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-ov 5298  df-oprab 5299  df-mpt 5461  df-mpt2 5462  df-iota 5740  df-recs 5814  df-rdg 5849  df-er 6076  df-en 6249  df-dom 6250  df-sdom 6251  df-riota 6415  df-pnf 8179  df-mnf 8180  df-xr 8181  df-ltxr 8182  df-le 8183  df-sub 8314  df-neg 8316  df-n 8782  df-z 9026  df-seq 9775  df-exp 9830
Copyright terms: Public domain