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

Theorem exp0 10923
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 9853 . . 3  |-  0  e.  ZZ
2 expval 10921 . . 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 649 . 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 2241 . . 3  |-  0  =  0
5 iftrue 3456 . . 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 9 . 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 2289 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 5    = wceq 1608    e. wcel 1610   ifcif 3450   {csn 3524   class class class wbr 3900    X. cxp 4557   ` cfv 4571  (class class class)co 5685   CCcc 8589   0cc0 8591   1c1 8592    x. cmul 8596    < clt 8721   -ucneg 8887    / cdiv 9255   NNcn 9566   ZZcz 9842    seq cseq 10861   ^cexp 10919
This theorem is referenced by:  expp1  10925  expneg  10926  expcllem  10929  mulexp  10956  expadd  10959  expmul  10962  leexp1a  10975  exple1  10976  bernneq  11041  modexp  11050  exp0d  11053  faclbnd  11117  faclbnd3  11119  faclbnd4lem1  11120  faclbnd4lem3  11122  faclbnd4lem4  11123  facubnd  11127  cjexp  11448  absexp  11600  binom  12099  climcndslem1  12116  ef0lem  12168  ege2le3  12179  eft0val  12200  demoivreALT  12289  bits0  12427  0bits  12438  bitsinv1  12441  sadcadd  12457  smumullem  12491  numexp0  12899  cnfldexp  16085  expmhm  16127  expcn  18054  iblcnlem1  18820  itgcnlem  18822  dvexp  18980  dvexp2  18981  plyconst  19266  0dgr  19305  0dgrb  19306  coefv0  19307  aaliou3lem2  19401  tayl0  19419  cxpexp  19701  cxp0  19703  1cubr  19788  log2ublem3  19894  basellem2  19969  basellem5  19972  musum  20081  logexprlim  20114  lgsquad2lem2  20248  subfacval2  22690  bpoly0  23765  psgnunilem4  26392
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9  ax-5 1522  ax-6 1523  ax-7 1524  ax-gen 1525  ax-8 1612  ax-11 1613  ax-13 1614  ax-14 1615  ax-17 1617  ax-12o 1653  ax-10 1667  ax-9 1673  ax-4 1681  ax-16 1915  ax-ext 2222  ax-sep 4017  ax-nul 4025  ax-pr 4087  ax-un 4382  ax-1cn 8649  ax-icn 8650  ax-addcl 8651  ax-addrcl 8652  ax-mulcl 8653  ax-mulrcl 8654  ax-i2m1 8659  ax-1ne0 8660  ax-rnegex 8662  ax-rrecex 8663  ax-cnre 8664
This theorem depends on definitions:  df-bi 176  df-or 358  df-an 359  df-3or 934  df-3an 935  df-tru 1309  df-ex 1527  df-nf 1529  df-sb 1872  df-eu 2106  df-mo 2107  df-clab 2228  df-cleq 2234  df-clel 2237  df-nfc 2362  df-ne 2402  df-ral 2499  df-rex 2500  df-rab 2502  df-v 2714  df-sbc 2907  df-dif 3061  df-un 3063  df-in 3065  df-ss 3069  df-nul 3343  df-if 3451  df-sn 3530  df-pr 3531  df-op 3533  df-uni 3708  df-br 3901  df-opab 3955  df-mpt 3956  df-id 4181  df-xp 4573  df-rel 4574  df-cnv 4575  df-co 4576  df-dm 4577  df-rn 4578  df-res 4579  df-ima 4580  df-fun 4581  df-fv 4587  df-ov 5688  df-oprab 5689  df-mpt2 5690  df-recs 6248  df-rdg 6283  df-neg 8889  df-z 9843  df-seq 10862  df-exp 10920
  Copyright terms: Public domain W3C validator