MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp0 Structured version   Visualization version   GIF version

Theorem exp0 13421
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 (𝐴 ∈ ℂ → (𝐴↑0) = 1)

Proof of Theorem exp0
StepHypRef Expression
1 0z 11980 . . 3 0 ∈ ℤ
2 expval 13419 . . 3 ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
31, 2mpan2 687 . 2 (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
4 eqid 2818 . . 3 0 = 0
54iftruei 4470 . 2 if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1
63, 5syl6eq 2869 1 (𝐴 ∈ ℂ → (𝐴↑0) = 1)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  ifcif 4463  {csn 4557   class class class wbr 5057   × cxp 5546  cfv 6348  (class class class)co 7145  cc 10523  0cc0 10525  1c1 10526   · cmul 10530   < clt 10663  -cneg 10859   / cdiv 11285  cn 11626  cz 11969  seqcseq 13357  cexp 13417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-1cn 10583  ax-addrcl 10586  ax-rnegex 10596  ax-cnre 10598
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-iota 6307  df-fun 6350  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-neg 10861  df-z 11970  df-seq 13358  df-exp 13418
This theorem is referenced by:  0exp0e1  13422  expp1  13424  expneg  13425  expcllem  13428  mulexp  13456  expadd  13459  expmul  13462  exp0d  13492  leexp1a  13527  exple1  13528  bernneq  13578  modexp  13587  faclbnd4lem1  13641  faclbnd4lem3  13643  faclbnd4lem4  13644  cjexp  14497  absexp  14652  binom  15173  incexclem  15179  incexc  15180  climcndslem1  15192  pwdif  15211  fprodconst  15320  fallfac0  15370  bpoly0  15392  ege2le3  15431  eft0val  15453  demoivreALT  15542  pwp1fsum  15730  bits0  15765  0bits  15776  bitsinv1  15779  sadcadd  15795  smumullem  15829  numexp0  16400  psgnunilem4  18554  psgn0fv0  18568  psgnsn  18577  psgnprfval1  18579  cnfldexp  20506  expmhm  20542  expcn  23407  iblcnlem1  24315  itgcnlem  24317  dvexp  24477  dvexp2  24478  plyconst  24723  0dgr  24762  0dgrb  24763  aaliou3lem2  24859  cxp0  25180  1cubr  25347  log2ublem3  25453  basellem2  25586  basellem5  25589  lgsquad2lem2  25888  0dp2dp  30512  oddpwdc  31511  breprexp  31803  subfacval2  32331  fwddifn0  33522  stoweidlem19  42181  fmtno0  43579  bits0ALTV  43721  0dig2nn0e  44600  0dig2nn0o  44601  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608  nn0sumshdiglem1  44609  nn0sumshdiglem2  44610
  Copyright terms: Public domain W3C validator