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

Theorem exp0 9016
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 8226 . . 3
2 expval 9014 . . 3
31, 2mpan2 647 . 2
4 eqid 1918 . . 3
5 iftrue 3020 . . 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 3014  csn 3086   class class class wbr 3396   cxp 4032  cfv 4046  (class class class)co 5032  cc 7255  cc0 7257  c1 7258   cmul 7262   clt 7370  cneg 7488   cdiv 7489  cn 7490  cz 7492   cseq 8958  cexp 9012
This theorem is referenced by:  expp1 9018  expneg 9019  expcllem 9022  mulexp 9047  expadd 9050  expmul 9053  expmwordi 9065  exple1 9066  bernneq 9126  modexp 9135  faclbnd 9161  faclbnd3 9163  faclbnd4lem1 9164  faclbnd4lem3 9166  faclbnd4lem4 9167  faclbnd6 9170  hashmap 9227  cjexp 9320  absexp 9452  binom 9791  climcndslem1 9808  geoser 9821  cvgrat 9833  ef0lem 9854  ege2le3 9864  efexp 9874  eft0val 9884  demoivreALT 9966  prmdvdsexpr 10195  phiprm 10214  odzdvds 10228  pclem 10258  pcpre1 10262  prmpwdvds 10305  numexp0 10445  expcn 12948  iblcnlem1 13887  itgcnlem 13889  dvexp 14021  dvexp2 14022  plyconst 14108  plyeq0lem 14112  plyco 14142  0dgr 14146  0dgrb 14147  coefv0 14148  dgreq0 14165  vieta1 14204  abelthlem9 14275  cxpexp 14451  cxp0 14453  cxpmul2 14472  1cubr 14494  log2ublem3 14597  ftalem5 14630  basellem2 14635  basellem5 14638  bposlem5 14717  chebbnd1lem1 14723  qabvexp 14743  ostth2lem2 14751  ostth3 14755  pgp0 16573  sylow2alem2 16592  subfacval2 16629  lgsval2lem 16665  lgsmod 16680  lgsdilem2 16690  lgsne0 16692  bpoly0 17737  mzpexpmpt 20180  pell14qrexpclnn0 20336  pellfund14 20370  rmxy0 20395  jm2.17a 20434  jm2.17b 20435  rpexp1i 20467  jm2.18 20470  jm2.23 20478  expdioph 20505  aaliou3lem2 20750  cnsrexpcl 21352
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 3481  ax-sep 3491  ax-nul 3500  ax-pow 3536  ax-pr 3560  ax-un 3836  ax-resscn 7311  ax-1cn 7312  ax-icn 7313  ax-addcl 7314  ax-addrcl 7315  ax-mulcl 7316  ax-mulrcl 7317  ax-mulcom 7318  ax-addass 7319  ax-mulass 7320  ax-distr 7321  ax-i2m1 7322  ax-1ne0 7323  ax-1rid 7324  ax-rnegex 7325  ax-rrecex 7326  ax-cnre 7327  ax-pre-lttri 7328  ax-pre-lttrn 7329  ax-pre-ltadd 7330  ax-pre-mulgt0 7331
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 2329  df-sbc 2496  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-pss 2650  df-nul 2908  df-if 3015  df-pw 3075  df-sn 3092  df-pr 3093  df-tp 3094  df-op 3095  df-uni 3247  df-iun 3320  df-br 3397  df-opab 3450  df-tr 3465  df-eprel 3646  df-id 3650  df-po 3655  df-so 3669  df-fr 3689  df-we 3705  df-ord 3721  df-on 3722  df-lim 3723  df-suc 3724  df-om 4001  df-xp 4048  df-rel 4049  df-cnv 4050  df-co 4051  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fun 4056  df-fn 4057  df-f 4058  df-f1 4059  df-fo 4060  df-f1o 4061  df-fv 4062  df-ov 5034  df-oprab 5035  df-mpt 5196  df-mpt2 5197  df-iota 5444  df-rdg 5535  df-er 5710  df-en 5869  df-dom 5870  df-sdom 5871  df-riota 6022  df-pnf 7371  df-mnf 7372  df-xr 7373  df-ltxr 7374  df-le 7375  df-sub 7506  df-neg 7508  df-n 7974  df-z 8217  df-seq 8959  df-exp 9013
Copyright terms: Public domain