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

Theorem exp0 8583
Description: Value of a complex number raised to the 0th power. Note that under our definition, 0^0 = 1, 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 |- (A e. CC -> (A^0) = 1)

Proof of Theorem exp0
StepHypRef Expression
1 0z 7888 . . 3 |- 0 e. ZZ
2 expval 8581 . . 3 |- ((A e. CC /\ 0 e. ZZ) -> (A^0) = if(0 = 0, 1, if(0 < 0, ( seq 1( x. , (NN X. {A}))` 0), (1 / ( seq 1( x. , (NN X. {A}))` -u0)))))
31, 2mpan2 678 . 2 |- (A e. CC -> (A^0) = if(0 = 0, 1, if(0 < 0, ( seq 1( x. , (NN X. {A}))` 0), (1 / ( seq 1( x. , (NN X. {A}))` -u0)))))
4 eqid 1960 . . 3 |- 0 = 0
5 iftrue 3033 . . 3 |- (0 = 0 -> if(0 = 0, 1, if(0 < 0, ( seq 1( x. , (NN X. {A}))` 0), (1 / ( seq 1( x. , (NN X. {A}))` -u0)))) = 1)
64, 5ax-mp 8 . 2 |- if(0 = 0, 1, if(0 < 0, ( seq 1( x. , (NN X. {A}))` 0), (1 / ( seq 1( x. , (NN X. {A}))` -u0)))) = 1
73, 6syl6eq 2008 1 |- (A e. CC -> (A^0) = 1)
Colors of variables: wff set class
Syntax hints:   -> wi 4   = wceq 1457   e. wcel 1459  ifcif 3027  {csn 3097   class class class wbr 3378   X. cxp 4000  ` cfv 4014  (class class class)co 4928  CCcc 6962  0cc0 6964  1c1 6965   x. cmul 6969   < clt 7076  -ucneg 7187   / cdiv 7188  NNcn 7189  ZZcz 7191   seq cseq 8527  ^cexp 8579
This theorem is referenced by:  expp1 8585  expneg 8586  expcllem 8589  mulexp 8612  expadd 8615  expmul 8618  expmwordi 8630  exple1 8631  bernneq 8691  modexp 8699  faclbnd 8725  faclbnd3 8727  faclbnd4lem1 8728  faclbnd4lem3 8730  faclbnd4lem4 8731  faclbnd6 8734  hashpw 8782  cjexp 8868  absexp 8998  binom 9249  climcndslem1 9266  geoser 9276  cvgrat 9287  ef0lem 9335  ege2le3 9345  efexp 9355  eft0val 9365  demoivreALT 9438  phiprm 9675  oddvds 9686  pclem 9715  pcpre1 9719  pcmpt 9744  prmpwdvds 9753  4001lem1 9852  expcn 11280  plyconst 13579  plyeq0lem 13584  plyco 13614  0dgr 13618  0dgrb 13619  coefv0 13620  dgreq0 13637  vieta1 13672  basellem2 13688  basellem5 13691  iblrelem0 13903  bpoly0 14769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-13 1465  ax-14 1466  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-rep 3464  ax-sep 3474  ax-nul 3483  ax-pow 3519  ax-pr 3543  ax-un 3813  ax-resscn 7018  ax-1cn 7019  ax-icn 7020  ax-addcl 7021  ax-addrcl 7022  ax-mulcl 7023  ax-mulrcl 7024  ax-mulcom 7025  ax-addass 7026  ax-mulass 7027  ax-distr 7028  ax-i2m1 7029  ax-1ne0 7030  ax-1rid 7031  ax-rnegex 7032  ax-rrecex 7033  ax-cnre 7034  ax-pre-lttri 7035  ax-pre-lttrn 7036  ax-pre-ltadd 7037  ax-pre-mulgt0 7038
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3or 947  df-3an 948  df-tru 1354  df-ex 1381  df-sb 1633  df-eu 1860  df-mo 1861  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-nel 2081  df-ral 2173  df-rex 2174  df-reu 2175  df-rab 2176  df-v 2367  df-sbc 2532  df-csb 2606  df-dif 2665  df-un 2667  df-in 2669  df-ss 2671  df-pss 2673  df-nul 2927  df-if 3028  df-pw 3086  df-sn 3101  df-pr 3102  df-tp 3104  df-op 3105  df-uni 3234  df-iun 3306  df-br 3379  df-opab 3433  df-tr 3448  df-eprel 3626  df-id 3629  df-po 3634  df-so 3648  df-fr 3667  df-we 3683  df-ord 3699  df-on 3700  df-lim 3701  df-suc 3702  df-om 3969  df-xp 4016  df-rel 4017  df-cnv 4018  df-co 4019  df-dm 4020  df-rn 4021  df-res 4022  df-ima 4023  df-fun 4024  df-fn 4025  df-f 4026  df-f1 4027  df-fo 4028  df-f1o 4029  df-fv 4030  df-ov 4930  df-oprab 4931  df-mpt 5065  df-mpt2 5066  df-iota 5238  df-rdg 5324  df-er 5498  df-en 5643  df-dom 5644  df-sdom 5645  df-riota 5786  df-pnf 7077  df-mnf 7078  df-xr 7079  df-ltxr 7080  df-le 7081  df-sub 7205  df-neg 7207  df-n 7665  df-z 7879  df-seq 8528  df-exp 8580
Copyright terms: Public domain