Theorem 0cn 10220

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 10192	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 10183	. . . 4 ⊢ i ∈ ℂ
3		mulcl 10208	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 710	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 10182	. . 3 ⊢ 1 ∈ ℂ
6		addcl 10206	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 710	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2832	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2135  (class class class)co 6809  ℂcc 10122  0cc0 10124  1c1 10125  ici 10126   + caddc 10127   · cmul 10129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-ext 2736  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-mulcl 10186  ax-i2m1 10192

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1850  df-cleq 2749  df-clel 2752

This theorem is referenced by:  0cnd  10221  c0ex  10222  1re  10227  00id  10399  mul02lem1  10400  mul02  10402  mul01  10403  addid1  10404  addid2  10407  negcl  10469  subid  10488  subid1  10489  neg0  10515  negid  10516  negsub  10517  subneg  10518  negneg  10519  negeq0  10523  negsubdi  10525  renegcli  10530  mulneg1  10654  msqge0  10737  ixi  10844  muleqadd  10859  div0  10903  ofsubge0  11207  0m0e0  11318  elznn0  11580  ser0  13043  0exp0e1  13055  0exp  13085  sq0  13145  sqeqor  13168  binom2  13169  bcval5  13295  s1co  13775  shftval3  14011  shftidt2  14016  cjne0  14098  sqrt0  14177  abs0  14220  abs00bd  14226  abs2dif  14267  clim0  14432  climz  14475  serclim0  14503  rlimneg  14572  sumrblem  14637  fsumcvg  14638  summolem2a  14641  sumss  14650  fsumss  14651  fsumcvg2  14653  fsumsplit  14666  sumsplit  14694  fsumrelem  14734  fsumrlim  14738  fsumo1  14739  0fallfac  14963  0risefac  14964  binomfallfac  14967  fsumcube  14986  ef0  15016  eftlub  15034  sin0  15074  tan0  15076  divalglem9  15322  sadadd2lem2  15370  sadadd3  15381  bezout  15458  pcmpt2  15795  4sqlem11  15857  ramcl  15931  4001lem2  16047  odadd1  18447  cnaddablx  18467  cnaddabl  18468  cnaddid  18469  frgpnabllem1  18472  cncrng  19965  cnfld0  19968  cnbl0  22774  cnblcld  22775  cnfldnm  22779  xrge0gsumle  22833  xrge0tsms  22834  cnheibor  22951  cnlmod  23136  csscld  23244  clsocv  23245  cnflduss  23348  cnfldcusp  23349  rrxmvallem  23383  rrxmval  23384  mbfss  23608  mbfmulc2lem  23609  0plef  23634  0pledm  23635  itg1ge0  23648  itg1addlem4  23661  itg2splitlem  23710  itg2addlem  23720  ibl0  23748  iblcnlem  23750  iblss2  23767  itgss3  23776  dvconst  23875  dvcnp2  23878  dvrec  23913  dvexp3  23936  dveflem  23937  dvef  23938  dv11cn  23959  lhop1lem  23971  plyun0  24148  plyeq0lem  24161  coeeulem  24175  coeeu  24176  coef3  24183  dgrle  24194  0dgrb  24197  coefv0  24199  coemulc  24206  coe1termlem  24209  coe1term  24210  dgr0  24213  dgrmulc  24222  dgrcolem2  24225  vieta1lem2  24261  iaa  24275  aareccl  24276  aalioulem3  24284  taylthlem2  24323  psercn  24375  pserdvlem2  24377  abelthlem2  24381  abelthlem3  24382  abelthlem5  24384  abelthlem7  24387  abelth  24390  sin2kpi  24430  cos2kpi  24431  sinkpi  24466  efopn  24599  logtayl  24601  cxpval  24605  0cxp  24607  cxpexp  24609  cxpcl  24615  cxpge0  24624  mulcxplem  24625  mulcxp  24626  cxpmul2  24630  dvsqrt  24678  dvcnsqrt  24680  cxpcn3  24684  abscxpbnd  24689  efrlim  24891  ftalem2  24995  ftalem3  24996  ftalem4  24997  ftalem5  24998  ftalem7  25000  prmorcht  25099  muinv  25114  1sgm2ppw  25120  logfacbnd3  25143  logexprlim  25145  dchrelbas2  25157  dchrmulid2  25172  dchrfi  25175  dchrinv  25181  lgsdir2  25250  lgsdir  25252  dchrvmasumiflem1  25385  dchrvmasumiflem2  25386  rpvmasum2  25396  log2sumbnd  25428  selberg2lem  25434  logdivbnd  25440  ax5seglem8  26011  axlowdimlem6  26022  axlowdimlem13  26029  ex-co  27602  avril1  27626  vc0  27734  vcz  27735  cnaddabloOLD  27741  cnidOLD  27742  ipasslem8  27997  siilem2  28012  hvmul0  28186  hi01  28258  norm-iii  28302  h1de2ctlem  28719  pjmuli  28853  pjneli  28887  eigre  28999  eigorth  29002  elnlfn  29092  0cnfn  29144  0lnfn  29149  lnopunilem2  29175  xrge0tsmsd  30090  qqh0  30333  qqhcn  30340  eulerpartlemgs2  30747  sgnneg  30907  breprexpnat  31017  hgt750lem2  31035  subfacp1lem6  31470  sinccvglem  31869  abs2sqle  31877  abs2sqlt  31878  tan2h  33710  poimirlem16  33734  poimirlem19  33737  poimirlem31  33749  mblfinlem2  33756  ovoliunnfl  33760  voliunnfl  33762  dvtanlem  33768  ftc1anclem5  33798  cntotbnd  33904  flcidc  38242  dvconstbi  39031  expgrowth  39032  dvradcnv2  39044  binomcxplemdvbinom  39050  binomcxplemnotnn0  39053  xralrple3  40084  negcncfg  40593  ioodvbdlimc1  40647  ioodvbdlimc2  40649  itgsinexplem1  40668  stoweidlem26  40742  stoweidlem36  40752  stoweidlem55  40771  stirlinglem8  40797  fourierdlem103  40925  sqwvfoura  40944  sqwvfourb  40945  ovn0lem  41281  nn0sumshdiglemA  42919  nn0sumshdiglemB  42920  nn0sumshdiglem1  42921  sec0  43010