Theorem 0cn 11225

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11195	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11186	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11211	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11185	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11209	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2831	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  0cc0 11127  1c1 11128  ici 11129   + caddc 11130   · cmul 11132

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-i2m1 11195

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

This theorem is referenced by:  0cnd  11226  c0ex  11227  1re  11233  00id  11408  mul02lem1  11409  mul02  11411  mul01  11412  addrid  11413  addlid  11416  negcl  11480  subid  11500  subid1  11501  neg0  11527  negid  11528  negsub  11529  subneg  11530  negneg  11531  negeq0  11535  negsubdi  11537  renegcli  11542  mulneg1  11671  msqge0  11756  ixi  11864  muleqadd  11879  diveq0  11904  div0  11927  div0OLD  11928  ofsubge0  12237  0m0e0  12358  nn0sscn  12504  elznn0  12601  ser0  14070  0exp0e1  14082  0exp  14113  sq0  14208  sqeqor  14232  binom2  14233  bcval5  14334  s1co  14850  shftval3  15093  shftidt2  15098  cjne0  15180  sqrt0  15258  abs0  15302  abs00bd  15308  abs2dif  15349  clim0  15520  climz  15563  serclim0  15591  rlimneg  15661  sumrblem  15725  fsumcvg  15726  summolem2a  15729  sumss  15738  fsumss  15739  fsumcvg2  15741  fsumsplit  15755  sumsplit  15782  fsumrelem  15821  fsumrlim  15825  fsumo1  15826  0fallfac  16051  0risefac  16052  binomfallfac  16055  fsumcube  16074  ef0  16105  eftlub  16125  sin0  16165  tan0  16167  divalglem9  16418  sadadd2lem2  16467  sadadd3  16478  bezout  16560  pcmpt2  16911  4sqlem11  16973  ramcl  17047  4001lem2  17159  odadd1  19827  cnaddablx  19847  cnaddabl  19848  cnaddid  19849  frgpnabllem1  19852  cncrng  21349  cncrngOLD  21350  cnfld0  21353  pzriprnglem5  21444  pzriprnglem6  21445  psdmplcl  22098  cnbl0  24710  cnblcld  24711  cnfldnm  24715  cnn0opn  24724  xrge0gsumle  24771  xrge0tsms  24772  cnheibor  24903  cnlmod  25089  csscld  25199  clsocv  25200  cnflduss  25306  cnfldcusp  25307  rrxmvallem  25354  rrxmval  25355  mbfss  25597  mbfmulc2lem  25598  0plef  25623  0pledm  25624  itg1ge0  25637  itg1addlem4  25650  itg2splitlem  25699  itg2addlem  25709  ibl0  25738  iblcnlem  25740  iblss2  25757  itgss3  25766  dvconst  25868  dvcnp2  25871  dvcnp2OLD  25872  dveflem  25933  dv11cn  25956  lhop1lem  25968  plyun0  26152  plyeq0lem  26165  coeeulem  26179  coeeu  26180  coef3  26187  dgrle  26198  0dgrb  26201  coefv0  26203  coemulc  26210  coe1termlem  26213  coe1term  26214  dgr0  26218  dgrmulc  26227  dgrcolem2  26230  vieta1lem2  26269  iaa  26283  aareccl  26284  aalioulem3  26292  taylthlem2  26332  taylthlem2OLD  26333  psercn  26386  pserdvlem2  26388  abelthlem2  26392  abelthlem3  26393  abelthlem5  26395  abelthlem7  26398  abelth  26401  sin2kpi  26442  cos2kpi  26443  sinkpi  26481  efopn  26617  logtayl  26619  cxpval  26623  0cxp  26625  cxpexp  26627  cxpcl  26633  cxpge0  26642  mulcxplem  26643  mulcxp  26644  cxpmul2  26648  dvsqrt  26701  dvcnsqrt  26703  cxpcn3  26708  abscxpbnd  26713  efrlim  26929  efrlimOLD  26930  ftalem2  27034  ftalem3  27035  ftalem4  27036  ftalem5  27037  ftalem7  27039  prmorcht  27138  muinv  27153  1sgm2ppw  27161  logfacbnd3  27184  logexprlim  27186  dchrelbas2  27198  dchrmullid  27213  dchrfi  27216  dchrinv  27222  lgsdir2  27291  lgsdir  27293  addsqnreup  27404  dchrvmasumiflem1  27462  dchrvmasumiflem2  27463  rpvmasum2  27473  log2sumbnd  27505  selberg2lem  27511  logdivbnd  27517  ax5seglem8  28861  axlowdimlem6  28872  axlowdimlem13  28879  ex-co  30365  avril1  30390  vc0  30501  vcz  30502  cnaddabloOLD  30508  cnidOLD  30509  ipasslem8  30764  siilem2  30779  hvmul0  30951  hi01  31023  norm-iii  31067  h1de2ctlem  31482  pjmuli  31616  pjneli  31650  eigre  31762  eigorth  31765  elnlfn  31855  0cnfn  31907  0lnfn  31912  lnopunilem2  31938  sgnneg  32758  xrge0tsmsd  33002  constrsscn  33720  qqh0  33961  qqhcn  33968  eulerpartlemgs2  34358  breprexpnat  34612  hgt750lem2  34630  subfacp1lem6  35153  sinccvglem  35640  abs2sqle  35648  abs2sqlt  35649  tan2h  37582  poimirlem16  37606  poimirlem19  37609  poimirlem31  37621  mblfinlem2  37628  ovoliunnfl  37632  voliunnfl  37634  ftc1anclem5  37667  cntotbnd  37766  60lcm7e420  41969  lcmineqlem10  41997  3lexlogpow5ineq1  42013  sn-1ne2  42262  0tie0  42311  sn-it0e0  42405  addinvcom  42421  sn-0tie0  42429  fltnltalem  42632  flcidc  43141  dvconstbi  44306  expgrowth  44307  dvradcnv2  44319  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  xralrple3  45349  negcncfg  45858  ioodvbdlimc1  45910  ioodvbdlimc2  45912  itgsinexplem1  45931  stoweidlem26  46003  stoweidlem36  46013  stoweidlem55  46032  stirlinglem8  46058  fourierdlem103  46186  sqwvfoura  46205  sqwvfourb  46206  ovn0lem  46542  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  nn0sumshdiglem1  48549  sec0  49572