Theorem exp0 14033

Description: Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14034), 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 12571	. . 3 ⊢ 0 ∈ ℤ
2		expval 14031	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
3	1, 2	mpan2 689	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
4		eqid 2732	. . 3 ⊢ 0 = 0
5	4	iftruei 4535	. 2 ⊢ if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1
6	3, 5	eqtrdi 2788	1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ifcif 4528  {csn 4628   class class class wbr 5148   × cxp 5674  ‘cfv 6543  (class class class)co 7411  ℂcc 11110  0cc0 11112  1c1 11113   · cmul 11117   < clt 11250  -cneg 11447   / cdiv 11873  ℕcn 12214  ℤcz 12560  seqcseq 13968  ↑cexp 14029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-1cn 11170  ax-addrcl 11173  ax-rnegex 11183  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-neg 11449  df-z 12561  df-seq 13969  df-exp 14030

This theorem is referenced by:  0exp0e1  14034  expp1  14036  expneg  14037  expcllem  14040  mulexp  14069  expadd  14072  expmul  14075  exp0d  14107  leexp1a  14142  exple1  14143  bernneq  14194  modexp  14203  faclbnd4lem1  14255  faclbnd4lem3  14257  faclbnd4lem4  14258  cjexp  15099  absexp  15253  binom  15778  incexclem  15784  incexc  15785  climcndslem1  15797  pwdif  15816  fprodconst  15924  fallfac0  15974  bpoly0  15996  ege2le3  16035  eft0val  16057  demoivreALT  16146  pwp1fsum  16336  bits0  16371  0bits  16382  bitsinv1  16385  sadcadd  16401  smumullem  16435  numexp0  17011  psgnunilem4  19367  psgn0fv0  19381  psgnsn  19390  psgnprfval1  19392  cnfldexp  20984  expmhm  21020  expcn  24395  iblcnlem1  25312  itgcnlem  25314  dvexp  25477  dvexp2  25478  plyconst  25727  0dgr  25766  0dgrb  25767  aaliou3lem2  25863  cxp0  26185  1cubr  26354  log2ublem3  26460  basellem2  26593  basellem5  26596  lgsquad2lem2  26895  0dp2dp  32113  oddpwdc  33422  breprexp  33714  subfacval2  34247  fwddifn0  35211  gg-expcn  35239  stoweidlem19  44820  fmtno0  46293  bits0ALTV  46432  0dig2nn0e  47382  0dig2nn0o  47383  nn0sumshdiglemA  47389  nn0sumshdiglemB  47390  nn0sumshdiglem1  47391  nn0sumshdiglem2  47392