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

Theorem exp0 8640
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 7937 . . 3 |- 0 e. ZZ
2 expval 8638 . . 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 655 . 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 1938 . . 3 |- 0 = 0
5 iftrue 3015 . . 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 1986 1 |- (A e. CC -> (A^0) = 1)
Colors of variables: wff set class
Syntax hints:   -> wi 4   = wceq 1434   e. wcel 1436  ifcif 3009  {csn 3079   class class class wbr 3363   X. cxp 3994  ` cfv 4008  (class class class)co 4927  CCcc 7005  0cc0 7007  1c1 7008   x. cmul 7012   < clt 7119  -ucneg 7231   / cdiv 7232  NNcn 7233  ZZcz 7235   seq cseq 8584  ^cexp 8636
This theorem is referenced by:  expp1 8642  expneg 8643  expcllem 8646  mulexp 8670  expadd 8673  expmul 8676  expmwordi 8688  exple1 8689  bernneq 8749  modexp 8757  faclbnd 8783  faclbnd3 8785  faclbnd4lem1 8786  faclbnd4lem3 8788  faclbnd4lem4 8789  faclbnd6 8792  hashmap 8840  cjexp 8925  absexp 9055  binom 9373  climcndslem1 9390  geoser 9402  cvgrat 9413  ef0lem 9434  ege2le3 9444  efexp 9454  eft0val 9464  demoivreALT 9534  phiprm 9776  oddvds 9787  pclem 9816  pcpre1 9820  pcmpt 9851  prmpwdvds 9860  4001lem1 10001  expcn 11500  iblcnlem1 12379  itgcnlem 12381  dvexp 12489  plyconst 12549  plyeq0lem 12553  plyco 12583  0dgr 12587  0dgrb 12588  coefv0 12589  dgreq0 12606  vieta1 12645  cxpexp 12790  cxp0 12792  cxpmul2 12810  ftalem5 12906  basellem2 12911  basellem5 12914  bposlem5 12933  chebbnd1lem1 12939  qabvexp 12962  ostth2lem2 12970  ostth3 12974  bpoly0 15391
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-13 1442  ax-14 1443  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-rep 3449  ax-sep 3459  ax-nul 3468  ax-pow 3504  ax-pr 3528  ax-un 3800  ax-resscn 7061  ax-1cn 7062  ax-icn 7063  ax-addcl 7064  ax-addrcl 7065  ax-mulcl 7066  ax-mulrcl 7067  ax-mulcom 7068  ax-addass 7069  ax-mulass 7070  ax-distr 7071  ax-i2m1 7072  ax-1ne0 7073  ax-1rid 7074  ax-rnegex 7075  ax-rrecex 7076  ax-cnre 7077  ax-pre-lttri 7078  ax-pre-lttrn 7079  ax-pre-ltadd 7080  ax-pre-mulgt0 7081
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-3or 922  df-3an 923  df-tru 1329  df-ex 1356  df-sb 1611  df-eu 1838  df-mo 1839  df-clab 1926  df-cleq 1931  df-clel 1934  df-ne 2058  df-nel 2059  df-ral 2151  df-rex 2152  df-reu 2153  df-rab 2154  df-v 2345  df-sbc 2510  df-csb 2585  df-dif 2645  df-un 2647  df-in 2649  df-ss 2651  df-pss 2653  df-nul 2907  df-if 3010  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3219  df-iun 3291  df-br 3364  df-opab 3418  df-tr 3433  df-eprel 3613  df-id 3616  df-po 3621  df-so 3635  df-fr 3654  df-we 3670  df-ord 3686  df-on 3687  df-lim 3688  df-suc 3689  df-om 3963  df-xp 4010  df-rel 4011  df-cnv 4012  df-co 4013  df-dm 4014  df-rn 4015  df-res 4016  df-ima 4017  df-fun 4018  df-fn 4019  df-f 4020  df-f1 4021  df-fo 4022  df-f1o 4023  df-fv 4024  df-ov 4929  df-oprab 4930  df-mpt 5065  df-mpt2 5066  df-iota 5278  df-rdg 5364  df-er 5538  df-en 5683  df-dom 5684  df-sdom 5685  df-riota 5826  df-pnf 7120  df-mnf 7121  df-xr 7122  df-ltxr 7123  df-le 7124  df-sub 7249  df-neg 7251  df-n 7714  df-z 7928  df-seq 8585  df-exp 8637
Copyright terms: Public domain