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

Theorem exp0 8744
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 8038 . . 3
2 expval 8742 . . 3
31, 2mpan2 646 . 2
4 eqid 1917 . . 3
5 iftrue 3009 . . 3
64, 5ax-mp 8 . 2
73, 6syl6eq 1965 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1413   wcel 1415  cif 3003  csn 3073   class class class wbr 3358   cxp 3993  cfv 4007  (class class class)co 4944  cc 7105  cc0 7107  c1 7108   cmul 7112   clt 7219  cneg 7331   cdiv 7332  cn 7333  cz 7335   cseq 8687  cexp 8740
This theorem is referenced by:  expp1 8746  expneg 8747  expcllem 8750  mulexp 8774  expadd 8777  expmul 8780  expmwordi 8792  exple1 8793  bernneq 8852  modexp 8860  faclbnd 8886  faclbnd3 8888  faclbnd4lem1 8889  faclbnd4lem3 8891  faclbnd4lem4 8892  faclbnd6 8895  hashmap 8949  cjexp 9038  absexp 9169  binom 9492  climcndslem1 9509  geoser 9521  cvgrat 9532  ef0lem 9553  ege2le3 9563  efexp 9573  eft0val 9583  demoivreALT 9653  prmdvdsexpr 9879  phiprm 9898  odzdvds 9912  pclem 9941  pcpre1 9945  prmpwdvds 9988  4001lem1 10129  expcn 12109  iblcnlem1 12988  itgcnlem 12990  dvexp 13098  plyconst 13158  plyeq0lem 13162  plyco 13192  0dgr 13196  0dgrb 13197  coefv0 13198  dgreq0 13215  vieta1 13254  cxpexp 13399  cxp0 13401  cxpmul2 13419  ftalem5 13515  basellem2 13520  basellem5 13523  bposlem5 13542  chebbnd1lem1 13548  qabvexp 13568  ostth2lem2 13576  ostth3 13580  pgp0 15163  sylow2alem2 15182  subfacval2 15219  bpoly0 16311  mzpexpmpt 18505  pell14qrexpclnn0 18664  pellfund14 18698  rmxy0 18723  jm2.17a 18762  jm2.17b 18763  rpexp1i 18796  jm2.18 18799  jm2.23 18807  expdioph 18834  dvexp2 19075  aaliou3lem2 19106  cnsrexpcl 19326
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797  ax-resscn 7161  ax-1cn 7162  ax-icn 7163  ax-addcl 7164  ax-addrcl 7165  ax-mulcl 7166  ax-mulrcl 7167  ax-mulcom 7168  ax-addass 7169  ax-mulass 7170  ax-distr 7171  ax-i2m1 7172  ax-1ne0 7173  ax-1rid 7174  ax-rnegex 7175  ax-rrecex 7176  ax-cnre 7177  ax-pre-lttri 7178  ax-pre-lttrn 7179  ax-pre-ltadd 7180  ax-pre-mulgt0 7181
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-tru 1308  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-nel 2037  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-sbc 2491  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-if 3004  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  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 3650  df-we 3666  df-ord 3682  df-on 3683  df-lim 3684  df-suc 3685  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 4946  df-oprab 4947  df-mpt 5106  df-mpt2 5107  df-iota 5336  df-rdg 5424  df-er 5598  df-en 5750  df-dom 5751  df-sdom 5752  df-riota 5896  df-pnf 7220  df-mnf 7221  df-xr 7222  df-ltxr 7223  df-le 7224  df-sub 7349  df-neg 7351  df-n 7814  df-z 8029  df-seq 8688  df-exp 8741
Copyright terms: Public domain