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

Theorem exp0 8572
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. (Revised by Mario Carneiro, 2-Jul-2013.)
Assertion
Ref Expression
exp0 |- (A e. CC -> (A^0) = 1)

Proof of Theorem exp0
StepHypRef Expression
1 0z 7881 . . 3 |- 0 e. ZZ
2 expval 8570 . . 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}))` -u0)))))
31, 2mpan2 678 . 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}))` -u0)))))
4 eqid 1960 . . 3 |- 0 = 0
5 iftrue 3033 . . 3 |- (0 = 0 -> if(0 = 0, 1, if(0 < 0, ( seq 1( x. , (NN X. {A}))` 0), (1 / ( seq 1( x. , (NN X. {A}))` -u0)))) = 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}))` -u0)))) = 1
73, 6syl6eq 2008 1 |- (A e. CC -> (A^0) = 1)
Colors of variables: wff set class
Syntax hints:   -> wi 4   = wceq 1457   e. wcel 1459  ifcif 3027  {csn 3095   class class class wbr 3376   X. cxp 3998  ` cfv 4012  (class class class)co 4924  CCcc 6958  0cc0 6960  1c1 6961   x. cmul 6965   < clt 7072  -ucneg 7183   / cdiv 7184  NNcn 7185  ZZcz 7187   seq cseq 8517  ^cexp 8568
This theorem is referenced by:  expp1 8574  expneg 8575  expcllem 8578  mulexp 8601  expadd 8604  expmul 8607  expmwordi 8619  exple1 8620  bernneq 8680  modexp 8688  faclbnd 8714  faclbnd3 8716  faclbnd4lem1 8717  faclbnd4lem3 8719  faclbnd4lem4 8720  faclbnd6 8723  hashpw 8771  cjexp 8857  absexp 8987  binom 9234  geoser 9258  cvgrat 9269  ef0lem 9317  ege2le3 9327  efexp 9337  eft0val 9347  demoivreALT 9420  phiprm 9657  oddvds 9668  pclem 9697  pcpre1 9701  pcmpt 9726  prmpwdvds 9735  4001lem1 9834  expcn 11265  harmoniclem 13495  iblrelem0 13712  bpoly0 14579
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-13 1465  ax-14 1466  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-rep 3462  ax-sep 3472  ax-nul 3481  ax-pow 3517  ax-pr 3541  ax-un 3811  ax-resscn 7014  ax-1cn 7015  ax-icn 7016  ax-addcl 7017  ax-addrcl 7018  ax-mulcl 7019  ax-mulrcl 7020  ax-mulcom 7021  ax-addass 7022  ax-mulass 7023  ax-distr 7024  ax-i2m1 7025  ax-1ne0 7026  ax-1rid 7027  ax-rnegex 7028  ax-rrecex 7029  ax-cnre 7030  ax-pre-lttri 7031  ax-pre-lttrn 7032  ax-pre-ltadd 7033  ax-pre-mulgt0 7034
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3or 947  df-3an 948  df-tru 1354  df-ex 1381  df-sb 1633  df-eu 1860  df-mo 1861  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-nel 2081  df-ral 2173  df-rex 2174  df-reu 2175  df-rab 2176  df-v 2367  df-sbc 2532  df-csb 2606  df-dif 2665  df-un 2667  df-in 2669  df-ss 2671  df-pss 2673  df-nul 2927  df-if 3028  df-pw 3084  df-sn 3099  df-pr 3100  df-tp 3102  df-op 3103  df-uni 3232  df-iun 3304  df-br 3377  df-opab 3431  df-tr 3446  df-eprel 3624  df-id 3627  df-po 3632  df-so 3646  df-fr 3665  df-we 3681  df-ord 3697  df-on 3698  df-lim 3699  df-suc 3700  df-om 3967  df-xp 4014  df-rel 4015  df-cnv 4016  df-co 4017  df-dm 4018  df-rn 4019  df-res 4020  df-ima 4021  df-fun 4022  df-fn 4023  df-f 4024  df-f1 4025  df-fo 4026  df-f1o 4027  df-fv 4028  df-ov 4926  df-oprab 4927  df-mpt 5061  df-mpt2 5062  df-iota 5234  df-rdg 5320  df-er 5494  df-en 5639  df-dom 5640  df-sdom 5641  df-riota 5782  df-pnf 7073  df-mnf 7074  df-xr 7075  df-ltxr 7076  df-le 7077  df-sub 7201  df-neg 7203  df-n 7660  df-z 7872  df-seq 8518  df-exp 8569
Copyright terms: Public domain