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

Theorem exp0 11853
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 10645 . . 3  |-  0  e.  ZZ
2 expval 11851 . . 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 664 . 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 2433 . . 3  |-  0  =  0
54iftruei 3786 . 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
63, 5syl6eq 2481 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755   ifcif 3779   {csn 3865   class class class wbr 4280    X. cxp 4825   ` cfv 5406  (class class class)co 6080   CCcc 9268   0cc0 9270   1c1 9271    x. cmul 9275    < clt 9406   -ucneg 9584    / cdiv 9981   NNcn 10310   ZZcz 10634    seqcseq 11790   ^cexp 11849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fv 5414  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-recs 6818  df-rdg 6852  df-neg 9586  df-z 10635  df-seq 11791  df-exp 11850
This theorem is referenced by:  0exp0e1  11854  expp1  11856  expneg  11857  expcllem  11860  mulexp  11887  expadd  11890  expmul  11893  leexp1a  11906  exple1  11907  bernneq  11974  modexp  11983  exp0d  11986  faclbnd4lem1  12053  faclbnd4lem3  12055  faclbnd4lem4  12056  cjexp  12623  absexp  12777  binom  13276  incexclem  13282  incexc  13283  climcndslem1  13295  ege2le3  13358  eft0val  13379  demoivreALT  13468  bits0  13607  0bits  13618  bitsinv1  13621  sadcadd  13637  smumullem  13671  numexp0  14088  psgnunilem4  15983  psgn0fv0  15997  psgnprfval1  16006  cnfldexp  17693  expmhm  17724  expcn  20290  iblcnlem1  21107  itgcnlem  21109  dvexp  21269  dvexp2  21270  plyconst  21559  0dgr  21598  0dgrb  21599  aaliou3lem2  21694  cxp0  22000  1cubr  22122  log2ublem3  22228  basellem2  22304  basellem5  22307  lgsquad2lem2  22583  oddpwdc  26585  subfacval2  26923  fprodconst  27336  fallfac0  27378  bpoly0  28040  m1expeven  29618  stoweidlem19  29660  rusgranumwlk  30421  psgnsn  30602
  Copyright terms: Public domain W3C validator