Theorem exp0 14106

Description: Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14107), 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 12624	. . 3 ⊢ 0 ∈ ℤ
2		expval 14104	. . 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 2737	. . 3 ⊢ 0 = 0
5	4	iftruei 4532	. 2 ⊢ if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1
6	3, 5	eqtrdi 2793	1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ifcif 4525  {csn 4626   class class class wbr 5143   × cxp 5683  ‘cfv 6561  (class class class)co 7431  ℂcc 11153  0cc0 11155  1c1 11156   · cmul 11160   < clt 11295  -cneg 11493   / cdiv 11920  ℕcn 12266  ℤcz 12613  seqcseq 14042  ↑cexp 14102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-1cn 11213  ax-addrcl 11216  ax-rnegex 11226  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-neg 11495  df-z 12614  df-seq 14043  df-exp 14103

This theorem is referenced by:  0exp0e1  14107  expp1  14109  expneg  14110  expcllem  14113  mulexp  14142  expadd  14145  expmul  14148  exp0d  14180  leexp1a  14215  exple1  14216  bernneq  14268  modexp  14277  faclbnd4lem1  14332  faclbnd4lem3  14334  faclbnd4lem4  14335  cjexp  15189  absexp  15343  binom  15866  incexclem  15872  incexc  15873  climcndslem1  15885  pwdif  15904  fprodconst  16014  fallfac0  16064  bpoly0  16086  ege2le3  16126  eft0val  16148  demoivreALT  16237  pwp1fsum  16428  bits0  16465  0bits  16476  bitsinv1  16479  sadcadd  16495  smumullem  16529  numexp0  17113  psgnunilem4  19515  psgn0fv0  19529  psgnsn  19538  psgnprfval1  19540  cnfldexp  21417  expmhm  21454  expcn  24896  expcnOLD  24898  iblcnlem1  25823  itgcnlem  25825  dvexp  25991  dvexp2  25992  plyconst  26245  0dgr  26284  0dgrb  26285  aaliou3lem2  26385  cxp0  26712  1cubr  26885  log2ublem3  26991  basellem2  27125  basellem5  27128  lgsquad2lem2  27429  0dp2dp  32891  fldext2chn  33769  oddpwdc  34356  breprexp  34648  subfacval2  35192  fwddifn0  36165  stoweidlem19  46034  fmtno0  47527  bits0ALTV  47666  0dig2nn0e  48533  0dig2nn0o  48534  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  nn0sumshdiglem2  48543