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

Theorem exp0 9670
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 8877 . . 3
2 expval 9668 . . 3
31, 2mpan2 647 . 2
4 eqid 2030 . . 3
5 iftrue 3140 . . 3
64, 5ax-mp 8 . 2
73, 6syl6eq 2078 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1526   wcel 1528  cif 3134  csn 3208   class class class wbr 3531   cxp 4170  cfv 4184  (class class class)co 5206  cc 7906  cc0 7908  c1 7909   cmul 7913   clt 8021  cneg 8139   cdiv 8140  cn 8141  cz 8143   cseq 9611  cexp 9666
This theorem is referenced by:  expp1 9672  expneg 9673  expcllem 9676  mulexp 9703  expadd 9706  expmul 9709  expmwordi 9721  exple1 9722  bernneq 9782  modexp 9791  faclbnd 9818  faclbnd3 9820  faclbnd4lem1 9821  faclbnd4lem3 9823  faclbnd4lem4 9824  faclbnd6 9827  hashmap 9885  cjexp 9980  absexp 10112  binom 10449  climcndslem1 10466  geoser 10481  cvgrat 10493  ef0lem 10514  ege2le3 10524  efexp 10534  eft0val 10544  demoivreALT 10627  prmdvdsexpr 10856  phiprm 10876  odzdvds 10891  pclem 10922  pcpre1 10926  prmpwdvds 10969  numexp0 11109  pgp0 11995  sylow2alem2 12014  cnfldexp 13110  expmhm 13134  expcn 14165  iblcnlem1 14705  itgcnlem 14707  dvexp 14839  dvexp2 14840  plyconst 15086  plyeq0lem 15090  plyco 15120  0dgr 15124  0dgrb 15125  coefv0 15126  dgreq0 15143  vieta1 15182  abelthlem9 15258  cxpexp 15441  cxp0 15443  cxpmul2 15462  1cubr 15486  log2ublem3 15592  ftalem5 15635  basellem2 15640  basellem5 15643  bposlem5 15722  lgsval2lem 15740  lgsmod 15755  lgsdilem2 15765  lgsne0 15767  lgsquad2lem2 15787  chebbnd1lem1 15806  qabvexp 15826  ostth2lem2 15834  ostth3 15838  subfacval2 18110  bpoly0 19183  mzpexpmpt 21275  pell14qrexpclnn0 21432  pellfund14 21466  rmxy0 21491  jm2.17a 21530  jm2.17b 21531  rpexp1i 21563  jm2.18 21566  jm2.23 21574  expdioph 21601  aaliou3lem2 21685  cnsrexpcl 21890
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-13 1534  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-rep 3616  ax-sep 3626  ax-nul 3635  ax-pow 3671  ax-pr 3695  ax-un 3973  ax-resscn 7962  ax-1cn 7963  ax-icn 7964  ax-addcl 7965  ax-addrcl 7966  ax-mulcl 7967  ax-mulrcl 7968  ax-mulcom 7969  ax-addass 7970  ax-mulass 7971  ax-distr 7972  ax-i2m1 7973  ax-1ne0 7974  ax-1rid 7975  ax-rnegex 7976  ax-rrecex 7977  ax-cnre 7978  ax-pre-lttri 7979  ax-pre-lttrn 7980  ax-pre-ltadd 7981  ax-pre-mulgt0 7982
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1261  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-nel 2150  df-ral 2243  df-rex 2244  df-reu 2245  df-rab 2246  df-v 2442  df-sbc 2609  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-pss 2763  df-nul 3026  df-if 3135  df-pw 3196  df-sn 3214  df-pr 3215  df-tp 3216  df-op 3217  df-uni 3375  df-iun 3451  df-br 3532  df-opab 3585  df-tr 3600  df-eprel 3783  df-id 3787  df-po 3792  df-so 3806  df-fr 3826  df-we 3842  df-ord 3858  df-on 3859  df-lim 3860  df-suc 3861  df-om 4139  df-xp 4186  df-rel 4187  df-cnv 4188  df-co 4189  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fun 4194  df-fn 4195  df-f 4196  df-f1 4197  df-fo 4198  df-f1o 4199  df-fv 4200  df-ov 5208  df-oprab 5209  df-mpt 5371  df-mpt2 5372  df-iota 5647  df-recs 5722  df-rdg 5750  df-er 5952  df-en 6121  df-dom 6122  df-sdom 6123  df-riota 6281  df-pnf 8022  df-mnf 8023  df-xr 8024  df-ltxr 8025  df-le 8026  df-sub 8157  df-neg 8159  df-n 8625  df-z 8868  df-seq 9612  df-exp 9667
Copyright terms: Public domain