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

Theorem exp0 10463
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 9404 . . 3  |-  0  e.  ZZ
2 expval 10461 . . 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 2064 . . 3  |-  0  =  0
5 iftrue 3187 . . 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 2112 1  |-  ( A  e.  CC  ->  ( A ^ 0 )  =  1 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1520    e. wcel 1522   ifcif 3181   {csn 3255   class class class wbr 3586    X. cxp 4254   ` cfv 4268  (class class class)co 5360   CCcc 8156   0cc0 8158   1c1 8159    x. cmul 8163    < clt 8286   -ucneg 8451    / cdiv 8815   NNcn 9124   ZZcz 9393    seq cseq 10401   ^cexp 10459
This theorem is referenced by:  expp1  10465  expneg  10466  expcllem  10469  mulexp  10496  expadd  10499  expmul  10502  leexp1a  10515  exple1  10516  bernneq  10581  modexp  10590  exp0d  10593  faclbnd  10657  faclbnd3  10659  faclbnd4lem1  10660  faclbnd4lem3  10662  faclbnd4lem4  10663  facubnd  10667  hashmap  10740  cjexp  10830  absexp  10981  binom  11476  climcndslem1  11493  ef0lem  11543  ege2le3  11554  eft0val  11575  demoivreALT  11664  prmdvdsexpr  11900  numexp0  12196  pgp0  13616  sylow2alem2  13638  ablfac1eu  14016  pgpfac1lem3a  14019  cnfldexp  15114  expmhm  15156  expcn  17060  iblcnlem1  17822  itgcnlem  17824  dvexp  17956  dvexp2  17957  plyconst  18231  0dgr  18270  0dgrb  18271  coefv0  18272  dgreq0  18289  cxpexp  18605  cxp0  18607  1cubr  18692  log2ublem3  18798  basellem2  18873  basellem5  18876  0sgm  18936  musum  18985  logexprlim  19018  lgsmod  19114  lgsquad2lem2  19152  ostth2lem2  19337  subfacval2  21592  bpoly0  22662  rmxy0  24782  expdioph  24890  aaliou3lem2  24966  psgnunilem4  25237
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 1562  ax-10 1576  ax-9 1582  ax-4 1589  ax-16 1775  ax-ext 2046  ax-sep 3701  ax-nul 3709  ax-pow 3745  ax-pr 3769  ax-un 4061  ax-resscn 8214  ax-1cn 8215  ax-icn 8216  ax-addcl 8217  ax-addrcl 8218  ax-mulcl 8219  ax-mulrcl 8220  ax-mulcom 8221  ax-addass 8222  ax-mulass 8223  ax-distr 8224  ax-i2m1 8225  ax-1ne0 8226  ax-1rid 8227  ax-rnegex 8228  ax-rrecex 8229  ax-cnre 8230  ax-pre-lttri 8231  ax-pre-lttrn 8232  ax-pre-ltadd 8233  ax-pre-mulgt0 8234
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 897  df-3an 898  df-tru 1259  df-ex 1447  df-sb 1736  df-eu 1958  df-mo 1959  df-clab 2052  df-cleq 2057  df-clel 2060  df-ne 2184  df-nel 2185  df-ral 2278  df-rex 2279  df-reu 2280  df-rab 2281  df-v 2477  df-sbc 2651  df-csb 2733  df-dif 2796  df-un 2798  df-in 2800  df-ss 2804  df-pss 2806  df-nul 3073  df-if 3182  df-pw 3243  df-sn 3261  df-pr 3262  df-tp 3263  df-op 3264  df-uni 3425  df-iun 3502  df-br 3587  df-opab 3641  df-mpt 3642  df-tr 3674  df-eprel 3856  df-id 3860  df-po 3865  df-so 3866  df-fr 3903  df-we 3905  df-ord 3946  df-on 3947  df-lim 3948  df-suc 3949  df-om 4224  df-xp 4270  df-rel 4271  df-cnv 4272  df-co 4273  df-dm 4274  df-rn 4275  df-res 4276  df-ima 4277  df-fun 4278  df-fn 4279  df-f 4280  df-f1 4281  df-fo 4282  df-f1o 4283  df-fv 4284  df-ov 5363  df-oprab 5364  df-mpt2 5365  df-iota 5770  df-recs 5843  df-rdg 5878  df-er 6115  df-en 6302  df-dom 6303  df-sdom 6304  df-riota 6468  df-pnf 8287  df-mnf 8288  df-xr 8289  df-ltxr 8290  df-le 8291  df-sub 8452  df-neg 8453  df-n 9125  df-z 9394  df-seq 10402  df-exp 10460
Copyright terms: Public domain