Theorem exp0 14027

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ifcif 4527  {csn 4627   class class class wbr 5147   × cxp 5673  ‘cfv 6540  (class class class)co 7404  ℂcc 11104  0cc0 11106  1c1 11107   · cmul 11111   < clt 11244  -cneg 11441   / cdiv 11867  ℕcn 12208  ℤcz 12554  seqcseq 13962  ↑cexp 14023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-1cn 11164  ax-addrcl 11167  ax-rnegex 11177  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-iota 6492  df-fun 6542  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-neg 11443  df-z 12555  df-seq 13963  df-exp 14024

This theorem is referenced by:  0exp0e1  14028  expp1  14030  expneg  14031  expcllem  14034  mulexp  14063  expadd  14066  expmul  14069  exp0d  14101  leexp1a  14136  exple1  14137  bernneq  14188  modexp  14197  faclbnd4lem1  14249  faclbnd4lem3  14251  faclbnd4lem4  14252  cjexp  15093  absexp  15247  binom  15772  incexclem  15778  incexc  15779  climcndslem1  15791  pwdif  15810  fprodconst  15918  fallfac0  15968  bpoly0  15990  ege2le3  16029  eft0val  16051  demoivreALT  16140  pwp1fsum  16330  bits0  16365  0bits  16376  bitsinv1  16379  sadcadd  16395  smumullem  16429  numexp0  17005  psgnunilem4  19358  psgn0fv0  19372  psgnsn  19381  psgnprfval1  19383  cnfldexp  20963  expmhm  20999  expcn  24370  iblcnlem1  25287  itgcnlem  25289  dvexp  25452  dvexp2  25453  plyconst  25702  0dgr  25741  0dgrb  25742  aaliou3lem2  25838  cxp0  26160  1cubr  26327  log2ublem3  26433  basellem2  26566  basellem5  26569  lgsquad2lem2  26868  0dp2dp  32053  oddpwdc  33291  breprexp  33583  subfacval2  34116  fwddifn0  35074  gg-expcn  35102  stoweidlem19  44670  fmtno0  46143  bits0ALTV  46282  0dig2nn0e  47200  0dig2nn0o  47201  nn0sumshdiglemA  47207  nn0sumshdiglemB  47208  nn0sumshdiglem1  47209  nn0sumshdiglem2  47210