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

Theorem exp0 10079
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 9118 . . 3  |-  0  e.  ZZ
2 expval 10077 . . 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 648 . 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 2082 . . 3  |-  0  = 
0
5 iftrue 3204 . . 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 2130 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1536    e. wcel 1538   ifcif 3198   {csn 3272   class class class wbr 3600    X. cxp 4273   ` cfv 4287  (class class class)co 5354   CCcc 8135   0cc0 8137   1c1 8138    x. cmul 8142    < clt 8254   -ucneg 8374    / cdiv 8375   NNcn 8376   ZZcz 8378    seq cseq 10020   ^cexp 10075
This theorem is referenced by:  expp1  10081  expneg  10082  expcllem  10085  mulexp  10112  expadd  10115  expmul  10118  expmwordi  10130  exple1  10131  bernneq  10194  modexp  10203  faclbnd  10227  faclbnd3  10229  faclbnd4lem1  10230  faclbnd4lem3  10232  faclbnd4lem4  10233  faclbnd6  10236  hashmap  10296  cjexp  10392  absexp  10524  binom  10868  climcndslem1  10885  geoser  10900  cvgrat  10912  ef0lem  10933  ege2le3  10943  efexp  10953  eft0val  10963  demoivreALT  11046  prmdvdsexpr  11281  phiprm  11301  odzdvds  11316  pclem  11347  pcpre1  11351  pcexp  11367  prmpwdvds  11406  numexp0  11546  decsplit0b  11550  pgp0  12739  sylow2alem2  12758  cnfldexp  14082  expmhm  14123  expcn  16097  iblcnlem1  16858  itgcnlem  16860  dvexp  16992  dvexp2  16993  plyconst  17246  plyeq0lem  17250  plyco  17281  0dgr  17285  0dgrb  17286  coefv0  17287  dgreq0  17304  vieta1  17343  abelthlem9  17419  cxpexp  17602  cxp0  17604  cxpmul2  17623  1cubr  17647  log2ublem3  17753  ftalem5  17807  basellem2  17812  basellem5  17815  0sgm  17856  musum  17893  bposlem5  17917  lgsval2lem  17935  lgsmod  17950  lgsdilem2  17960  lgsne0  17962  lgsquad2lem2  17982  chebbnd1lem1  18001  qabvexp  18021  ostth2lem2  18029  ostth3  18033  subfacval2  20280  bpoly0  21384  mzpexpmpt  23274  pell14qrexpclnn0  23430  pellfund14  23464  rmxy0  23489  jm2.17a  23528  jm2.17b  23529  rpexp1i  23561  jm2.18  23564  jm2.23  23572  expdioph  23599  aaliou3lem2  23677  cnsrexpcl  23898  psgnunilem4  23948
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-13 1542  ax-14 1543  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-sep 3715  ax-nul 3723  ax-pow 3759  ax-pr 3783  ax-un 4075  ax-resscn 8193  ax-1cn 8194  ax-icn 8195  ax-addcl 8196  ax-addrcl 8197  ax-mulcl 8198  ax-mulrcl 8199  ax-mulcom 8200  ax-addass 8201  ax-mulass 8202  ax-distr 8203  ax-i2m1 8204  ax-1ne0 8205  ax-1rid 8206  ax-rnegex 8207  ax-rrecex 8208  ax-cnre 8209  ax-pre-lttri 8210  ax-pre-lttrn 8211  ax-pre-ltadd 8212  ax-pre-mulgt0 8213
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 904  df-3an 905  df-tru 1268  df-ex 1456  df-sb 1754  df-eu 1976  df-mo 1977  df-clab 2070  df-cleq 2075  df-clel 2078  df-ne 2201  df-nel 2202  df-ral 2295  df-rex 2296  df-reu 2297  df-rab 2298  df-v 2494  df-sbc 2668  df-csb 2750  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3089  df-if 3199  df-pw 3260  df-sn 3278  df-pr 3279  df-tp 3280  df-op 3281  df-uni 3439  df-iun 3516  df-br 3601  df-opab 3655  df-mpt 3656  df-tr 3688  df-eprel 3870  df-id 3874  df-po 3879  df-so 3880  df-fr 3917  df-we 3919  df-ord 3960  df-on 3961  df-lim 3962  df-suc 3963  df-om 4243  df-xp 4289  df-rel 4290  df-cnv 4291  df-co 4292  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fun 4297  df-fn 4298  df-f 4299  df-f1 4300  df-fo 4301  df-f1o 4302  df-fv 4303  df-ov 5357  df-oprab 5358  df-mpt2 5359  df-iota 5762  df-recs 5835  df-rdg 5870  df-er 6102  df-en 6289  df-dom 6290  df-sdom 6291  df-riota 6455  df-pnf 8255  df-mnf 8256  df-xr 8257  df-ltxr 8258  df-le 8259  df-sub 8392  df-neg 8393  df-n 8863  df-z 9108  df-seq 10021  df-exp 10076
Copyright terms: Public domain