Theorem 0cn 11124

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11094	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11085	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11110	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11108	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2833	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  0cc0 11026  1c1 11027  ici 11028   + caddc 11029   · cmul 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-i2m1 11094

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

This theorem is referenced by:  0cnd  11125  c0ex  11126  1re  11132  00id  11308  mul02lem1  11309  mul02  11311  mul01  11312  addrid  11313  addlid  11316  negcl  11380  subid  11400  subid1  11401  neg0  11427  negid  11428  negsub  11429  subneg  11430  negneg  11431  negeq0  11435  negsubdi  11437  renegcli  11442  mulneg1  11573  msqge0  11658  ixi  11766  muleqadd  11781  diveq0  11806  div0  11829  div0OLD  11830  ofsubge0  12144  0m0e0  12260  nn0sscn  12406  elznn0  12503  ser0  13977  0exp0e1  13989  0exp  14020  sq0  14115  sqeqor  14139  binom2  14140  bcval5  14241  s1co  14756  shftval3  14999  shftidt2  15004  cjne0  15086  sqrt0  15164  abs0  15208  abs00bd  15214  abs2dif  15256  clim0  15429  climz  15472  serclim0  15500  rlimneg  15570  sumrblem  15634  fsumcvg  15635  summolem2a  15638  sumss  15647  fsumss  15648  fsumcvg2  15650  fsumsplit  15664  sumsplit  15691  fsumrelem  15730  fsumrlim  15734  fsumo1  15735  0fallfac  15960  0risefac  15961  binomfallfac  15964  fsumcube  15983  ef0  16014  eftlub  16034  sin0  16074  tan0  16076  divalglem9  16328  sadadd2lem2  16377  sadadd3  16388  bezout  16470  pcmpt2  16821  4sqlem11  16883  ramcl  16957  4001lem2  17069  odadd1  19777  cnaddablx  19797  cnaddabl  19798  cnaddid  19799  frgpnabllem1  19802  cncrng  21343  cncrngOLD  21344  cnfld0  21347  pzriprnglem5  21440  pzriprnglem6  21441  psdmplcl  22105  cnbl0  24717  cnblcld  24718  cnfldnm  24722  cnn0opn  24731  xrge0gsumle  24778  xrge0tsms  24779  cnheibor  24910  cnlmod  25096  csscld  25205  clsocv  25206  cnflduss  25312  cnfldcusp  25313  rrxmvallem  25360  rrxmval  25361  mbfss  25603  mbfmulc2lem  25604  0plef  25629  0pledm  25630  itg1ge0  25643  itg1addlem4  25656  itg2splitlem  25705  itg2addlem  25715  ibl0  25744  iblcnlem  25746  iblss2  25763  itgss3  25772  dvconst  25874  dvcnp2  25877  dvcnp2OLD  25878  dveflem  25939  dv11cn  25962  lhop1lem  25974  plyun0  26158  plyeq0lem  26171  coeeulem  26185  coeeu  26186  coef3  26193  dgrle  26204  0dgrb  26207  coefv0  26209  coemulc  26216  coe1termlem  26219  coe1term  26220  dgr0  26224  dgrmulc  26233  dgrcolem2  26236  vieta1lem2  26275  iaa  26289  aareccl  26290  aalioulem3  26298  taylthlem2  26338  taylthlem2OLD  26339  psercn  26392  pserdvlem2  26394  abelthlem2  26398  abelthlem3  26399  abelthlem5  26401  abelthlem7  26404  abelth  26407  sin2kpi  26448  cos2kpi  26449  sinkpi  26487  efopn  26623  logtayl  26625  cxpval  26629  0cxp  26631  cxpexp  26633  cxpcl  26639  cxpge0  26648  mulcxplem  26649  mulcxp  26650  cxpmul2  26654  dvsqrt  26707  dvcnsqrt  26709  cxpcn3  26714  abscxpbnd  26719  efrlim  26935  efrlimOLD  26936  ftalem2  27040  ftalem3  27041  ftalem4  27042  ftalem5  27043  ftalem7  27045  prmorcht  27144  muinv  27159  1sgm2ppw  27167  logfacbnd3  27190  logexprlim  27192  dchrelbas2  27204  dchrmullid  27219  dchrfi  27222  dchrinv  27228  lgsdir2  27297  lgsdir  27299  addsqnreup  27410  dchrvmasumiflem1  27468  dchrvmasumiflem2  27469  rpvmasum2  27479  log2sumbnd  27511  selberg2lem  27517  logdivbnd  27523  ax5seglem8  29009  axlowdimlem6  29020  axlowdimlem13  29027  ex-co  30513  avril1  30538  vc0  30649  vcz  30650  cnaddabloOLD  30656  cnidOLD  30657  ipasslem8  30912  siilem2  30927  hvmul0  31099  hi01  31171  norm-iii  31215  h1de2ctlem  31630  pjmuli  31764  pjneli  31798  eigre  31910  eigorth  31913  elnlfn  32003  0cnfn  32055  0lnfn  32060  lnopunilem2  32086  sgnneg  32914  xrge0tsmsd  33155  constrsscn  33897  qqh0  34141  qqhcn  34148  eulerpartlemgs2  34537  breprexpnat  34791  hgt750lem2  34809  subfacp1lem6  35379  sinccvglem  35866  abs2sqle  35874  abs2sqlt  35875  tan2h  37813  poimirlem16  37837  poimirlem19  37840  poimirlem31  37852  mblfinlem2  37859  ovoliunnfl  37863  voliunnfl  37865  ftc1anclem5  37898  cntotbnd  37997  60lcm7e420  42274  lcmineqlem10  42302  3lexlogpow5ineq1  42318  sn-1ne2  42530  0tie0  42580  sn-it0e0  42681  addinvcom  42697  sn-0tie0  42716  fltnltalem  42915  flcidc  43422  dvconstbi  44585  expgrowth  44586  dvradcnv2  44598  binomcxplemdvbinom  44604  binomcxplemnotnn0  44607  xralrple3  45628  negcncfg  46135  ioodvbdlimc1  46187  ioodvbdlimc2  46189  itgsinexplem1  46208  stoweidlem26  46280  stoweidlem36  46290  stoweidlem55  46309  stirlinglem8  46335  fourierdlem103  46463  sqwvfoura  46482  sqwvfourb  46483  ovn0lem  46819  nthrucw  47140  nn0sumshdiglemA  48875  nn0sumshdiglemB  48876  nn0sumshdiglem1  48877  sec0  50015