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

Theorem exp0 8625
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 7922 . . 3 |- 0 e. ZZ
2 expval 8623 . . 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 3014 . . 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 3008  {csn 3078   class class class wbr 3362   X. cxp 3993  ` cfv 4007  (class class class)co 4922  CCcc 6990  0cc0 6992  1c1 6993   x. cmul 6997   < clt 7104  -ucneg 7216   / cdiv 7217  NNcn 7218  ZZcz 7220   seq cseq 8569  ^cexp 8621
This theorem is referenced by:  expp1 8627  expneg 8628  expcllem 8631  mulexp 8655  expadd 8658  expmul 8661  expmwordi 8673  exple1 8674  bernneq 8734  modexp 8742  faclbnd 8768  faclbnd3 8770  faclbnd4lem1 8771  faclbnd4lem3 8773  faclbnd4lem4 8774  faclbnd6 8777  hashmap 8825  cjexp 8910  absexp 9040  binom 9358  climcndslem1 9375  geoser 9387  cvgrat 9398  ef0lem 9419  ege2le3 9429  efexp 9439  eft0val 9449  demoivreALT 9519  phiprm 9759  oddvds 9770  pclem 9799  pcpre1 9803  pcmpt 9834  prmpwdvds 9843  4001lem1 9984  expcn 11478  iblcnlem1 12357  itgcnlem 12359  dvexp 12467  plyconst 12527  plyeq0lem 12531  plyco 12561  0dgr 12565  0dgrb 12566  coefv0 12567  dgreq0 12584  vieta1 12623  cxpexp 12768  cxp0 12770  cxpmul2 12788  ftalem5 12884  basellem2 12889  basellem5 12892  bposlem5 12911  chebbnd1lem1 12917  qabvexp 12940  ostth2lem2 12948  ostth3 12952  bpoly0 15369
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 3448  ax-sep 3458  ax-nul 3467  ax-pow 3503  ax-pr 3527  ax-un 3799  ax-resscn 7046  ax-1cn 7047  ax-icn 7048  ax-addcl 7049  ax-addrcl 7050  ax-mulcl 7051  ax-mulrcl 7052  ax-mulcom 7053  ax-addass 7054  ax-mulass 7055  ax-distr 7056  ax-i2m1 7057  ax-1ne0 7058  ax-1rid 7059  ax-rnegex 7060  ax-rrecex 7061  ax-cnre 7062  ax-pre-lttri 7063  ax-pre-lttrn 7064  ax-pre-ltadd 7065  ax-pre-mulgt0 7066
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 3009  df-pw 3067  df-sn 3084  df-pr 3085  df-tp 3086  df-op 3087  df-uni 3218  df-iun 3290  df-br 3363  df-opab 3417  df-tr 3432  df-eprel 3612  df-id 3615  df-po 3620  df-so 3634  df-fr 3653  df-we 3669  df-ord 3685  df-on 3686  df-lim 3687  df-suc 3688  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-ov 4924  df-oprab 4925  df-mpt 5059  df-mpt2 5060  df-iota 5263  df-rdg 5349  df-er 5523  df-en 5668  df-dom 5669  df-sdom 5670  df-riota 5811  df-pnf 7105  df-mnf 7106  df-xr 7107  df-ltxr 7108  df-le 7109  df-sub 7234  df-neg 7236  df-n 7699  df-z 7913  df-seq 8570  df-exp 8622
Copyright terms: Public domain