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

Theorem exp0 13423
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 11981 . . 3 0 ∈ ℤ
2 expval 13421 . . 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 2826 . . 3 0 = 0
54iftruei 4477 . 2 if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1
63, 5syl6eq 2877 1 (𝐴 ∈ ℂ → (𝐴↑0) = 1)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  ifcif 4470  {csn 4564   class class class wbr 5063   × cxp 5552  cfv 6352  (class class class)co 7148  cc 10524  0cc0 10526  1c1 10527   · cmul 10531   < clt 10664  -cneg 10860   / cdiv 11286  cn 11627  cz 11970  seqcseq 13359  cexp 13419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326  ax-1cn 10584  ax-addrcl 10587  ax-rnegex 10597  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-iota 6312  df-fun 6354  df-fv 6360  df-ov 7151  df-oprab 7152  df-mpo 7153  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-neg 10862  df-z 11971  df-seq 13360  df-exp 13420
This theorem is referenced by:  0exp0e1  13424  expp1  13426  expneg  13427  expcllem  13430  mulexp  13458  expadd  13461  expmul  13464  exp0d  13494  leexp1a  13529  exple1  13530  bernneq  13580  modexp  13589  faclbnd4lem1  13643  faclbnd4lem3  13645  faclbnd4lem4  13646  cjexp  14499  absexp  14654  binom  15175  incexclem  15181  incexc  15182  climcndslem1  15194  pwdif  15213  fprodconst  15322  fallfac0  15372  bpoly0  15394  ege2le3  15433  eft0val  15455  demoivreALT  15544  pwp1fsum  15732  bits0  15767  0bits  15778  bitsinv1  15781  sadcadd  15797  smumullem  15831  numexp0  16402  psgnunilem4  18545  psgn0fv0  18559  psgnsn  18568  psgnprfval1  18570  cnfldexp  20494  expmhm  20530  expcn  23395  iblcnlem1  24303  itgcnlem  24305  dvexp  24465  dvexp2  24466  plyconst  24711  0dgr  24750  0dgrb  24751  aaliou3lem2  24847  cxp0  25166  1cubr  25333  log2ublem3  25440  basellem2  25573  basellem5  25576  lgsquad2lem2  25875  0dp2dp  30499  oddpwdc  31498  breprexp  31790  subfacval2  32318  fwddifn0  33509  stoweidlem19  42170  fmtno0  43534  bits0ALTV  43676  0dig2nn0e  44504  0dig2nn0o  44505  nn0sumshdiglemA  44511  nn0sumshdiglemB  44512  nn0sumshdiglem1  44513  nn0sumshdiglem2  44514
  Copyright terms: Public domain W3C validator