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

Theorem exp0 11341
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 10249 . . 3  |-  0  e.  ZZ
2 expval 11339 . . 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 653 . 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 2404 . . 3  |-  0  =  0
5 iftrue 3705 . . 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 2452 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   ifcif 3699   {csn 3774   class class class wbr 4172    X. cxp 4835   ` cfv 5413  (class class class)co 6040   CCcc 8944   0cc0 8946   1c1 8947    x. cmul 8951    < clt 9076   -ucneg 9248    / cdiv 9633   NNcn 9956   ZZcz 10238    seq cseq 11278   ^cexp 11337
This theorem is referenced by:  expp1  11343  expneg  11344  expcllem  11347  mulexp  11374  expadd  11377  expmul  11380  leexp1a  11393  exple1  11394  bernneq  11460  modexp  11469  exp0d  11472  faclbnd  11536  faclbnd3  11538  faclbnd4lem1  11539  faclbnd4lem3  11541  faclbnd4lem4  11542  facubnd  11546  cjexp  11910  absexp  12064  binom  12564  incexclem  12571  incexc  12572  climcndslem1  12584  ef0lem  12636  ege2le3  12647  eft0val  12668  demoivreALT  12757  bits0  12895  0bits  12906  bitsinv1  12909  sadcadd  12925  smumullem  12959  numexp0  13367  cnfldexp  16689  expmhm  16731  expcn  18855  iblcnlem1  19632  itgcnlem  19634  dvexp  19792  dvexp2  19793  plyconst  20078  0dgr  20117  0dgrb  20118  coefv0  20119  aaliou3lem2  20213  tayl0  20231  cxpexp  20512  cxp0  20514  1cubr  20635  log2ublem3  20741  basellem2  20817  basellem5  20820  musum  20929  logexprlim  20962  lgsquad2lem2  21096  subfacval2  24826  fprodconst  25255  fallfac0  25296  bpoly0  26000  psgnunilem4  27288  m1expeven  27592  stoweidlem19  27635
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-recs 6592  df-rdg 6627  df-neg 9250  df-z 10239  df-seq 11279  df-exp 11338
  Copyright terms: Public domain W3C validator