Theorem exp0 14116

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ifcif 4548  {csn 4648   class class class wbr 5166   × cxp 5698  ‘cfv 6573  (class class class)co 7448  ℂcc 11182  0cc0 11184  1c1 11185   · cmul 11189   < clt 11324  -cneg 11521   / cdiv 11947  ℕcn 12293  ℤcz 12639  seqcseq 14052  ↑cexp 14112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-1cn 11242  ax-addrcl 11245  ax-rnegex 11255  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-iota 6525  df-fun 6575  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-neg 11523  df-z 12640  df-seq 14053  df-exp 14113

This theorem is referenced by:  0exp0e1  14117  expp1  14119  expneg  14120  expcllem  14123  mulexp  14152  expadd  14155  expmul  14158  exp0d  14190  leexp1a  14225  exple1  14226  bernneq  14278  modexp  14287  faclbnd4lem1  14342  faclbnd4lem3  14344  faclbnd4lem4  14345  cjexp  15199  absexp  15353  binom  15878  incexclem  15884  incexc  15885  climcndslem1  15897  pwdif  15916  fprodconst  16026  fallfac0  16076  bpoly0  16098  ege2le3  16138  eft0val  16160  demoivreALT  16249  pwp1fsum  16439  bits0  16474  0bits  16485  bitsinv1  16488  sadcadd  16504  smumullem  16538  numexp0  17123  psgnunilem4  19539  psgn0fv0  19553  psgnsn  19562  psgnprfval1  19564  cnfldexp  21440  expmhm  21477  expcn  24915  expcnOLD  24917  iblcnlem1  25843  itgcnlem  25845  dvexp  26011  dvexp2  26012  plyconst  26265  0dgr  26304  0dgrb  26305  aaliou3lem2  26403  cxp0  26730  1cubr  26903  log2ublem3  27009  basellem2  27143  basellem5  27146  lgsquad2lem2  27447  0dp2dp  32873  fldext2chn  33719  oddpwdc  34319  breprexp  34610  subfacval2  35155  fwddifn0  36128  stoweidlem19  45940  fmtno0  47414  bits0ALTV  47553  0dig2nn0e  48346  0dig2nn0o  48347  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0sumshdiglem1  48355  nn0sumshdiglem2  48356