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

Theorem exp0 11872
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 10660 . . 3  |-  0  e.  ZZ
2 expval 11870 . . 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 671 . 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 2443 . . 3  |-  0  =  0
54iftruei 3801 . 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 2491 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   ifcif 3794   {csn 3880   class class class wbr 4295    X. cxp 4841   ` cfv 5421  (class class class)co 6094   CCcc 9283   0cc0 9285   1c1 9286    x. cmul 9290    < clt 9421   -ucneg 9599    / cdiv 9996   NNcn 10325   ZZcz 10649    seqcseq 11809   ^cexp 11868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-i2m1 9353  ax-1ne0 9354  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fv 5429  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-recs 6835  df-rdg 6869  df-neg 9601  df-z 10650  df-seq 11810  df-exp 11869
This theorem is referenced by:  0exp0e1  11873  expp1  11875  expneg  11876  expcllem  11879  mulexp  11906  expadd  11909  expmul  11912  leexp1a  11925  exple1  11926  bernneq  11993  modexp  12002  exp0d  12005  faclbnd4lem1  12072  faclbnd4lem3  12074  faclbnd4lem4  12075  cjexp  12642  absexp  12796  binom  13296  incexclem  13302  incexc  13303  climcndslem1  13315  ege2le3  13378  eft0val  13399  demoivreALT  13488  bits0  13627  0bits  13638  bitsinv1  13641  sadcadd  13657  smumullem  13691  numexp0  14108  psgnunilem4  16006  psgn0fv0  16020  psgnprfval1  16029  cnfldexp  17852  expmhm  17883  expcn  20451  iblcnlem1  21268  itgcnlem  21270  dvexp  21430  dvexp2  21431  plyconst  21677  0dgr  21716  0dgrb  21717  aaliou3lem2  21812  cxp0  22118  1cubr  22240  log2ublem3  22346  basellem2  22422  basellem5  22425  lgsquad2lem2  22701  oddpwdc  26740  subfacval2  27078  fprodconst  27492  fallfac0  27534  bpoly0  28196  m1expeven  29775  stoweidlem19  29817  rusgranumwlk  30578  psgnsn  30774
  Copyright terms: Public domain W3C validator