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

Theorem exp0 8624
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 8622 . . 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 1961 . . 3 |- 0 = 0
5 iftrue 3034 . . 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 2009 1 |- (A e. CC -> (A^0) = 1)
Colors of variables: wff set class
Syntax hints:   -> wi 4   = wceq 1457   e. wcel 1459  ifcif 3028  {csn 3098   class class class wbr 3379   X. cxp 4006  ` cfv 4020  (class class class)co 4935  CCcc 6997  0cc0 6999  1c1 7000   x. cmul 7004   < clt 7111  -ucneg 7222   / cdiv 7223  NNcn 7224  ZZcz 7226   seq cseq 8568  ^cexp 8620
This theorem is referenced by:  expp1 8626  expneg 8627  expcllem 8630  mulexp 8653  expadd 8656  expmul 8659  expmwordi 8671  exple1 8672  bernneq 8732  modexp 8740  faclbnd 8766  faclbnd3 8768  faclbnd4lem1 8769  faclbnd4lem3 8771  faclbnd4lem4 8772  faclbnd6 8775  hashmap 8822  cjexp 8911  absexp 9041  binom 9293  climcndslem1 9310  geoser 9321  cvgrat 9332  ef0lem 9353  ege2le3 9363  efexp 9373  eft0val 9383  demoivreALT 9452  phiprm 9691  oddvds 9702  pclem 9731  pcpre1 9735  pcmpt 9760  prmpwdvds 9769  4001lem1 9876  expcn 11317  iblcnlem1 12160  itgcnlem 12162  dvexp 12241  plyconst 12266  plyeq0lem 12270  plyco 12300  0dgr 12304  0dgrb 12305  coefv0 12306  dgreq0 12323  vieta1 12359  cxpexp 12490  cxp0 12492  cxpmul2 12508  basellem2 12526  basellem5 12529  bpoly0 14980
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 1672  ax-ext 1943  ax-rep 3465  ax-sep 3475  ax-nul 3484  ax-pow 3520  ax-pr 3544  ax-un 3814  ax-resscn 7053  ax-1cn 7054  ax-icn 7055  ax-addcl 7056  ax-addrcl 7057  ax-mulcl 7058  ax-mulrcl 7059  ax-mulcom 7060  ax-addass 7061  ax-mulass 7062  ax-distr 7063  ax-i2m1 7064  ax-1ne0 7065  ax-1rid 7066  ax-rnegex 7067  ax-rrecex 7068  ax-cnre 7069  ax-pre-lttri 7070  ax-pre-lttrn 7071  ax-pre-ltadd 7072  ax-pre-mulgt0 7073
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 1634  df-eu 1861  df-mo 1862  df-clab 1949  df-cleq 1954  df-clel 1957  df-ne 2081  df-nel 2082  df-ral 2174  df-rex 2175  df-reu 2176  df-rab 2177  df-v 2368  df-sbc 2533  df-csb 2607  df-dif 2666  df-un 2668  df-in 2670  df-ss 2672  df-pss 2674  df-nul 2928  df-if 3029  df-pw 3087  df-sn 3102  df-pr 3103  df-tp 3105  df-op 3106  df-uni 3235  df-iun 3307  df-br 3380  df-opab 3434  df-tr 3449  df-eprel 3627  df-id 3630  df-po 3635  df-so 3649  df-fr 3668  df-we 3684  df-ord 3700  df-on 3701  df-lim 3702  df-suc 3703  df-om 3975  df-xp 4022  df-rel 4023  df-cnv 4024  df-co 4025  df-dm 4026  df-rn 4027  df-res 4028  df-ima 4029  df-fun 4030  df-fn 4031  df-f 4032  df-f1 4033  df-fo 4034  df-f1o 4035  df-fv 4036  df-ov 4937  df-oprab 4938  df-mpt 5072  df-mpt2 5073  df-iota 5273  df-rdg 5359  df-er 5533  df-en 5678  df-dom 5679  df-sdom 5680  df-riota 5821  df-pnf 7112  df-mnf 7113  df-xr 7114  df-ltxr 7115  df-le 7116  df-sub 7240  df-neg 7242  df-n 7704  df-z 7918  df-seq 8569  df-exp 8621
Copyright terms: Public domain