Theorem exp0 13988

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ifcif 4479  {csn 4580   class class class wbr 5098   × cxp 5622  ‘cfv 6492  (class class class)co 7358  ℂcc 11024  0cc0 11026  1c1 11027   · cmul 11031   < clt 11166  -cneg 11365   / cdiv 11794  ℕcn 12145  ℤcz 12488  seqcseq 13924  ↑cexp 13984

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-1cn 11084  ax-addrcl 11087  ax-rnegex 11097  ax-cnre 11099

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-neg 11367  df-z 12489  df-seq 13925  df-exp 13985

This theorem is referenced by:  0exp0e1  13989  expp1  13991  expneg  13992  expcllem  13995  mulexp  14024  expadd  14027  expmul  14030  exp0d  14063  leexp1a  14098  exple1  14100  bernneq  14152  modexp  14161  faclbnd4lem1  14216  faclbnd4lem3  14218  faclbnd4lem4  14219  cjexp  15073  absexp  15227  binom  15753  incexclem  15759  incexc  15760  climcndslem1  15772  pwdif  15791  fprodconst  15901  fallfac0  15951  bpoly0  15973  ege2le3  16013  eft0val  16037  demoivreALT  16126  pwp1fsum  16318  bits0  16355  0bits  16366  bitsinv1  16369  sadcadd  16385  smumullem  16419  numexp0  17003  psgnunilem4  19426  psgn0fv0  19440  psgnsn  19449  psgnprfval1  19451  cnfldexp  21359  expmhm  21391  expcn  24819  expcnOLD  24821  iblcnlem1  25745  itgcnlem  25747  dvexp  25913  dvexp2  25914  plyconst  26167  0dgr  26206  0dgrb  26207  aaliou3lem2  26307  cxp0  26635  1cubr  26808  log2ublem3  26914  basellem2  27048  basellem5  27051  lgsquad2lem2  27352  0dp2dp  32990  fldext2chn  33885  oddpwdc  34511  breprexp  34790  subfacval2  35381  fwddifn0  36358  stoweidlem19  46259  fmtno0  47782  bits0ALTV  47921  0dig2nn0e  48854  0dig2nn0o  48855  nn0sumshdiglemA  48861  nn0sumshdiglemB  48862  nn0sumshdiglem1  48863  nn0sumshdiglem2  48864