HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem exp0 10478
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 9419 . . 3  |-  0  e.  ZZ
2 expval 10476 . . 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 645 . 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 2065 . . 3  |-  0  =  0
5 iftrue 3188 . . 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 2113 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1520    e. wcel 1522   ifcif 3182   {csn 3256   class class class wbr 3592    X. cxp 4260   ` cfv 4274  (class class class)co 5366   CCcc 8162   0cc0 8164   1c1 8165    x. cmul 8169    < clt 8294   -ucneg 8459    / cdiv 8824   NNcn 9133   ZZcz 9408    seq cseq 10416   ^cexp 10474
This theorem is referenced by:  expp1  10480  expneg  10481  expcllem  10484  mulexp  10511  expadd  10514  expmul  10517  leexp1a  10530  exple1  10531  bernneq  10596  modexp  10605  exp0d  10608  faclbnd  10672  faclbnd3  10674  faclbnd4lem1  10675  faclbnd4lem3  10677  faclbnd4lem4  10678  facubnd  10682  hashmap  10755  cjexp  10845  absexp  10997  binom  11492  climcndslem1  11509  ef0lem  11559  ege2le3  11570  eft0val  11591  demoivreALT  11680  prmdvdsexpr  11916  numexp0  12212  pgp0  13633  sylow2alem2  13655  ablfac1eu  14033  pgpfac1lem3a  14036  cnfldexp  15131  expmhm  15173  expcn  17077  iblcnlem1  17839  itgcnlem  17841  dvexp  17973  dvexp2  17974  plyconst  18248  0dgr  18287  0dgrb  18288  coefv0  18289  cxpexp  18622  cxp0  18624  1cubr  18709  log2ublem3  18815  basellem2  18890  basellem5  18893  0sgm  18953  musum  19002  logexprlim  19035  lgsmod  19131  lgsquad2lem2  19169  ostth2lem2  19354  subfacval2  21611  bpoly0  22679  rmxy0  24799  expdioph  24907  aaliou3lem2  24983  psgnunilem4  25254
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1442  ax-6 1443  ax-7 1444  ax-gen 1445  ax-8 1524  ax-11 1525  ax-13 1526  ax-14 1527  ax-17 1529  ax-12o 1563  ax-10 1577  ax-9 1583  ax-4 1590  ax-16 1776  ax-ext 2047  ax-sep 3707  ax-nul 3715  ax-pr 3775  ax-un 4067  ax-1cn 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-mulrcl 8226  ax-i2m1 8231  ax-1ne0 8232  ax-rnegex 8234  ax-rrecex 8235  ax-cnre 8236
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 897  df-3an 898  df-ex 1447  df-sb 1737  df-eu 1959  df-mo 1960  df-clab 2053  df-cleq 2058  df-clel 2061  df-ne 2185  df-ral 2279  df-rex 2280  df-rab 2282  df-v 2478  df-sbc 2652  df-dif 2797  df-un 2799  df-in 2801  df-ss 2805  df-nul 3074  df-if 3183  df-sn 3262  df-pr 3263  df-op 3265  df-uni 3431  df-br 3593  df-opab 3647  df-mpt 3648  df-id 3866  df-xp 4276  df-rel 4277  df-cnv 4278  df-co 4279  df-dm 4280  df-rn 4281  df-res 4282  df-ima 4283  df-fun 4284  df-fv 4290  df-ov 5369  df-oprab 5370  df-mpt2 5371  df-recs 5849  df-rdg 5884  df-neg 8461  df-z 9409  df-seq 10417  df-exp 10475
Copyright terms: Public domain