Theorem 0cn 11136

Description: Zero is a complex number. See also 0cnALT 11381. (Contributed by NM, 19-Feb-2005.)

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11106	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11097	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11122	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 693	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11120	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 693	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2833	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  0cc0 11038  1c1 11039  ici 11040   + caddc 11041   · cmul 11043

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  0cnd  11137  c0ex  11138  1re  11144  00id  11321  mul02lem1  11322  mul02  11324  mul01  11325  addrid  11326  addlid  11329  negcl  11393  subid  11413  subid1  11414  neg0  11440  negid  11441  negsub  11442  subneg  11443  negneg  11444  negeq0  11448  negsubdi  11450  renegcli  11455  mulneg1  11586  msqge0  11671  ixi  11779  muleqadd  11794  diveq0  11819  div0  11842  div0OLD  11843  ofsubge0  12158  0m0e0  12296  nn0sscn  12442  elznn0  12539  ser0  14016  0exp0e1  14028  0exp  14059  sq0  14154  sqeqor  14178  binom2  14179  bcval5  14280  s1co  14795  shftval3  15038  shftidt2  15043  cjne0  15125  sqrt0  15203  abs0  15247  abs00bd  15253  abs2dif  15295  clim0  15468  climz  15511  serclim0  15539  rlimneg  15609  sumrblem  15673  fsumcvg  15674  summolem2a  15677  sumss  15686  fsumss  15687  fsumcvg2  15689  fsumsplit  15703  sumsplit  15730  fsumrelem  15770  fsumrlim  15774  fsumo1  15775  0fallfac  16002  0risefac  16003  binomfallfac  16006  fsumcube  16025  ef0  16056  eftlub  16076  sin0  16116  tan0  16118  divalglem9  16370  sadadd2lem2  16419  sadadd3  16430  bezout  16512  pcmpt2  16864  4sqlem11  16926  ramcl  17000  4001lem2  17112  odadd1  19823  cnaddablx  19843  cnaddabl  19844  cnaddid  19845  frgpnabllem1  19848  cncrng  21373  cnfld0  21376  pzriprnglem5  21465  pzriprnglem6  21466  psdmplcl  22128  cnbl0  24738  cnblcld  24739  cnfldnm  24743  cnn0opn  24752  xrge0gsumle  24799  xrge0tsms  24800  cnheibor  24922  cnlmod  25107  csscld  25216  clsocv  25217  cnflduss  25323  cnfldcusp  25324  rrxmvallem  25371  rrxmval  25372  mbfss  25613  mbfmulc2lem  25614  0plef  25639  0pledm  25640  itg1ge0  25653  itg1addlem4  25666  itg2splitlem  25715  itg2addlem  25725  ibl0  25754  iblcnlem  25756  iblss2  25773  itgss3  25782  dvconst  25884  dvcnp2  25887  dveflem  25946  dv11cn  25968  lhop1lem  25980  plyun0  26162  plyeq0lem  26175  coeeulem  26189  coeeu  26190  coef3  26197  dgrle  26208  0dgrb  26211  coefv0  26213  coemulc  26220  coe1termlem  26223  coe1term  26224  dgr0  26227  dgrmulc  26236  dgrcolem2  26239  vieta1lem2  26277  iaa  26291  aareccl  26292  aalioulem3  26300  taylthlem2  26339  psercn  26391  pserdvlem2  26393  abelthlem2  26397  abelthlem3  26398  abelthlem5  26400  abelthlem7  26403  abelth  26406  sin2kpi  26447  cos2kpi  26448  sinkpi  26486  efopn  26622  logtayl  26624  cxpval  26628  0cxp  26630  cxpexp  26632  cxpcl  26638  cxpge0  26647  mulcxplem  26648  mulcxp  26649  cxpmul2  26653  dvsqrt  26706  dvcnsqrt  26708  cxpcn3  26712  abscxpbnd  26717  efrlim  26933  ftalem2  27037  ftalem3  27038  ftalem4  27039  ftalem5  27040  ftalem7  27042  prmorcht  27141  muinv  27156  1sgm2ppw  27163  logfacbnd3  27186  logexprlim  27188  dchrelbas2  27200  dchrmullid  27215  dchrfi  27218  dchrinv  27224  lgsdir2  27293  lgsdir  27295  addsqnreup  27406  dchrvmasumiflem1  27464  dchrvmasumiflem2  27465  rpvmasum2  27475  log2sumbnd  27507  selberg2lem  27513  logdivbnd  27519  ax5seglem8  29005  axlowdimlem6  29016  axlowdimlem13  29023  ex-co  30508  avril1  30533  vc0  30645  vcz  30646  cnaddabloOLD  30652  cnidOLD  30653  ipasslem8  30908  siilem2  30923  hvmul0  31095  hi01  31167  norm-iii  31211  h1de2ctlem  31626  pjmuli  31760  pjneli  31794  eigre  31906  eigorth  31909  elnlfn  31999  0cnfn  32051  0lnfn  32056  lnopunilem2  32082  sgnneg  32906  xrge0tsmsd  33134  constrsscn  33884  qqh0  34128  qqhcn  34135  eulerpartlemgs2  34524  breprexpnat  34778  hgt750lem2  34796  subfacp1lem6  35367  sinccvglem  35854  abs2sqle  35862  abs2sqlt  35863  tan2h  37933  poimirlem16  37957  poimirlem19  37960  poimirlem31  37972  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  ftc1anclem5  38018  cntotbnd  38117  60lcm7e420  42449  lcmineqlem10  42477  3lexlogpow5ineq1  42493  sn-1ne2  42703  0tie0  42747  sn-it0e0  42848  addinvcom  42864  sn-0tie0  42896  fltnltalem  43095  flcidc  43598  dvconstbi  44761  expgrowth  44762  dvradcnv2  44774  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  xralrple3  45803  negcncfg  46309  ioodvbdlimc1  46361  ioodvbdlimc2  46363  itgsinexplem1  46382  stoweidlem26  46454  stoweidlem36  46464  stoweidlem55  46483  stirlinglem8  46509  fourierdlem103  46637  sqwvfoura  46656  sqwvfourb  46657  ovn0lem  46993  nthrucw  47316  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  sec0  50235