Theorem 0cn 11337

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11307	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11298	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11323	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 705	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11297	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11321	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 705	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2861	1 ⊢ 0 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237  0cc0 11239  1c1 11240  ici 11241   + caddc 11242   · cmul 11244

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-i2m1 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  0cnd  11338  c0ex  11339  1re  11347  00id  11524  mul02lem1  11525  mul02  11527  mul01  11528  addrid  11529  addlid  11532  negcl  11596  subid  11616  subid1  11617  neg0  11643  negid  11644  negsub  11645  subneg  11646  negneg  11647  negeq0  11651  negsubdi  11653  renegcli  11658  mulneg1  11791  msqge0  11877  ixi  11985  muleqadd  12000  diveq0  12024  div0  12045  ofsubge0  12359  0m0e0  12501  nn0sscn  12651  elznn0  12748  ser0  14237  0exp0e1  14249  0exp  14280  sq0  14375  sqeqor  14401  binom2  14402  bcval5  14503  s1co  15026  shftval3  15272  shftidt2  15277  sgnneg  15296  cjne0  15373  sqrt0  15451  abs0  15495  abs00bd  15501  abs2dif  15543  clim0  15717  climz  15760  serclim0  15788  rlimneg  15858  sumrblem  15921  fsumcvg  15922  summolem2a  15925  sumss  15934  fsumss  15935  fsumcvg2  15937  fsumsplit  15951  sumsplit  15978  fsumrelem  16018  fsumrlim  16022  fsumo1  16023  0fallfac  16247  0risefac  16248  binomfallfac  16251  fsumcube  16270  ef0  16301  eftlub  16321  sin0  16361  tan0  16363  divalglem9  16615  sadadd2lem2  16664  sadadd3  16675  bezout  16760  pcmpt2  17115  4sqlem11  17177  ramcl  17251  4001lem2  17364  odadd1  20113  cnaddablx  20133  cnaddabl  20134  cnaddid  20135  frgpnabllem1  20138  cncrng  21751  cnfld0  21754  pzriprnglem5  21846  pzriprnglem6  21847  psdmplcl  22538  cnbl0  25147  cnblcld  25148  cnfldnm  25152  cnn0opn  25161  xrge0gsumle  25208  xrge0tsms  25209  cnheibor  25331  cnlmod  25516  csscld  25625  clsocv  25626  cnflduss  25732  cnfldcusp  25733  rrxmvallem  25780  rrxmval  25781  mbfss  26022  mbfmulc2lem  26023  0plef  26048  0pledm  26049  itg1ge0  26062  itg1addlem4  26075  itg2splitlem  26124  itg2addlem  26134  ibl0  26162  iblcnlem  26164  iblss2  26181  itgss3  26190  dvconst  26292  dvcnp2  26295  dveflem  26354  dv11cn  26376  lhop1lem  26388  plyun0  26570  plyeq0lem  26584  coeeulem  26598  coeeu  26599  coef3  26606  dgrle  26617  0dgrb  26620  coefv0  26622  coemulc  26629  coe1termlem  26632  coe1term  26633  dgr0  26636  dgrmulc  26645  dgrcolem2  26648  vieta1lem2  26689  iaaOLD  26709  aareccl  26710  aalioulem3  26718  taylthlem2  26758  psercn  26810  pserdvlem2  26812  abelthlem2  26816  abelthlem3  26817  abelthlem5  26819  abelthlem7  26822  abelth  26825  sin2kpi  26869  cos2kpi  26870  sinkpi  26907  efopn  27043  logtayl  27045  cxpval  27049  0cxp  27051  cxpexp  27053  cxpcl  27059  cxpge0  27068  mulcxplem  27069  mulcxp  27070  cxpmul2  27074  dvsqrt  27127  dvcnsqrt  27129  cxpcn3  27133  abscxpbnd  27138  efrlim  27354  ftalem2  27458  ftalem3  27459  ftalem4  27460  ftalem5  27461  ftalem7  27463  prmorcht  27562  muinv  27577  1sgm2ppw  27584  logfacbnd3  27607  logexprlim  27609  dchrelbas2  27621  dchrmullid  27636  dchrfi  27639  dchrinv  27645  lgsdir2  27714  lgsdir  27716  addsqnreup  27827  dchrvmasumiflem1  27885  dchrvmasumiflem2  27886  rpvmasum2  27896  log2sumbnd  27928  selberg2lem  27934  logdivbnd  27940  ax5seglem8  29571  axlowdimlem6  29582  axlowdimlem13  29589  ex-co  31096  avril1  31121  vc0  31233  vcz  31234  cnaddabloOLD  31240  cnidOLD  31241  ipasslem8  31496  siilem2  31511  hvmul0  31683  hi01  31755  norm-iii  31799  h1de2ctlem  32214  pjmuli  32348  pjneli  32382  eigre  32494  eigorth  32497  elnlfn  32587  0cnfn  32639  0lnfn  32644  lnopunilem2  32670  xrge0tsmsd  33733  constrsscn  34483  qqh0  34727  qqhcn  34734  eulerpartlemgs2  35123  breprexpnat  35374  hgt750lem2  35392  subfacp1lem6  36158  sinccvglem  36645  abs2sqle  36653  abs2sqlt  36654  tan2h  38803  poimirlem16  38822  poimirlem19  38825  poimirlem31  38837  mblfinlem2  38844  ovoliunnfl  38848  voliunnfl  38850  ftc1anclem5  38883  cntotbnd  38996  60lcm7e420  43326  lcmineqlem10  43354  3lexlogpow5ineq1  43370  25or6to4  43522  sn-1ne2  43596  0tie0  43638  sn-it0e0  43733  addinvcom  43749  sn-0tie0  43781  fltnltalem  43939  flcidc  44433  dvconstbi  45579  expgrowth  45580  dvradcnv2  45592  binomcxplemdvbinom  45598  binomcxplemnotnn0  45601  xralrple3  46658  negcncfg  47164  ioodvbdlimc1  47216  ioodvbdlimc2  47218  itgsinexplem1  47237  stoweidlem26  47309  stoweidlem36  47319  stoweidlem55  47338  stirlinglem8  47364  fourierdlem103  47492  sqwvfoura  47511  sqwvfourb  47512  ovn0lem  47848  sqrtnnaa  48186  sqrtnzqaa  48187  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  nn0sumshdiglem1  50064  sinh0  51241  cosh0  51245  tanh0  51251  sec0  51281