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

Theorem exp0 10986
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 9914 . . 3  |-  0  e.  ZZ
2 expval 10984 . . 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 655 . 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 2253 . . 3  |-  0  =  0
5 iftrue 3476 . . 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 10 . 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 2301 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   ifcif 3470   {csn 3544   class class class wbr 3920    X. cxp 4578   ` cfv 4592  (class class class)co 5710   CCcc 8615   0cc0 8617   1c1 8618    x. cmul 8622    < clt 8747   -ucneg 8918    / cdiv 9303   NNcn 9626   ZZcz 9903    seq cseq 10924   ^cexp 10982
This theorem is referenced by:  expp1  10988  expneg  10989  expcllem  10992  mulexp  11019  expadd  11022  expmul  11025  leexp1a  11038  exple1  11039  bernneq  11105  modexp  11114  exp0d  11117  faclbnd  11181  faclbnd3  11183  faclbnd4lem1  11184  faclbnd4lem3  11186  faclbnd4lem4  11187  facubnd  11191  cjexp  11512  absexp  11666  binom  12165  climcndslem1  12182  ef0lem  12234  ege2le3  12245  eft0val  12266  demoivreALT  12355  bits0  12493  0bits  12504  bitsinv1  12507  sadcadd  12523  smumullem  12557  numexp0  12965  cnfldexp  16239  expmhm  16281  expcn  18208  iblcnlem1  18974  itgcnlem  18976  dvexp  19134  dvexp2  19135  plyconst  19420  0dgr  19459  0dgrb  19460  coefv0  19461  aaliou3lem2  19555  tayl0  19573  cxpexp  19847  cxp0  19849  1cubr  19970  log2ublem3  20076  basellem2  20151  basellem5  20154  musum  20263  logexprlim  20296  lgsquad2lem2  20430  subfacval2  22889  bpoly0  23959  psgnunilem4  26586  stoweidlem19  26902
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108  ax-un 4403  ax-1cn 8675  ax-icn 8676  ax-addcl 8677  ax-addrcl 8678  ax-mulcl 8679  ax-mulrcl 8680  ax-i2m1 8685  ax-1ne0 8686  ax-rnegex 8688  ax-rrecex 8689  ax-cnre 8690
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-mpt 3976  df-id 4202  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fv 4608  df-ov 5713  df-oprab 5714  df-mpt2 5715  df-recs 6274  df-rdg 6309  df-neg 8920  df-z 9904  df-seq 10925  df-exp 10983
  Copyright terms: Public domain W3C validator