Theorem 0cn 11298

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11268	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11259	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11284	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 705	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11258	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11282	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 705	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2858	1 ⊢ 0 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198  0cc0 11200  1c1 11201  ici 11202   + caddc 11203   · cmul 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-i2m1 11268

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  0cnd  11299  c0ex  11300  1re  11308  00id  11485  mul02lem1  11486  mul02  11488  mul01  11489  addrid  11490  addlid  11493  negcl  11557  subid  11577  subid1  11578  neg0  11604  negid  11605  negsub  11606  subneg  11607  negneg  11608  negeq0  11612  negsubdi  11614  renegcli  11619  mulneg1  11752  msqge0  11837  ixi  11945  muleqadd  11960  diveq0  11984  div0  12005  ofsubge0  12319  0m0e0  12461  nn0sscn  12611  elznn0  12708  ser0  14197  0exp0e1  14209  0exp  14240  sq0  14335  sqeqor  14360  binom2  14361  bcval5  14462  s1co  14984  shftval3  15229  shftidt2  15234  sgnneg  15253  cjne0  15330  sqrt0  15408  abs0  15452  abs00bd  15458  abs2dif  15500  clim0  15673  climz  15716  serclim0  15744  rlimneg  15814  sumrblem  15877  fsumcvg  15878  summolem2a  15881  sumss  15890  fsumss  15891  fsumcvg2  15893  fsumsplit  15907  sumsplit  15934  fsumrelem  15974  fsumrlim  15978  fsumo1  15979  0fallfac  16203  0risefac  16204  binomfallfac  16207  fsumcube  16226  ef0  16257  eftlub  16277  sin0  16317  tan0  16319  divalglem9  16571  sadadd2lem2  16620  sadadd3  16631  bezout  16716  pcmpt2  17071  4sqlem11  17133  ramcl  17207  4001lem2  17320  odadd1  20062  cnaddablx  20082  cnaddabl  20083  cnaddid  20084  frgpnabllem1  20087  cncrng  21699  cnfld0  21702  pzriprnglem5  21791  pzriprnglem6  21792  psdmplcl  22483  cnbl0  25092  cnblcld  25093  cnfldnm  25097  cnn0opn  25106  xrge0gsumle  25153  xrge0tsms  25154  cnheibor  25276  cnlmod  25461  csscld  25570  clsocv  25571  cnflduss  25677  cnfldcusp  25678  rrxmvallem  25725  rrxmval  25726  mbfss  25967  mbfmulc2lem  25968  0plef  25993  0pledm  25994  itg1ge0  26007  itg1addlem4  26020  itg2splitlem  26069  itg2addlem  26079  ibl0  26107  iblcnlem  26109  iblss2  26126  itgss3  26135  dvconst  26237  dvcnp2  26240  dveflem  26299  dv11cn  26321  lhop1lem  26333  plyun0  26515  plyeq0lem  26529  coeeulem  26543  coeeu  26544  coef3  26551  dgrle  26562  0dgrb  26565  coefv0  26567  coemulc  26574  coe1termlem  26577  coe1term  26578  dgr0  26581  dgrmulc  26590  dgrcolem2  26593  vieta1lem2  26634  iaaOLD  26652  aareccl  26653  aalioulem3  26661  taylthlem2  26701  psercn  26753  pserdvlem2  26755  abelthlem2  26759  abelthlem3  26760  abelthlem5  26762  abelthlem7  26765  abelth  26768  sin2kpi  26812  cos2kpi  26813  sinkpi  26850  efopn  26986  logtayl  26988  cxpval  26992  0cxp  26994  cxpexp  26996  cxpcl  27002  cxpge0  27011  mulcxplem  27012  mulcxp  27013  cxpmul2  27017  dvsqrt  27070  dvcnsqrt  27072  cxpcn3  27076  abscxpbnd  27081  efrlim  27297  ftalem2  27401  ftalem3  27402  ftalem4  27403  ftalem5  27404  ftalem7  27406  prmorcht  27505  muinv  27520  1sgm2ppw  27527  logfacbnd3  27550  logexprlim  27552  dchrelbas2  27564  dchrmullid  27579  dchrfi  27582  dchrinv  27588  lgsdir2  27657  lgsdir  27659  addsqnreup  27770  dchrvmasumiflem1  27828  dchrvmasumiflem2  27829  rpvmasum2  27839  log2sumbnd  27871  selberg2lem  27877  logdivbnd  27883  ax5seglem8  29514  axlowdimlem6  29525  axlowdimlem13  29532  ex-co  31039  avril1  31064  vc0  31176  vcz  31177  cnaddabloOLD  31183  cnidOLD  31184  ipasslem8  31439  siilem2  31454  hvmul0  31626  hi01  31698  norm-iii  31742  h1de2ctlem  32157  pjmuli  32291  pjneli  32325  eigre  32437  eigorth  32440  elnlfn  32530  0cnfn  32582  0lnfn  32587  lnopunilem2  32613  xrge0tsmsd  33634  constrsscn  34372  qqh0  34616  qqhcn  34623  eulerpartlemgs2  35012  breprexpnat  35263  hgt750lem2  35281  subfacp1lem6  35950  sinccvglem  36437  abs2sqle  36445  abs2sqlt  36446  tan2h  38535  poimirlem16  38554  poimirlem19  38557  poimirlem31  38569  mblfinlem2  38576  ovoliunnfl  38580  voliunnfl  38582  ftc1anclem5  38615  cntotbnd  38730  60lcm7e420  43060  lcmineqlem10  43088  3lexlogpow5ineq1  43104  25or6to4  43256  sn-1ne2  43330  0tie0  43372  sn-it0e0  43467  addinvcom  43483  sn-0tie0  43515  fltnltalem  43673  flcidc  44171  dvconstbi  45317  expgrowth  45318  dvradcnv2  45330  binomcxplemdvbinom  45336  binomcxplemnotnn0  45339  xralrple3  46384  negcncfg  46890  ioodvbdlimc1  46942  ioodvbdlimc2  46944  itgsinexplem1  46963  stoweidlem26  47035  stoweidlem36  47045  stoweidlem55  47064  stirlinglem8  47090  fourierdlem103  47218  sqwvfoura  47237  sqwvfourb  47238  ovn0lem  47574  sqrtnnaa  47912  sqrtnzqaa  47913  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0sumshdiglem1  49732  sec0  50852