Theorem exp0 14211

Description: Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14212), 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 12707	. . 3 ⊢ 0 ∈ ℤ
2		expval 14209	. . 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 4584   class class class wbr 5102   × cxp 5648  ‘cfv 6538  (class class class)co 7420  ℂcc 11201  0cc0 11203  1c1 11204   · cmul 11208   < clt 11346   -cneg 11545   / cdiv 11976  ℕcn 12338  ℤcz 12696  seqcseq 14147  ↑cexp 14207

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 11261  ax-addrcl 11264  ax-rnegex 11274  ax-cnre 11276

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 4585  df-pr 4587  df-op 4835  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 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-neg 11547  df-z 12697  df-seq 14148  df-exp 14208

This theorem is used by:  0exp0e1  14212  expp1  14214  expneg  14215  expcllem  14218  mulexp  14247  expadd  14250  expmul  14253  exp0d  14286  leexp1a  14321  exple1  14323  bernneq  14376  modexp  14385  faclbnd4lem1  14440  faclbnd4lem3  14442  faclbnd4lem4  14443  cjexp  15322  absexp  15476  binom  16004  incexclem  16010  incexc  16011  climcndslem1  16023  pwdif  16042  fprodconst  16150  fallfac0  16199  bpoly0  16221  ege2le3  16261  eft0val  16285  demoivreALT  16374  pwp1fsum  16566  bits0  16603  0bits  16614  bitsinv1  16617  sadcadd  16633  smumullem  16667  numexp0  17258  psgnunilem4  19716  psgn0fv0  19730  psgnsn  19739  psgnprfval1  19741  cnfldexp  21716  expmhm  21747  expcn  25198  iblcnlem1  26113  itgcnlem  26115  dvexp  26278  dvexp2  26279  plyconst  26529  0dgr  26569  0dgrb  26570  aaliou3lem2  26675  cxp0  27003  1cubr  27175  log2ublem3  27281  basellem2  27414  basellem5  27417  lgsquad2lem2  27717  0dp2dp  33521  fldext2chn  34406  oddpwdc  35032  breprexp  35308  subfacval2  36038  fwddifn0  37021  stoweidlem19  47122  fmtno0  48718  bits0ALTV  48870  0dig2nn0e  49817  0dig2nn0o  49818  nn0sumshdiglemA  49824  nn0sumshdiglemB  49825  nn0sumshdiglem1  49826  nn0sumshdiglem2  49827