Theorem exp0 13488

Description: Value of a complex number raised to the 0th power. Note that under our definition, 0↑0 = 1 (0exp0e1 13489) , following the convention used by Gleason. Part of 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 12036	. . 3 ⊢ 0 ∈ ℤ
2		expval 13486	. . 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 2758	. . 3 ⊢ 0 = 0
5	4	iftruei 4430	. 2 ⊢ if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1
6	3, 5	eqtrdi 2809	1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ifcif 4423  {csn 4525   class class class wbr 5035   × cxp 5525  ‘cfv 6339  (class class class)co 7155  ℂcc 10578  0cc0 10580  1c1 10581   · cmul 10585   < clt 10718  -cneg 10914   / cdiv 11340  ℕcn 11679  ℤcz 12025  seqcseq 13423  ↑cexp 13484

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301  ax-1cn 10638  ax-addrcl 10641  ax-rnegex 10651  ax-cnre 10653

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-iota 6298  df-fun 6341  df-fv 6347  df-ov 7158  df-oprab 7159  df-mpo 7160  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-neg 10916  df-z 12026  df-seq 13424  df-exp 13485

This theorem is referenced by:  0exp0e1  13489  expp1  13491  expneg  13492  expcllem  13495  mulexp  13523  expadd  13526  expmul  13529  exp0d  13559  leexp1a  13594  exple1  13595  bernneq  13645  modexp  13654  faclbnd4lem1  13708  faclbnd4lem3  13710  faclbnd4lem4  13711  cjexp  14562  absexp  14717  binom  15238  incexclem  15244  incexc  15245  climcndslem1  15257  pwdif  15276  fprodconst  15385  fallfac0  15435  bpoly0  15457  ege2le3  15496  eft0val  15518  demoivreALT  15607  pwp1fsum  15797  bits0  15832  0bits  15843  bitsinv1  15846  sadcadd  15862  smumullem  15896  numexp0  16472  psgnunilem4  18697  psgn0fv0  18711  psgnsn  18720  psgnprfval1  18722  cnfldexp  20204  expmhm  20240  expcn  23578  iblcnlem1  24492  itgcnlem  24494  dvexp  24657  dvexp2  24658  plyconst  24907  0dgr  24946  0dgrb  24947  aaliou3lem2  25043  cxp0  25365  1cubr  25532  log2ublem3  25638  basellem2  25771  basellem5  25774  lgsquad2lem2  26073  0dp2dp  30711  oddpwdc  31844  breprexp  32136  subfacval2  32669  fwddifn0  34041  stoweidlem19  43055  fmtno0  44453  bits0ALTV  44592  0dig2nn0e  45419  0dig2nn0o  45420  nn0sumshdiglemA  45426  nn0sumshdiglemB  45427  nn0sumshdiglem1  45428  nn0sumshdiglem2  45429