Theorem exp0 13969

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ifcif 4475  {csn 4576   class class class wbr 5091   × cxp 5614  ‘cfv 6481  (class class class)co 7346  ℂcc 11001  0cc0 11003  1c1 11004   · cmul 11008   < clt 11143  -cneg 11342   / cdiv 11771  ℕcn 12122  ℤcz 12465  seqcseq 13905  ↑cexp 13965

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-1cn 11061  ax-addrcl 11064  ax-rnegex 11074  ax-cnre 11076

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-neg 11344  df-z 12466  df-seq 13906  df-exp 13966

This theorem is referenced by:  0exp0e1  13970  expp1  13972  expneg  13973  expcllem  13976  mulexp  14005  expadd  14008  expmul  14011  exp0d  14044  leexp1a  14079  exple1  14081  bernneq  14133  modexp  14142  faclbnd4lem1  14197  faclbnd4lem3  14199  faclbnd4lem4  14200  cjexp  15054  absexp  15208  binom  15734  incexclem  15740  incexc  15741  climcndslem1  15753  pwdif  15772  fprodconst  15882  fallfac0  15932  bpoly0  15954  ege2le3  15994  eft0val  16018  demoivreALT  16107  pwp1fsum  16299  bits0  16336  0bits  16347  bitsinv1  16350  sadcadd  16366  smumullem  16400  numexp0  16984  psgnunilem4  19407  psgn0fv0  19421  psgnsn  19430  psgnprfval1  19432  cnfldexp  21339  expmhm  21371  expcn  24788  expcnOLD  24790  iblcnlem1  25714  itgcnlem  25716  dvexp  25882  dvexp2  25883  plyconst  26136  0dgr  26175  0dgrb  26176  aaliou3lem2  26276  cxp0  26604  1cubr  26777  log2ublem3  26883  basellem2  27017  basellem5  27020  lgsquad2lem2  27321  0dp2dp  32884  fldext2chn  33736  oddpwdc  34362  breprexp  34641  subfacval2  35219  fwddifn0  36197  stoweidlem19  46056  fmtno0  47570  bits0ALTV  47709  0dig2nn0e  48643  0dig2nn0o  48644  nn0sumshdiglemA  48650  nn0sumshdiglemB  48651  nn0sumshdiglem1  48652  nn0sumshdiglem2  48653