Theorem 0cn 11282

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11252	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11243	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11268	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 691	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11242	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11266	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 691	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2841	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  0cc0 11184  1c1 11185  ici 11186   + caddc 11187   · cmul 11189

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-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-i2m1 11252

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  0cnd  11283  c0ex  11284  1re  11290  00id  11465  mul02lem1  11466  mul02  11468  mul01  11469  addrid  11470  addlid  11473  negcl  11536  subid  11555  subid1  11556  neg0  11582  negid  11583  negsub  11584  subneg  11585  negneg  11586  negeq0  11590  negsubdi  11592  renegcli  11597  mulneg1  11726  msqge0  11811  ixi  11919  muleqadd  11934  diveq0  11959  div0  11982  div0OLD  11983  ofsubge0  12292  0m0e0  12413  nn0sscn  12558  elznn0  12654  ser0  14105  0exp0e1  14117  0exp  14148  sq0  14241  sqeqor  14265  binom2  14266  bcval5  14367  s1co  14882  shftval3  15125  shftidt2  15130  cjne0  15212  sqrt0  15290  abs0  15334  abs00bd  15340  abs2dif  15381  clim0  15552  climz  15595  serclim0  15623  rlimneg  15695  sumrblem  15759  fsumcvg  15760  summolem2a  15763  sumss  15772  fsumss  15773  fsumcvg2  15775  fsumsplit  15789  sumsplit  15816  fsumrelem  15855  fsumrlim  15859  fsumo1  15860  0fallfac  16085  0risefac  16086  binomfallfac  16089  fsumcube  16108  ef0  16139  eftlub  16157  sin0  16197  tan0  16199  divalglem9  16449  sadadd2lem2  16496  sadadd3  16507  bezout  16590  pcmpt2  16940  4sqlem11  17002  ramcl  17076  4001lem2  17189  odadd1  19890  cnaddablx  19910  cnaddabl  19911  cnaddid  19912  frgpnabllem1  19915  cncrng  21424  cncrngOLD  21425  cnfld0  21428  pzriprnglem5  21519  pzriprnglem6  21520  psdmplcl  22189  cnbl0  24815  cnblcld  24816  cnfldnm  24820  xrge0gsumle  24874  xrge0tsms  24875  cnheibor  25006  cnlmod  25192  csscld  25302  clsocv  25303  cnflduss  25409  cnfldcusp  25410  rrxmvallem  25457  rrxmval  25458  mbfss  25700  mbfmulc2lem  25701  0plef  25726  0pledm  25727  itg1ge0  25740  itg1addlem4  25753  itg1addlem4OLD  25754  itg2splitlem  25803  itg2addlem  25813  ibl0  25842  iblcnlem  25844  iblss2  25861  itgss3  25870  dvconst  25972  dvcnp2  25975  dvcnp2OLD  25976  dvrec  26013  dvexp3  26036  dveflem  26037  dv11cn  26060  lhop1lem  26072  plyun0  26256  plyeq0lem  26269  coeeulem  26283  coeeu  26284  coef3  26291  dgrle  26302  0dgrb  26305  coefv0  26307  coemulc  26314  coe1termlem  26317  coe1term  26318  dgr0  26322  dgrmulc  26331  dgrcolem2  26334  vieta1lem2  26371  iaa  26385  aareccl  26386  aalioulem3  26394  taylthlem2  26434  taylthlem2OLD  26435  psercn  26488  pserdvlem2  26490  abelthlem2  26494  abelthlem3  26495  abelthlem5  26497  abelthlem7  26500  abelth  26503  sin2kpi  26543  cos2kpi  26544  sinkpi  26582  efopn  26718  logtayl  26720  cxpval  26724  0cxp  26726  cxpexp  26728  cxpcl  26734  cxpge0  26743  mulcxplem  26744  mulcxp  26745  cxpmul2  26749  dvsqrt  26802  dvcnsqrt  26804  cxpcn3  26809  abscxpbnd  26814  efrlim  27030  efrlimOLD  27031  ftalem2  27135  ftalem3  27136  ftalem4  27137  ftalem5  27138  ftalem7  27140  prmorcht  27239  muinv  27254  1sgm2ppw  27262  logfacbnd3  27285  logexprlim  27287  dchrelbas2  27299  dchrmullid  27314  dchrfi  27317  dchrinv  27323  lgsdir2  27392  lgsdir  27394  addsqnreup  27505  dchrvmasumiflem1  27563  dchrvmasumiflem2  27564  rpvmasum2  27574  log2sumbnd  27606  selberg2lem  27612  logdivbnd  27618  ax5seglem8  28969  axlowdimlem6  28980  axlowdimlem13  28987  ex-co  30470  avril1  30495  vc0  30606  vcz  30607  cnaddabloOLD  30613  cnidOLD  30614  ipasslem8  30869  siilem2  30884  hvmul0  31056  hi01  31128  norm-iii  31172  h1de2ctlem  31587  pjmuli  31721  pjneli  31755  eigre  31867  eigorth  31870  elnlfn  31960  0cnfn  32012  0lnfn  32017  lnopunilem2  32043  xrge0tsmsd  33041  constrsscn  33730  qqh0  33930  qqhcn  33937  eulerpartlemgs2  34345  sgnneg  34505  breprexpnat  34611  hgt750lem2  34629  subfacp1lem6  35153  sinccvglem  35640  abs2sqle  35648  abs2sqlt  35649  tan2h  37572  poimirlem16  37596  poimirlem19  37599  poimirlem31  37611  mblfinlem2  37618  ovoliunnfl  37622  voliunnfl  37624  dvtanlem  37629  ftc1anclem5  37657  cntotbnd  37756  60lcm7e420  41967  lcmineqlem10  41995  3lexlogpow5ineq1  42011  sn-1ne2  42254  0tie0  42304  sn-it0e0  42391  addinvcom  42407  sn-0tie0  42415  fltnltalem  42617  flcidc  43131  dvconstbi  44303  expgrowth  44304  dvradcnv2  44316  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  xralrple3  45289  negcncfg  45802  ioodvbdlimc1  45854  ioodvbdlimc2  45856  itgsinexplem1  45875  stoweidlem26  45947  stoweidlem36  45957  stoweidlem55  45976  stirlinglem8  46002  fourierdlem103  46130  sqwvfoura  46149  sqwvfourb  46150  ovn0lem  46486  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0sumshdiglem1  48355  sec0  48852