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

Theorem exp0 8657
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 7952 . . 3
2 expval 8655 . . 3
31, 2mpan2 651 . 2
4 eqid 1929 . . 3
5 iftrue 3014 . . 3
64, 5ax-mp 8 . 2
73, 6syl6eq 1977 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1425   wcel 1427  cif 3008  csn 3078   class class class wbr 3362   cxp 3993  cfv 4007  (class class class)co 4931  cc 7020  cc0 7022  c1 7023   cmul 7027   clt 7134  cneg 7246   cdiv 7247  cn 7248  cz 7250   cseq 8600  cexp 8653
This theorem is referenced by:  expp1 8659  expneg 8660  expcllem 8663  mulexp 8687  expadd 8690  expmul 8693  expmwordi 8705  exple1 8706  bernneq 8766  modexp 8774  faclbnd 8800  faclbnd3 8802  faclbnd4lem1 8803  faclbnd4lem3 8805  faclbnd4lem4 8806  faclbnd6 8809  hashmap 8857  cjexp 8943  absexp 9074  binom 9393  climcndslem1 9410  geoser 9422  cvgrat 9433  ef0lem 9454  ege2le3 9464  efexp 9474  eft0val 9484  demoivreALT 9554  phiprm 9796  oddvds 9807  pclem 9836  pcpre1 9840  pcmpt 9871  prmpwdvds 9880  4001lem1 10021  expcn 11768  iblcnlem1 12647  itgcnlem 12649  dvexp 12757  plyconst 12817  plyeq0lem 12821  plyco 12851  0dgr 12855  0dgrb 12856  coefv0 12857  dgreq0 12874  vieta1 12913  cxpexp 13058  cxp0 13060  cxpmul2 13078  ftalem5 13174  basellem2 13179  basellem5 13182  bposlem5 13201  chebbnd1lem1 13207  qabvexp 13227  ostth2lem2 13235  ostth3 13239  bpoly0 15786  mzpexpmpt 17982  pell14qrexpclnn0 18146  pellfund14 18180  rmxy0 18205  jm2.17a 18244  jm2.17b 18245  rpexp1i 18278  jm2.18 18281  jm2.23 18289  expdioph 18316  dvexp2 18489  aaliou3lem2 18520  cnsrexpcl 18691
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-rep 3448  ax-sep 3458  ax-nul 3467  ax-pow 3503  ax-pr 3527  ax-un 3799  ax-resscn 7076  ax-1cn 7077  ax-icn 7078  ax-addcl 7079  ax-addrcl 7080  ax-mulcl 7081  ax-mulrcl 7082  ax-mulcom 7083  ax-addass 7084  ax-mulass 7085  ax-distr 7086  ax-i2m1 7087  ax-1ne0 7088  ax-1rid 7089  ax-rnegex 7090  ax-rrecex 7091  ax-cnre 7092  ax-pre-lttri 7093  ax-pre-lttrn 7094  ax-pre-ltadd 7095  ax-pre-mulgt0 7096
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-tru 1320  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-nel 2050  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-sbc 2502  df-csb 2579  df-dif 2641  df-un 2643  df-in 2645  df-ss 2647  df-pss 2649  df-nul 2904  df-if 3009  df-pw 3067  df-sn 3084  df-pr 3085  df-tp 3086  df-op 3087  df-uni 3218  df-iun 3290  df-br 3363  df-opab 3417  df-tr 3432  df-eprel 3612  df-id 3615  df-po 3620  df-so 3634  df-fr 3653  df-we 3669  df-ord 3685  df-on 3686  df-lim 3687  df-suc 3688  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-ov 4933  df-oprab 4934  df-mpt 5070  df-mpt2 5071  df-iota 5290  df-rdg 5376  df-er 5550  df-en 5695  df-dom 5696  df-sdom 5697  df-riota 5839  df-pnf 7135  df-mnf 7136  df-xr 7137  df-ltxr 7138  df-le 7139  df-sub 7264  df-neg 7266  df-n 7729  df-z 7943  df-seq 8601  df-exp 8654
Copyright terms: Public domain