Theorem 0cn 11188

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11160	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11151	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11176	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 690	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11150	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11174	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 690	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2829	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7393  ℂcc 11090  0cc0 11092  1c1 11093  ici 11094   + caddc 11095   · cmul 11097

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-mulcl 11154  ax-i2m1 11160

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809

This theorem is referenced by:  0cnd  11189  c0ex  11190  1re  11196  00id  11371  mul02lem1  11372  mul02  11374  mul01  11375  addrid  11376  addlid  11379  negcl  11442  subid  11461  subid1  11462  neg0  11488  negid  11489  negsub  11490  subneg  11491  negneg  11492  negeq0  11496  negsubdi  11498  renegcli  11503  mulneg1  11632  msqge0  11717  ixi  11825  muleqadd  11840  div0  11884  ofsubge0  12193  0m0e0  12314  nn0sscn  12459  elznn0  12555  ser0  14002  0exp0e1  14014  0exp  14045  sq0  14138  sqeqor  14162  binom2  14163  bcval5  14260  s1co  14766  shftval3  15005  shftidt2  15010  cjne0  15092  sqrt0  15170  abs0  15214  abs00bd  15220  abs2dif  15261  clim0  15432  climz  15475  serclim0  15503  rlimneg  15575  sumrblem  15639  fsumcvg  15640  summolem2a  15643  sumss  15652  fsumss  15653  fsumcvg2  15655  fsumsplit  15669  sumsplit  15696  fsumrelem  15735  fsumrlim  15739  fsumo1  15740  0fallfac  15963  0risefac  15964  binomfallfac  15967  fsumcube  15986  ef0  16016  eftlub  16034  sin0  16074  tan0  16076  divalglem9  16326  sadadd2lem2  16373  sadadd3  16384  bezout  16467  pcmpt2  16808  4sqlem11  16870  ramcl  16944  4001lem2  17057  odadd1  19676  cnaddablx  19696  cnaddabl  19697  cnaddid  19698  frgpnabllem1  19701  cncrng  20900  cnfld0  20903  cnbl0  24219  cnblcld  24220  cnfldnm  24224  xrge0gsumle  24278  xrge0tsms  24279  cnheibor  24400  cnlmod  24585  csscld  24695  clsocv  24696  cnflduss  24802  cnfldcusp  24803  rrxmvallem  24850  rrxmval  24851  mbfss  25092  mbfmulc2lem  25093  0plef  25118  0pledm  25119  itg1ge0  25132  itg1addlem4  25145  itg1addlem4OLD  25146  itg2splitlem  25195  itg2addlem  25205  ibl0  25233  iblcnlem  25235  iblss2  25252  itgss3  25261  dvconst  25363  dvcnp2  25366  dvrec  25401  dvexp3  25424  dveflem  25425  dv11cn  25447  lhop1lem  25459  plyun0  25640  plyeq0lem  25653  coeeulem  25667  coeeu  25668  coef3  25675  dgrle  25686  0dgrb  25689  coefv0  25691  coemulc  25698  coe1termlem  25701  coe1term  25702  dgr0  25705  dgrmulc  25714  dgrcolem2  25717  vieta1lem2  25753  iaa  25767  aareccl  25768  aalioulem3  25776  taylthlem2  25815  psercn  25867  pserdvlem2  25869  abelthlem2  25873  abelthlem3  25874  abelthlem5  25876  abelthlem7  25879  abelth  25882  sin2kpi  25922  cos2kpi  25923  sinkpi  25960  efopn  26095  logtayl  26097  cxpval  26101  0cxp  26103  cxpexp  26105  cxpcl  26111  cxpge0  26120  mulcxplem  26121  mulcxp  26122  cxpmul2  26126  dvsqrt  26177  dvcnsqrt  26179  cxpcn3  26183  abscxpbnd  26188  efrlim  26401  ftalem2  26505  ftalem3  26506  ftalem4  26507  ftalem5  26508  ftalem7  26510  prmorcht  26609  muinv  26624  1sgm2ppw  26630  logfacbnd3  26653  logexprlim  26655  dchrelbas2  26667  dchrmullid  26682  dchrfi  26685  dchrinv  26691  lgsdir2  26760  lgsdir  26762  addsqnreup  26873  dchrvmasumiflem1  26931  dchrvmasumiflem2  26932  rpvmasum2  26942  log2sumbnd  26974  selberg2lem  26980  logdivbnd  26986  ax5seglem8  28059  axlowdimlem6  28070  axlowdimlem13  28077  ex-co  29556  avril1  29581  vc0  29690  vcz  29691  cnaddabloOLD  29697  cnidOLD  29698  ipasslem8  29953  siilem2  29968  hvmul0  30140  hi01  30212  norm-iii  30256  h1de2ctlem  30671  pjmuli  30805  pjneli  30839  eigre  30951  eigorth  30954  elnlfn  31044  0cnfn  31096  0lnfn  31101  lnopunilem2  31127  xrge0tsmsd  32080  qqh0  32793  qqhcn  32800  eulerpartlemgs2  33208  sgnneg  33368  breprexpnat  33475  hgt750lem2  33493  subfacp1lem6  34005  sinccvglem  34486  abs2sqle  34494  abs2sqlt  34495  tan2h  36282  poimirlem16  36306  poimirlem19  36309  poimirlem31  36321  mblfinlem2  36328  ovoliunnfl  36332  voliunnfl  36334  dvtanlem  36339  ftc1anclem5  36367  cntotbnd  36467  60lcm7e420  40678  lcmineqlem10  40706  3lexlogpow5ineq1  40722  sn-1ne2  40965  sn-it0e0  41068  addinvcom  41084  sn-0tie0  41092  fltnltalem  41184  flcidc  41685  dvconstbi  42862  expgrowth  42863  dvradcnv2  42875  binomcxplemdvbinom  42881  binomcxplemnotnn0  42884  xralrple3  43855  negcncfg  44368  ioodvbdlimc1  44420  ioodvbdlimc2  44422  itgsinexplem1  44441  stoweidlem26  44513  stoweidlem36  44523  stoweidlem55  44542  stirlinglem8  44568  fourierdlem103  44696  sqwvfoura  44715  sqwvfourb  44716  ovn0lem  45052  nn0sumshdiglemA  46951  nn0sumshdiglemB  46952  nn0sumshdiglem1  46953  sec0  47451