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

Theorem exp0 10115
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. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.)
Assertion
Ref Expression
exp0  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )

Proof of Theorem exp0
StepHypRef Expression
1 0z 9138 . . 3  |-  0  e.  ZZ
2 expval 10113 . . 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 } ) ) `  -u 0 ) ) ) ) )
31, 2mpan2 644 . 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 } ) ) `  -u 0 ) ) ) ) )
4 eqid 2062 . . 3  |-  0  =  0
5 iftrue 3185 . . 3  |-  ( 0  =  0  ->  if ( 0  =  0 ,  1 ,  if ( 0  <  0 ,  (  seq  1
(  x.  ,  ( NN  X.  { A } ) ) ` 
0 ) ,  ( 1  /  (  seq  1 (  x.  , 
( NN  X.  { A } ) ) `  -u 0 ) ) ) )  =  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 } ) ) `  -u 0 ) ) ) )  =  1
73, 6syl6eq 2110 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1518    e. wcel 1520   ifcif 3179   {csn 3253   class class class wbr 3584    X. cxp 4252   ` cfv 4266  (class class class)co 5356   CCcc 8151   0cc0 8153   1c1 8154    x. cmul 8158    < clt 8270   -ucneg 8390    / cdiv 8391   NNcn 8392   ZZcz 8394    seq cseq 10053   ^cexp 10111
This theorem is referenced by:  expp1  10117  expneg  10118  expcllem  10121  mulexp  10148  expadd  10151  expmul  10154  expmwordi  10167  exple1  10168  bernneq  10233  modexp  10242  faclbnd  10266  faclbnd3  10268  faclbnd4lem1  10269  faclbnd4lem3  10271  faclbnd4lem4  10272  faclbnd6  10275  facubnd  10276  hashmap  10349  cjexp  10445  absexp  10578  binom  10954  climcndslem1  10971  geoser  10987  cvgrat  10999  ef0lem  11020  ege2le3  11030  efexp  11040  eft0val  11050  demoivreALT  11133  prmdvdsexpr  11368  rpexp1i  11373  phiprm  11417  odzdvds  11432  pclem  11463  pcpre1  11467  pcexp  11483  prmpwdvds  11522  numexp0  11662  pgp0  13082  sylow2alem2  13104  ablfac1eu  13480  pgpfac1lem3  13483  cnfldexp  14577  expmhm  14619  expcn  16523  iblcnlem1  17284  itgcnlem  17286  dvexp  17418  dvexp2  17419  plyconst  17673  plyeq0lem  17677  plyco  17708  0dgr  17712  0dgrb  17713  coefv0  17714  dgreq0  17731  vieta1  17770  abelthlem9  17846  cxpexp  18033  cxp0  18035  cxpmul2  18054  1cubr  18090  log2ublem3  18196  ftalem5  18262  basellem2  18267  basellem5  18270  0sgm  18330  musum  18377  dchrptlem2  18438  bposlem5  18461  lgsval2lem  18479  lgsmod  18494  lgsdilem2  18504  lgsne0  18506  lgsquad2lem2  18532  chebbnd1lem1  18551  dchrisum0flblem1  18587  qabvexp  18619  ostth2lem2  18627  ostth3  18631  subfacval2  20882  bpoly0  21954  mzpexpmpt  23892  pell14qrexpclnn0  24018  pellfund14  24050  rmxy0  24075  jm2.17a  24114  jm2.17b  24115  jm2.18  24148  jm2.23  24156  expdioph  24183  aaliou3lem2  24259  cnsrexpcl  24480  psgnunilem4  24530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1440  ax-6 1441  ax-7 1442  ax-gen 1443  ax-8 1522  ax-11 1523  ax-13 1524  ax-14 1525  ax-17 1527  ax-12o 1560  ax-10 1574  ax-9 1580  ax-4 1587  ax-16 1773  ax-ext 2044  ax-sep 3699  ax-nul 3707  ax-pow 3743  ax-pr 3767  ax-un 4059  ax-resscn 8209  ax-1cn 8210  ax-icn 8211  ax-addcl 8212  ax-addrcl 8213  ax-mulcl 8214  ax-mulrcl 8215  ax-mulcom 8216  ax-addass 8217  ax-mulass 8218  ax-distr 8219  ax-i2m1 8220  ax-1ne0 8221  ax-1rid 8222  ax-rnegex 8223  ax-rrecex 8224  ax-cnre 8225  ax-pre-lttri 8226  ax-pre-lttrn 8227  ax-pre-ltadd 8228  ax-pre-mulgt0 8229
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 895  df-3an 896  df-tru 1257  df-ex 1445  df-sb 1734  df-eu 1956  df-mo 1957  df-clab 2050  df-cleq 2055  df-clel 2058  df-ne 2182  df-nel 2183  df-ral 2276  df-rex 2277  df-reu 2278  df-rab 2279  df-v 2475  df-sbc 2649  df-csb 2731  df-dif 2794  df-un 2796  df-in 2798  df-ss 2802  df-pss 2804  df-nul 3071  df-if 3180  df-pw 3241  df-sn 3259  df-pr 3260  df-tp 3261  df-op 3262  df-uni 3423  df-iun 3500  df-br 3585  df-opab 3639  df-mpt 3640  df-tr 3672  df-eprel 3854  df-id 3858  df-po 3863  df-so 3864  df-fr 3901  df-we 3903  df-ord 3944  df-on 3945  df-lim 3946  df-suc 3947  df-om 4222  df-xp 4268  df-rel 4269  df-cnv 4270  df-co 4271  df-dm 4272  df-rn 4273  df-res 4274  df-ima 4275  df-fun 4276  df-fn 4277  df-f 4278  df-f1 4279  df-fo 4280  df-f1o 4281  df-fv 4282  df-ov 5359  df-oprab 5360  df-mpt2 5361  df-iota 5766  df-recs 5839  df-rdg 5874  df-er 6111  df-en 6298  df-dom 6299  df-sdom 6300  df-riota 6464  df-pnf 8271  df-mnf 8272  df-xr 8273  df-ltxr 8274  df-le 8275  df-sub 8408  df-neg 8409  df-n 8883  df-z 9128  df-seq 10054  df-exp 10112
Copyright terms: Public domain