Theorem exp0 14018

Description: Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14019), 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 12526	. . 3 ⊢ 0 ∈ ℤ
2		expval 14016	. . 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 4474	. 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 4467  {csn 4568   class class class wbr 5086   × cxp 5622  ‘cfv 6492  (class class class)co 7360  ℂcc 11027  0cc0 11029  1c1 11030   · cmul 11034   < clt 11170  -cneg 11369   / cdiv 11798  ℕcn 12165  ℤcz 12515  seqcseq 13954  ↑cexp 14014

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 5231  ax-nul 5241  ax-pr 5370  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102

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 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 7363  df-oprab 7364  df-mpo 7365  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-neg 11371  df-z 12516  df-seq 13955  df-exp 14015

This theorem is referenced by:  0exp0e1  14019  expp1  14021  expneg  14022  expcllem  14025  mulexp  14054  expadd  14057  expmul  14060  exp0d  14093  leexp1a  14128  exple1  14130  bernneq  14182  modexp  14191  faclbnd4lem1  14246  faclbnd4lem3  14248  faclbnd4lem4  14249  cjexp  15103  absexp  15257  binom  15786  incexclem  15792  incexc  15793  climcndslem1  15805  pwdif  15824  fprodconst  15934  fallfac0  15984  bpoly0  16006  ege2le3  16046  eft0val  16070  demoivreALT  16159  pwp1fsum  16351  bits0  16388  0bits  16399  bitsinv1  16402  sadcadd  16418  smumullem  16452  numexp0  17037  psgnunilem4  19463  psgn0fv0  19477  psgnsn  19486  psgnprfval1  19488  cnfldexp  21394  expmhm  21426  expcn  24849  iblcnlem1  25765  itgcnlem  25767  dvexp  25930  dvexp2  25931  plyconst  26181  0dgr  26220  0dgrb  26221  aaliou3lem2  26320  cxp0  26647  1cubr  26819  log2ublem3  26925  basellem2  27059  basellem5  27062  lgsquad2lem2  27362  0dp2dp  32983  fldext2chn  33888  oddpwdc  34514  breprexp  34793  subfacval2  35385  fwddifn0  36362  stoweidlem19  46465  fmtno0  48015  bits0ALTV  48167  0dig2nn0e  49100  0dig2nn0o  49101  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  nn0sumshdiglem1  49109  nn0sumshdiglem2  49110