MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp0 Unicode version

Theorem exp0 10482
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 9423 . . 3  |-  0  e.  ZZ
2 expval 10480 . . 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 645 . 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 2069 . . 3  |-  0  =  0
5 iftrue 3192 . . 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 2117 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1524    e. wcel 1526   ifcif 3186   {csn 3260   class class class wbr 3596    X. cxp 4264   ` cfv 4278  (class class class)co 5370   CCcc 8166   0cc0 8168   1c1 8169    x. cmul 8173    < clt 8298   -ucneg 8463    / cdiv 8828   NNcn 9137   ZZcz 9412    seq cseq 10420   ^cexp 10478
This theorem is referenced by:  expp1  10484  expneg  10485  expcllem  10488  mulexp  10515  expadd  10518  expmul  10521  leexp1a  10534  exple1  10535  bernneq  10600  modexp  10609  exp0d  10612  faclbnd  10676  faclbnd3  10678  faclbnd4lem1  10679  faclbnd4lem3  10681  faclbnd4lem4  10682  facubnd  10686  hashmap  10759  cjexp  10849  absexp  11001  binom  11496  climcndslem1  11513  ef0lem  11563  ege2le3  11574  eft0val  11595  demoivreALT  11684  prmdvdsexpr  11920  numexp0  12216  pgp0  13637  sylow2alem2  13659  ablfac1eu  14037  pgpfac1lem3a  14040  cnfldexp  15135  expmhm  15177  expcn  17081  iblcnlem1  17843  itgcnlem  17845  dvexp  17977  dvexp2  17978  plyconst  18252  0dgr  18291  0dgrb  18292  coefv0  18293  cxpexp  18626  cxp0  18628  1cubr  18713  log2ublem3  18819  basellem2  18894  basellem5  18897  0sgm  18957  musum  19006  logexprlim  19039  lgsmod  19135  lgsquad2lem2  19173  ostth2lem2  19358  subfacval2  21615  bpoly0  22683  rmxy0  24837  expdioph  24945  aaliou3lem2  25021  psgnunilem4  25292
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1528  ax-11 1529  ax-13 1530  ax-14 1531  ax-17 1533  ax-12o 1567  ax-10 1581  ax-9 1587  ax-4 1594  ax-16 1780  ax-ext 2051  ax-sep 3711  ax-nul 3719  ax-pr 3779  ax-un 4071  ax-1cn 8225  ax-icn 8226  ax-addcl 8227  ax-addrcl 8228  ax-mulcl 8229  ax-mulrcl 8230  ax-i2m1 8235  ax-1ne0 8236  ax-rnegex 8238  ax-rrecex 8239  ax-cnre 8240
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 897  df-3an 898  df-ex 1451  df-sb 1741  df-eu 1963  df-mo 1964  df-clab 2057  df-cleq 2062  df-clel 2065  df-ne 2189  df-ral 2283  df-rex 2284  df-rab 2286  df-v 2482  df-sbc 2656  df-dif 2801  df-un 2803  df-in 2805  df-ss 2809  df-nul 3078  df-if 3187  df-sn 3266  df-pr 3267  df-op 3269  df-uni 3435  df-br 3597  df-opab 3651  df-mpt 3652  df-id 3870  df-xp 4280  df-rel 4281  df-cnv 4282  df-co 4283  df-dm 4284  df-rn 4285  df-res 4286  df-ima 4287  df-fun 4288  df-fv 4294  df-ov 5373  df-oprab 5374  df-mpt2 5375  df-recs 5853  df-rdg 5888  df-neg 8465  df-z 9413  df-seq 10421  df-exp 10479
  Copyright terms: Public domain W3C validator