Theorem exp0 14030

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ifcif 4488  {csn 4589   class class class wbr 5107   × cxp 5636  ‘cfv 6511  (class class class)co 7387  ℂcc 11066  0cc0 11068  1c1 11069   · cmul 11073   < clt 11208  -cneg 11406   / cdiv 11835  ℕcn 12186  ℤcz 12529  seqcseq 13966  ↑cexp 14026

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-1cn 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-neg 11408  df-z 12530  df-seq 13967  df-exp 14027

This theorem is referenced by:  0exp0e1  14031  expp1  14033  expneg  14034  expcllem  14037  mulexp  14066  expadd  14069  expmul  14072  exp0d  14105  leexp1a  14140  exple1  14142  bernneq  14194  modexp  14203  faclbnd4lem1  14258  faclbnd4lem3  14260  faclbnd4lem4  14261  cjexp  15116  absexp  15270  binom  15796  incexclem  15802  incexc  15803  climcndslem1  15815  pwdif  15834  fprodconst  15944  fallfac0  15994  bpoly0  16016  ege2le3  16056  eft0val  16080  demoivreALT  16169  pwp1fsum  16361  bits0  16398  0bits  16409  bitsinv1  16412  sadcadd  16428  smumullem  16462  numexp0  17046  psgnunilem4  19427  psgn0fv0  19441  psgnsn  19450  psgnprfval1  19452  cnfldexp  21316  expmhm  21353  expcn  24763  expcnOLD  24765  iblcnlem1  25689  itgcnlem  25691  dvexp  25857  dvexp2  25858  plyconst  26111  0dgr  26150  0dgrb  26151  aaliou3lem2  26251  cxp0  26579  1cubr  26752  log2ublem3  26858  basellem2  26992  basellem5  26995  lgsquad2lem2  27296  0dp2dp  32829  fldext2chn  33718  oddpwdc  34345  breprexp  34624  subfacval2  35174  fwddifn0  36152  stoweidlem19  46017  fmtno0  47541  bits0ALTV  47680  0dig2nn0e  48601  0dig2nn0o  48602  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  nn0sumshdiglem2  48611