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

Theorem exp0 10951
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 9881 . . 3  |-  0  e.  ZZ
2 expval 10949 . . 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 3473 . . 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 3467   {csn 3541   class class class wbr 3917    X. cxp 4575   ` cfv 4589  (class class class)co 5707   CCcc 8612   0cc0 8614   1c1 8615    x. cmul 8619    < clt 8744   -ucneg 8910    / cdiv 9279   NNcn 9594   ZZcz 9870    seq cseq 10889   ^cexp 10947
This theorem is referenced by:  expp1  10953  expneg  10954  expcllem  10957  mulexp  10984  expadd  10987  expmul  10990  leexp1a  11003  exple1  11004  bernneq  11069  modexp  11078  exp0d  11081  faclbnd  11145  faclbnd3  11147  faclbnd4lem1  11148  faclbnd4lem3  11150  faclbnd4lem4  11151  facubnd  11155  cjexp  11476  absexp  11628  binom  12127  climcndslem1  12144  ef0lem  12196  ege2le3  12207  eft0val  12228  demoivreALT  12317  bits0  12455  0bits  12466  bitsinv1  12469  sadcadd  12485  smumullem  12519  numexp0  12927  cnfldexp  16201  expmhm  16243  expcn  18170  iblcnlem1  18936  itgcnlem  18938  dvexp  19096  dvexp2  19097  plyconst  19382  0dgr  19421  0dgrb  19422  coefv0  19423  aaliou3lem2  19517  tayl0  19535  cxpexp  19817  cxp0  19819  1cubr  19904  log2ublem3  20010  basellem2  20085  basellem5  20088  musum  20197  logexprlim  20230  lgsquad2lem2  20364  subfacval2  22820  bpoly0  23890  psgnunilem4  26517
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 4035  ax-nul 4043  ax-pr 4105  ax-un 4400  ax-1cn 8672  ax-icn 8673  ax-addcl 8674  ax-addrcl 8675  ax-mulcl 8676  ax-mulrcl 8677  ax-i2m1 8682  ax-1ne0 8683  ax-rnegex 8685  ax-rrecex 8686  ax-cnre 8687
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 2511  df-rex 2512  df-rab 2514  df-v 2727  df-sbc 2920  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-nul 3360  df-if 3468  df-sn 3547  df-pr 3548  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-mpt 3973  df-id 4199  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fun 4599  df-fv 4605  df-ov 5710  df-oprab 5711  df-mpt2 5712  df-recs 6271  df-rdg 6306  df-neg 8912  df-z 9871  df-seq 10890  df-exp 10948
  Copyright terms: Public domain W3C validator