Theorem exp0 14000

Description: Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14001), 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 12511	. . 3 ⊢ 0 ∈ ℤ
2		expval 13998	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
3	1, 2	mpan2 692	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
4		eqid 2737	. . 3 ⊢ 0 = 0
5	4	iftruei 4488	. 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 1542   ∈ wcel 2114  ifcif 4481  {csn 4582   class class class wbr 5100   × cxp 5630  ‘cfv 6500  (class class class)co 7368  ℂcc 11036  0cc0 11038  1c1 11039   · cmul 11043   < clt 11178  -cneg 11377   / cdiv 11806  ℕcn 12157  ℤcz 12500  seqcseq 13936  ↑cexp 13996

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-neg 11379  df-z 12501  df-seq 13937  df-exp 13997

This theorem is referenced by:  0exp0e1  14001  expp1  14003  expneg  14004  expcllem  14007  mulexp  14036  expadd  14039  expmul  14042  exp0d  14075  leexp1a  14110  exple1  14112  bernneq  14164  modexp  14173  faclbnd4lem1  14228  faclbnd4lem3  14230  faclbnd4lem4  14231  cjexp  15085  absexp  15239  binom  15765  incexclem  15771  incexc  15772  climcndslem1  15784  pwdif  15803  fprodconst  15913  fallfac0  15963  bpoly0  15985  ege2le3  16025  eft0val  16049  demoivreALT  16138  pwp1fsum  16330  bits0  16367  0bits  16378  bitsinv1  16381  sadcadd  16397  smumullem  16431  numexp0  17015  psgnunilem4  19438  psgn0fv0  19452  psgnsn  19461  psgnprfval1  19463  cnfldexp  21371  expmhm  21403  expcn  24831  expcnOLD  24833  iblcnlem1  25757  itgcnlem  25759  dvexp  25925  dvexp2  25926  plyconst  26179  0dgr  26218  0dgrb  26219  aaliou3lem2  26319  cxp0  26647  1cubr  26820  log2ublem3  26926  basellem2  27060  basellem5  27063  lgsquad2lem2  27364  0dp2dp  33000  fldext2chn  33905  oddpwdc  34531  breprexp  34810  subfacval2  35400  fwddifn0  36377  stoweidlem19  46371  fmtno0  47894  bits0ALTV  48033  0dig2nn0e  48966  0dig2nn0o  48967  nn0sumshdiglemA  48973  nn0sumshdiglemB  48974  nn0sumshdiglem1  48975  nn0sumshdiglem2  48976