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

Theorem exp0 10103
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 9134 . . 3  |-  0  e.  ZZ
2 expval 10101 . . 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 643 . 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 2061 . . 3  |-  0  =  0
5 iftrue 3184 . . 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 2109 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1517    e. wcel 1519   ifcif 3178   {csn 3252   class class class wbr 3583    X. cxp 4251   ` cfv 4265  (class class class)co 5355   CCcc 8149   0cc0 8151   1c1 8152    x. cmul 8156    < clt 8268   -ucneg 8388    / cdiv 8389   NNcn 8390   ZZcz 8392    seq cseq 10041   ^cexp 10099
This theorem is referenced by:  expp1  10105  expneg  10106  expcllem  10109  mulexp  10136  expadd  10139  expmul  10142  expmwordi  10155  exple1  10156  bernneq  10220  modexp  10229  faclbnd  10253  faclbnd3  10255  faclbnd4lem1  10256  faclbnd4lem3  10258  faclbnd4lem4  10259  faclbnd6  10262  facubnd  10263  hashmap  10336  cjexp  10432  absexp  10564  binom  10915  climcndslem1  10932  geoser  10947  cvgrat  10959  ef0lem  10980  ege2le3  10990  efexp  11000  eft0val  11010  demoivreALT  11093  prmdvdsexpr  11328  rpexp1i  11333  phiprm  11350  odzdvds  11365  pclem  11396  pcpre1  11400  pcexp  11416  prmpwdvds  11455  numexp0  11595  pgp0  13015  sylow2alem2  13037  ablfac1eu  13413  pgpfac1lem3  13416  cnfldexp  14508  expmhm  14550  expcn  16453  iblcnlem1  17214  itgcnlem  17216  dvexp  17348  dvexp2  17349  plyconst  17602  plyeq0lem  17606  plyco  17637  0dgr  17641  0dgrb  17642  coefv0  17643  dgreq0  17660  vieta1  17699  abelthlem9  17775  cxpexp  17960  cxp0  17962  cxpmul2  17981  1cubr  18005  log2ublem3  18111  ftalem5  18165  basellem2  18170  basellem5  18173  0sgm  18214  musum  18251  bposlem5  18275  lgsval2lem  18293  lgsmod  18308  lgsdilem2  18318  lgsne0  18320  lgsquad2lem2  18340  chebbnd1lem1  18359  qabvexp  18379  ostth2lem2  18387  ostth3  18391  subfacval2  20642  bpoly0  21733  mzpexpmpt  23637  pell14qrexpclnn0  23793  pellfund14  23825  rmxy0  23850  jm2.17a  23889  jm2.17b  23890  jm2.18  23923  jm2.23  23931  expdioph  23958  aaliou3lem2  24034  cnsrexpcl  24255  psgnunilem4  24305
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-7 1441  ax-gen 1442  ax-8 1521  ax-11 1522  ax-13 1523  ax-14 1524  ax-17 1526  ax-12o 1559  ax-10 1573  ax-9 1579  ax-4 1586  ax-16 1772  ax-ext 2043  ax-sep 3698  ax-nul 3706  ax-pow 3742  ax-pr 3766  ax-un 4058  ax-resscn 8207  ax-1cn 8208  ax-icn 8209  ax-addcl 8210  ax-addrcl 8211  ax-mulcl 8212  ax-mulrcl 8213  ax-mulcom 8214  ax-addass 8215  ax-mulass 8216  ax-distr 8217  ax-i2m1 8218  ax-1ne0 8219  ax-1rid 8220  ax-rnegex 8221  ax-rrecex 8222  ax-cnre 8223  ax-pre-lttri 8224  ax-pre-lttrn 8225  ax-pre-ltadd 8226  ax-pre-mulgt0 8227
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 894  df-3an 895  df-tru 1256  df-ex 1444  df-sb 1733  df-eu 1955  df-mo 1956  df-clab 2049  df-cleq 2054  df-clel 2057  df-ne 2181  df-nel 2182  df-ral 2275  df-rex 2276  df-reu 2277  df-rab 2278  df-v 2474  df-sbc 2648  df-csb 2730  df-dif 2793  df-un 2795  df-in 2797  df-ss 2801  df-pss 2803  df-nul 3070  df-if 3179  df-pw 3240  df-sn 3258  df-pr 3259  df-tp 3260  df-op 3261  df-uni 3422  df-iun 3499  df-br 3584  df-opab 3638  df-mpt 3639  df-tr 3671  df-eprel 3853  df-id 3857  df-po 3862  df-so 3863  df-fr 3900  df-we 3902  df-ord 3943  df-on 3944  df-lim 3945  df-suc 3946  df-om 4221  df-xp 4267  df-rel 4268  df-cnv 4269  df-co 4270  df-dm 4271  df-rn 4272  df-res 4273  df-ima 4274  df-fun 4275  df-fn 4276  df-f 4277  df-f1 4278  df-fo 4279  df-f1o 4280  df-fv 4281  df-ov 5358  df-oprab 5359  df-mpt2 5360  df-iota 5764  df-recs 5837  df-rdg 5872  df-er 6109  df-en 6296  df-dom 6297  df-sdom 6298  df-riota 6462  df-pnf 8269  df-mnf 8270  df-xr 8271  df-ltxr 8272  df-le 8273  df-sub 8406  df-neg 8407  df-n 8879  df-z 9124  df-seq 10042  df-exp 10100
Copyright terms: Public domain