Theorem 0cn 11142

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11112	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11103	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11128	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11102	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11126	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2825	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042  0cc0 11044  1c1 11045  ici 11046   + caddc 11047   · cmul 11049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-i2m1 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  0cnd  11143  c0ex  11144  1re  11150  00id  11325  mul02lem1  11326  mul02  11328  mul01  11329  addrid  11330  addlid  11333  negcl  11397  subid  11417  subid1  11418  neg0  11444  negid  11445  negsub  11446  subneg  11447  negneg  11448  negeq0  11452  negsubdi  11454  renegcli  11459  mulneg1  11590  msqge0  11675  ixi  11783  muleqadd  11798  diveq0  11823  div0  11846  div0OLD  11847  ofsubge0  12161  0m0e0  12277  nn0sscn  12423  elznn0  12520  ser0  13995  0exp0e1  14007  0exp  14038  sq0  14133  sqeqor  14157  binom2  14158  bcval5  14259  s1co  14775  shftval3  15018  shftidt2  15023  cjne0  15105  sqrt0  15183  abs0  15227  abs00bd  15233  abs2dif  15275  clim0  15448  climz  15491  serclim0  15519  rlimneg  15589  sumrblem  15653  fsumcvg  15654  summolem2a  15657  sumss  15666  fsumss  15667  fsumcvg2  15669  fsumsplit  15683  sumsplit  15710  fsumrelem  15749  fsumrlim  15753  fsumo1  15754  0fallfac  15979  0risefac  15980  binomfallfac  15983  fsumcube  16002  ef0  16033  eftlub  16053  sin0  16093  tan0  16095  divalglem9  16347  sadadd2lem2  16396  sadadd3  16407  bezout  16489  pcmpt2  16840  4sqlem11  16902  ramcl  16976  4001lem2  17088  odadd1  19754  cnaddablx  19774  cnaddabl  19775  cnaddid  19776  frgpnabllem1  19779  cncrng  21276  cncrngOLD  21277  cnfld0  21280  pzriprnglem5  21371  pzriprnglem6  21372  psdmplcl  22025  cnbl0  24637  cnblcld  24638  cnfldnm  24642  cnn0opn  24651  xrge0gsumle  24698  xrge0tsms  24699  cnheibor  24830  cnlmod  25016  csscld  25125  clsocv  25126  cnflduss  25232  cnfldcusp  25233  rrxmvallem  25280  rrxmval  25281  mbfss  25523  mbfmulc2lem  25524  0plef  25549  0pledm  25550  itg1ge0  25563  itg1addlem4  25576  itg2splitlem  25625  itg2addlem  25635  ibl0  25664  iblcnlem  25666  iblss2  25683  itgss3  25692  dvconst  25794  dvcnp2  25797  dvcnp2OLD  25798  dveflem  25859  dv11cn  25882  lhop1lem  25894  plyun0  26078  plyeq0lem  26091  coeeulem  26105  coeeu  26106  coef3  26113  dgrle  26124  0dgrb  26127  coefv0  26129  coemulc  26136  coe1termlem  26139  coe1term  26140  dgr0  26144  dgrmulc  26153  dgrcolem2  26156  vieta1lem2  26195  iaa  26209  aareccl  26210  aalioulem3  26218  taylthlem2  26258  taylthlem2OLD  26259  psercn  26312  pserdvlem2  26314  abelthlem2  26318  abelthlem3  26319  abelthlem5  26321  abelthlem7  26324  abelth  26327  sin2kpi  26368  cos2kpi  26369  sinkpi  26407  efopn  26543  logtayl  26545  cxpval  26549  0cxp  26551  cxpexp  26553  cxpcl  26559  cxpge0  26568  mulcxplem  26569  mulcxp  26570  cxpmul2  26574  dvsqrt  26627  dvcnsqrt  26629  cxpcn3  26634  abscxpbnd  26639  efrlim  26855  efrlimOLD  26856  ftalem2  26960  ftalem3  26961  ftalem4  26962  ftalem5  26963  ftalem7  26965  prmorcht  27064  muinv  27079  1sgm2ppw  27087  logfacbnd3  27110  logexprlim  27112  dchrelbas2  27124  dchrmullid  27139  dchrfi  27142  dchrinv  27148  lgsdir2  27217  lgsdir  27219  addsqnreup  27330  dchrvmasumiflem1  27388  dchrvmasumiflem2  27389  rpvmasum2  27399  log2sumbnd  27431  selberg2lem  27437  logdivbnd  27443  ax5seglem8  28839  axlowdimlem6  28850  axlowdimlem13  28857  ex-co  30340  avril1  30365  vc0  30476  vcz  30477  cnaddabloOLD  30483  cnidOLD  30484  ipasslem8  30739  siilem2  30754  hvmul0  30926  hi01  30998  norm-iii  31042  h1de2ctlem  31457  pjmuli  31591  pjneli  31625  eigre  31737  eigorth  31740  elnlfn  31830  0cnfn  31882  0lnfn  31887  lnopunilem2  31913  sgnneg  32731  xrge0tsmsd  32975  constrsscn  33703  qqh0  33947  qqhcn  33954  eulerpartlemgs2  34344  breprexpnat  34598  hgt750lem2  34616  subfacp1lem6  35145  sinccvglem  35632  abs2sqle  35640  abs2sqlt  35641  tan2h  37579  poimirlem16  37603  poimirlem19  37606  poimirlem31  37618  mblfinlem2  37625  ovoliunnfl  37629  voliunnfl  37631  ftc1anclem5  37664  cntotbnd  37763  60lcm7e420  41971  lcmineqlem10  41999  3lexlogpow5ineq1  42015  sn-1ne2  42226  0tie0  42276  sn-it0e0  42377  addinvcom  42393  sn-0tie0  42412  fltnltalem  42623  flcidc  43132  dvconstbi  44296  expgrowth  44297  dvradcnv2  44309  binomcxplemdvbinom  44315  binomcxplemnotnn0  44318  xralrple3  45343  negcncfg  45852  ioodvbdlimc1  45904  ioodvbdlimc2  45906  itgsinexplem1  45925  stoweidlem26  45997  stoweidlem36  46007  stoweidlem55  46026  stirlinglem8  46052  fourierdlem103  46180  sqwvfoura  46199  sqwvfourb  46200  ovn0lem  46536  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  nn0sumshdiglem1  48583  sec0  49722