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

Theorem exp0 8640
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 7936 . . 3
2 expval 8638 . . 3
31, 2mpan2 651 . 2
4 eqid 1929 . . 3
5 iftrue 3010 . . 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 3004  csn 3074   class class class wbr 3358   cxp 3989  cfv 4003  (class class class)co 4924  cc 7004  cc0 7006  c1 7007   cmul 7011   clt 7118  cneg 7230   cdiv 7231  cn 7232  cz 7234   cseq 8584  cexp 8636
This theorem is referenced by:  expp1 8642  expneg 8643  expcllem 8646  mulexp 8670  expadd 8673  expmul 8676  expmwordi 8688  exple1 8689  bernneq 8749  modexp 8757  faclbnd 8783  faclbnd3 8785  faclbnd4lem1 8786  faclbnd4lem3 8788  faclbnd4lem4 8789  faclbnd6 8792  hashmap 8840  cjexp 8925  absexp 9056  binom 9375  climcndslem1 9392  geoser 9404  cvgrat 9415  ef0lem 9436  ege2le3 9446  efexp 9456  eft0val 9466  demoivreALT 9536  phiprm 9778  oddvds 9789  pclem 9818  pcpre1 9822  pcmpt 9853  prmpwdvds 9862  4001lem1 10003  expcn 11502  iblcnlem1 12381  itgcnlem 12383  dvexp 12491  plyconst 12551  plyeq0lem 12555  plyco 12585  0dgr 12589  0dgrb 12590  coefv0 12591  dgreq0 12608  vieta1 12647  cxpexp 12792  cxp0 12794  cxpmul2 12812  ftalem5 12908  basellem2 12913  basellem5 12916  bposlem5 12935  chebbnd1lem1 12941  qabvexp 12964  ostth2lem2 12972  ostth3 12976  bpoly0 15393  mzpexpmpt 17589  pell14qrexpclnn0 17754  pellfund14 17788  rmxy0 17813  jm2.17a 17852  jm2.17b 17853  rpexp1i 17886  jm2.18 17889  jm2.23 17897  expdioph 17924  dvexp2 18097  aaliou3lem2 18128
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 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3795  ax-resscn 7060  ax-1cn 7061  ax-icn 7062  ax-addcl 7063  ax-addrcl 7064  ax-mulcl 7065  ax-mulrcl 7066  ax-mulcom 7067  ax-addass 7068  ax-mulass 7069  ax-distr 7070  ax-i2m1 7071  ax-1ne0 7072  ax-1rid 7073  ax-rnegex 7074  ax-rrecex 7075  ax-cnre 7076  ax-pre-lttri 7077  ax-pre-lttrn 7078  ax-pre-ltadd 7079  ax-pre-mulgt0 7080
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 2577  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-pss 2645  df-nul 2900  df-if 3005  df-pw 3063  df-sn 3080  df-pr 3081  df-tp 3082  df-op 3083  df-uni 3214  df-iun 3286  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3649  df-we 3665  df-ord 3681  df-on 3682  df-lim 3683  df-suc 3684  df-om 3958  df-xp 4005  df-rel 4006  df-cnv 4007  df-co 4008  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fun 4013  df-fn 4014  df-f 4015  df-f1 4016  df-fo 4017  df-f1o 4018  df-fv 4019  df-ov 4926  df-oprab 4927  df-mpt 5063  df-mpt2 5064  df-iota 5277  df-rdg 5363  df-er 5537  df-en 5682  df-dom 5683  df-sdom 5684  df-riota 5825  df-pnf 7119  df-mnf 7120  df-xr 7121  df-ltxr 7122  df-le 7123  df-sub 7248  df-neg 7250  df-n 7713  df-z 7927  df-seq 8585  df-exp 8637
Copyright terms: Public domain