Theorem exp0 14133

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ifcif 4485  {csn 4587   class class class wbr 5107   × cxp 5657  ‘cfv 6537  (class class class)co 7417  ℂcc 11126  0cc0 11128  1c1 11129   · cmul 11133   < clt 11271  -cneg 11470   / cdiv 11899  ℕcn 12261  ℤcz 12619  seqcseq 14069  ↑cexp 14129

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-1cn 11186  ax-addrcl 11189  ax-rnegex 11199  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-neg 11472  df-z 12620  df-seq 14070  df-exp 14130

This theorem is used by:  0exp0e1  14134  expp1  14136  expneg  14137  expcllem  14140  mulexp  14169  expadd  14172  expmul  14175  exp0d  14208  leexp1a  14243  exple1  14245  bernneq  14297  modexp  14306  faclbnd4lem1  14361  faclbnd4lem3  14363  faclbnd4lem4  14364  cjexp  15241  absexp  15395  binom  15923  incexclem  15929  incexc  15930  climcndslem1  15942  pwdif  15961  fprodconst  16071  fallfac0  16120  bpoly0  16142  ege2le3  16182  eft0val  16206  demoivreALT  16295  pwp1fsum  16487  bits0  16524  0bits  16535  bitsinv1  16538  sadcadd  16554  smumullem  16588  numexp0  17173  psgnunilem4  19630  psgn0fv0  19644  psgnsn  19653  psgnprfval1  19655  cnfldexp  21624  expmhm  21655  expcn  25106  iblcnlem1  26022  itgcnlem  26024  dvexp  26187  dvexp2  26188  plyconst  26438  0dgr  26478  0dgrb  26479  aaliou3lem2  26586  cxp0  26915  1cubr  27087  log2ublem3  27193  basellem2  27326  basellem5  27329  lgsquad2lem2  27629  0dp2dp  33362  fldext2chn  34246  oddpwdc  34873  breprexp  35149  subfacval2  35774  fwddifn0  36752  stoweidlem19  46855  fmtno0  48451  bits0ALTV  48603  0dig2nn0e  49550  0dig2nn0o  49551  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  nn0sumshdiglem1  49559  nn0sumshdiglem2  49560