Theorem exp0 13974

Description: Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 13975), following standard convention, for instance 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

Step	Hyp	Ref	Expression
1		0z 12486	. . 3 ⊢ 0 ∈ ℤ
2		expval 13972	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
3	1, 2	mpan2 691	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
4		eqid 2733	. . 3 ⊢ 0 = 0
5	4	iftruei 4481	. 2 ⊢ if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1
6	3, 5	eqtrdi 2784	1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ifcif 4474  {csn 4575   class class class wbr 5093   × cxp 5617  ‘cfv 6486  (class class class)co 7352  ℂcc 11011  0cc0 11013  1c1 11014   · cmul 11018   < clt 11153  -cneg 11352   / cdiv 11781  ℕcn 12132  ℤcz 12475  seqcseq 13910  ↑cexp 13970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-1cn 11071  ax-addrcl 11074  ax-rnegex 11084  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-neg 11354  df-z 12476  df-seq 13911  df-exp 13971

This theorem is referenced by:  0exp0e1  13975  expp1  13977  expneg  13978  expcllem  13981  mulexp  14010  expadd  14013  expmul  14016  exp0d  14049  leexp1a  14084  exple1  14086  bernneq  14138  modexp  14147  faclbnd4lem1  14202  faclbnd4lem3  14204  faclbnd4lem4  14205  cjexp  15059  absexp  15213  binom  15739  incexclem  15745  incexc  15746  climcndslem1  15758  pwdif  15777  fprodconst  15887  fallfac0  15937  bpoly0  15959  ege2le3  15999  eft0val  16023  demoivreALT  16112  pwp1fsum  16304  bits0  16341  0bits  16352  bitsinv1  16355  sadcadd  16371  smumullem  16405  numexp0  16989  psgnunilem4  19411  psgn0fv0  19425  psgnsn  19434  psgnprfval1  19436  cnfldexp  21343  expmhm  21375  expcn  24791  expcnOLD  24793  iblcnlem1  25717  itgcnlem  25719  dvexp  25885  dvexp2  25886  plyconst  26139  0dgr  26178  0dgrb  26179  aaliou3lem2  26279  cxp0  26607  1cubr  26780  log2ublem3  26886  basellem2  27020  basellem5  27023  lgsquad2lem2  27324  0dp2dp  32896  fldext2chn  33762  oddpwdc  34388  breprexp  34667  subfacval2  35252  fwddifn0  36229  stoweidlem19  46141  fmtno0  47664  bits0ALTV  47803  0dig2nn0e  48737  0dig2nn0o  48738  nn0sumshdiglemA  48744  nn0sumshdiglemB  48745  nn0sumshdiglem1  48746  nn0sumshdiglem2  48747