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

Theorem exp0 8626
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 7927 . . 3 |- 0 e. ZZ
2 expval 8624 . . 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 669 . 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 1953 . . 3 |- 0 = 0
5 iftrue 3028 . . 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 2001 1 |- (A e. CC -> (A^0) = 1)
Colors of variables: wff set class
Syntax hints:   -> wi 4   = wceq 1449   e. wcel 1451  ifcif 3022  {csn 3092   class class class wbr 3373   X. cxp 4002  ` cfv 4016  (class class class)co 4931  CCcc 6996  0cc0 6998  1c1 6999   x. cmul 7003   < clt 7110  -ucneg 7222   / cdiv 7223  NNcn 7224  ZZcz 7226   seq cseq 8570  ^cexp 8622
This theorem is referenced by:  expp1 8628  expneg 8629  expcllem 8632  mulexp 8656  expadd 8659  expmul 8662  expmwordi 8674  exple1 8675  bernneq 8735  modexp 8743  faclbnd 8769  faclbnd3 8771  faclbnd4lem1 8772  faclbnd4lem3 8774  faclbnd4lem4 8775  faclbnd6 8778  hashmap 8826  cjexp 8911  absexp 9042  binom 9309  climcndslem1 9326  geoser 9337  cvgrat 9348  ef0lem 9369  ege2le3 9379  efexp 9389  eft0val 9399  demoivreALT 9468  phiprm 9707  oddvds 9718  pclem 9747  pcpre1 9751  pcmpt 9782  prmpwdvds 9791  4001lem1 9898  expcn 11382  iblcnlem1 12259  itgcnlem 12261  dvexp 12369  plyconst 12429  plyeq0lem 12433  plyco 12463  0dgr 12467  0dgrb 12468  coefv0 12469  dgreq0 12486  vieta1 12522  cxpexp 12653  cxp0 12655  cxpmul2 12672  basellem2 12694  basellem5 12697  qabvexp 12743  ostth2lem2 12751  ostth3 12755  bpoly0 15177
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-13 1457  ax-14 1458  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-rep 3459  ax-sep 3469  ax-nul 3478  ax-pow 3514  ax-pr 3538  ax-un 3808  ax-resscn 7052  ax-1cn 7053  ax-icn 7054  ax-addcl 7055  ax-addrcl 7056  ax-mulcl 7057  ax-mulrcl 7058  ax-mulcom 7059  ax-addass 7060  ax-mulass 7061  ax-distr 7062  ax-i2m1 7063  ax-1ne0 7064  ax-1rid 7065  ax-rnegex 7066  ax-rrecex 7067  ax-cnre 7068  ax-pre-lttri 7069  ax-pre-lttrn 7070  ax-pre-ltadd 7071  ax-pre-mulgt0 7072
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3or 938  df-3an 939  df-tru 1345  df-ex 1372  df-sb 1626  df-eu 1853  df-mo 1854  df-clab 1941  df-cleq 1946  df-clel 1949  df-ne 2073  df-nel 2074  df-ral 2166  df-rex 2167  df-reu 2168  df-rab 2169  df-v 2360  df-sbc 2525  df-csb 2600  df-dif 2660  df-un 2662  df-in 2664  df-ss 2666  df-pss 2668  df-nul 2922  df-if 3023  df-pw 3081  df-sn 3096  df-pr 3097  df-tp 3099  df-op 3100  df-uni 3229  df-iun 3301  df-br 3374  df-opab 3428  df-tr 3443  df-eprel 3621  df-id 3624  df-po 3629  df-so 3643  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3971  df-xp 4018  df-rel 4019  df-cnv 4020  df-co 4021  df-dm 4022  df-rn 4023  df-res 4024  df-ima 4025  df-fun 4026  df-fn 4027  df-f 4028  df-f1 4029  df-fo 4030  df-f1o 4031  df-fv 4032  df-ov 4933  df-oprab 4934  df-mpt 5068  df-mpt2 5069  df-iota 5270  df-rdg 5356  df-er 5530  df-en 5675  df-dom 5676  df-sdom 5677  df-riota 5818  df-pnf 7111  df-mnf 7112  df-xr 7113  df-ltxr 7114  df-le 7115  df-sub 7240  df-neg 7242  df-n 7704  df-z 7918  df-seq 8571  df-exp 8623
Copyright terms: Public domain