Theorem exp0 12170

Description: Value of a complex number raised to the 0th power. Note that under our definition, 00=1, 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

Proof of Theorem exp0

Step	Hyp	Ref	Expression
1		0z 10900	. . 3
2		expval 12168	. . 3
3	1, 2	mpan2 671	. 2
4		eqid 2457	. . 3
5	4	iftruei 3948	. 2
6	3, 5	syl6eq 2514	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  ifcif 3941  {csn 4029   class class class wbr 4452  X.cxp 5002  `cfv 5593  (class class class)co 6296  cc 9511  0cc0 9513  1c1 9514  cmul 9518  clt 9649  -ucneg 9829  cdiv 10231  cn 10561  cz 10889  seqcseq 12107  cexp 12166

This theorem is referenced by:  0exp0e1  12171  expp1  12173  expneg  12174  expcllem  12177  mulexp  12205  expadd  12208  expmul  12211  leexp1a  12224  exple1  12225  bernneq  12292  modexp  12301  exp0d  12304  faclbnd4lem1  12371  faclbnd4lem3  12373  faclbnd4lem4  12374  cjexp  12983  absexp  13137  binom  13642  incexclem  13648  incexc  13649  climcndslem1  13661  fprodconst  13782  ege2le3  13825  eft0val  13847  demoivreALT  13936  bits0  14078  0bits  14089  bitsinv1  14092  sadcadd  14108  smumullem  14142  numexp0  14562  psgnunilem4  16522  psgn0fv0  16536  psgnsn  16545  psgnprfval1  16547  cnfldexp  18451  expmhm  18485  expcn  21376  iblcnlem1  22194  itgcnlem  22196  dvexp  22356  dvexp2  22357  plyconst  22603  0dgr  22642  0dgrb  22643  aaliou3lem2  22739  cxp0  23051  1cubr  23173  log2ublem3  23279  basellem2  23355  basellem5  23358  lgsquad2lem2  23634  rusgranumwlk  24957  oddpwdc  28293  subfacval2  28631  fallfac0  29150  bpoly0  29812  m1expeven  31585  stoweidlem19  31801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-recs 7061  df-rdg 7095  df-neg 9831  df-z 10890  df-seq 12108  df-exp 12167