Theorem exp0 14028

Description: Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14029), 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 12566	. . 3 ⊢ 0 ∈ ℤ
2		expval 14026	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
3	1, 2	mpan2 688	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))))
4		eqid 2724	. . 3 ⊢ 0 = 0
5	4	iftruei 4527	. 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 1533   ∈ wcel 2098  ifcif 4520  {csn 4620   class class class wbr 5138   × cxp 5664  ‘cfv 6533  (class class class)co 7401  ℂcc 11104  0cc0 11106  1c1 11107   · cmul 11111   < clt 11245  -cneg 11442   / cdiv 11868  ℕcn 12209  ℤcz 12555  seqcseq 13963  ↑cexp 14024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-1cn 11164  ax-addrcl 11167  ax-rnegex 11177  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-iota 6485  df-fun 6535  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-neg 11444  df-z 12556  df-seq 13964  df-exp 14025

This theorem is referenced by:  0exp0e1  14029  expp1  14031  expneg  14032  expcllem  14035  mulexp  14064  expadd  14067  expmul  14070  exp0d  14102  leexp1a  14137  exple1  14138  bernneq  14189  modexp  14198  faclbnd4lem1  14250  faclbnd4lem3  14252  faclbnd4lem4  14253  cjexp  15094  absexp  15248  binom  15773  incexclem  15779  incexc  15780  climcndslem1  15792  pwdif  15811  fprodconst  15919  fallfac0  15969  bpoly0  15991  ege2le3  16030  eft0val  16052  demoivreALT  16141  pwp1fsum  16331  bits0  16366  0bits  16377  bitsinv1  16380  sadcadd  16396  smumullem  16430  numexp0  17008  psgnunilem4  19407  psgn0fv0  19421  psgnsn  19430  psgnprfval1  19432  cnfldexp  21262  expmhm  21298  expcn  24712  expcnOLD  24714  iblcnlem1  25639  itgcnlem  25641  dvexp  25807  dvexp2  25808  plyconst  26060  0dgr  26099  0dgrb  26100  aaliou3lem2  26197  cxp0  26520  1cubr  26690  log2ublem3  26796  basellem2  26930  basellem5  26933  lgsquad2lem2  27234  0dp2dp  32542  oddpwdc  33842  breprexp  34134  subfacval2  34667  fwddifn0  35631  stoweidlem19  45220  fmtno0  46693  bits0ALTV  46832  0dig2nn0e  47486  0dig2nn0o  47487  nn0sumshdiglemA  47493  nn0sumshdiglemB  47494  nn0sumshdiglem1  47495  nn0sumshdiglem2  47496