Theorem exp0 14208

Description: Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14209), 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 12704	. . 3 ⊢ 0 ∈ ℤ
2		expval 14206	. . 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 2760	. . 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 2811	1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ifcif 4481  {csn 4583   class class class wbr 5102   × cxp 5648  ‘cfv 6538  (class class class)co 7420  ℂcc 11198  0cc0 11200  1c1 11201   · cmul 11205   < clt 11343   -cneg 11542   / cdiv 11973  ℕcn 12335  ℤcz 12693  seqcseq 14144  ↑cexp 14204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-1cn 11258  ax-addrcl 11261  ax-rnegex 11271  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-neg 11544  df-z 12694  df-seq 14145  df-exp 14205

This theorem is used by:  0exp0e1  14209  expp1  14211  expneg  14212  expcllem  14215  mulexp  14244  expadd  14247  expmul  14250  exp0d  14283  leexp1a  14318  exple1  14320  bernneq  14373  modexp  14382  faclbnd4lem1  14437  faclbnd4lem3  14439  faclbnd4lem4  14440  cjexp  15317  absexp  15471  binom  15999  incexclem  16005  incexc  16006  climcndslem1  16018  pwdif  16037  fprodconst  16145  fallfac0  16194  bpoly0  16216  ege2le3  16256  eft0val  16280  demoivreALT  16369  pwp1fsum  16561  bits0  16598  0bits  16609  bitsinv1  16612  sadcadd  16628  smumullem  16662  numexp0  17253  psgnunilem4  19711  psgn0fv0  19725  psgnsn  19734  psgnprfval1  19736  cnfldexp  21711  expmhm  21742  expcn  25193  iblcnlem1  26108  itgcnlem  26110  dvexp  26273  dvexp2  26274  plyconst  26524  0dgr  26564  0dgrb  26565  aaliou3lem2  26670  cxp0  26998  1cubr  27170  log2ublem3  27276  basellem2  27409  basellem5  27412  lgsquad2lem2  27712  0dp2dp  33475  fldext2chn  34360  oddpwdc  34986  breprexp  35262  subfacval2  35952  fwddifn0  36929  stoweidlem19  47029  fmtno0  48625  bits0ALTV  48777  0dig2nn0e  49724  0dig2nn0o  49725  nn0sumshdiglemA  49731  nn0sumshdiglemB  49732  nn0sumshdiglem1  49733  nn0sumshdiglem2  49734