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

Theorem exp0 10516
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 9457 . . 3  |-  0  e.  ZZ
2 expval 10514 . . 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 647 . 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 2100 . . 3  |-  0  =  0
5 iftrue 3226 . . 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 2148 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1531    e. wcel 1533   ifcif 3220   {csn 3294   class class class wbr 3630    X. cxp 4298   ` cfv 4312  (class class class)co 5404   CCcc 8200   0cc0 8202   1c1 8203    x. cmul 8207    < clt 8332   -ucneg 8497    / cdiv 8862   NNcn 9171   ZZcz 9446    seq cseq 10454   ^cexp 10512
This theorem is referenced by:  expp1  10518  expneg  10519  expcllem  10522  mulexp  10549  expadd  10552  expmul  10555  leexp1a  10568  exple1  10569  bernneq  10634  modexp  10643  exp0d  10646  faclbnd  10710  faclbnd3  10712  faclbnd4lem1  10713  faclbnd4lem3  10715  faclbnd4lem4  10716  facubnd  10720  cjexp  10883  absexp  11035  binom  11530  climcndslem1  11547  ef0lem  11597  ege2le3  11608  eft0val  11629  demoivreALT  11718  numexp0  12250  cnfldexp  15169  expmhm  15211  expcn  17115  iblcnlem1  17877  itgcnlem  17879  dvexp  18011  dvexp2  18012  plyconst  18286  0dgr  18325  0dgrb  18326  coefv0  18327  cxpexp  18660  cxp0  18662  1cubr  18747  log2ublem3  18853  basellem2  18928  basellem5  18931  musum  19040  logexprlim  19073  lgsquad2lem2  19207  subfacval2  21649  bpoly0  22717  aaliou3lem2  25084  psgnunilem4  25355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-7 1454  ax-gen 1455  ax-8 1535  ax-11 1536  ax-13 1537  ax-14 1538  ax-17 1540  ax-12o 1574  ax-10 1588  ax-9 1594  ax-4 1601  ax-16 1787  ax-ext 2082  ax-sep 3745  ax-nul 3753  ax-pr 3813  ax-un 4105  ax-1cn 8259  ax-icn 8260  ax-addcl 8261  ax-addrcl 8262  ax-mulcl 8263  ax-mulrcl 8264  ax-i2m1 8269  ax-1ne0 8270  ax-rnegex 8272  ax-rrecex 8273  ax-cnre 8274
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 901  df-3an 902  df-ex 1457  df-sb 1748  df-eu 1970  df-mo 1971  df-clab 2088  df-cleq 2093  df-clel 2096  df-ne 2220  df-ral 2315  df-rex 2316  df-rab 2318  df-v 2514  df-sbc 2688  df-dif 2833  df-un 2835  df-in 2837  df-ss 2841  df-nul 3111  df-if 3221  df-sn 3300  df-pr 3301  df-op 3303  df-uni 3469  df-br 3631  df-opab 3685  df-mpt 3686  df-id 3904  df-xp 4314  df-rel 4315  df-cnv 4316  df-co 4317  df-dm 4318  df-rn 4319  df-res 4320  df-ima 4321  df-fun 4322  df-fv 4328  df-ov 5407  df-oprab 5408  df-mpt2 5409  df-recs 5887  df-rdg 5922  df-neg 8499  df-z 9447  df-seq 10455  df-exp 10513
  Copyright terms: Public domain W3C validator