MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0cn Structured version   Visualization version   GIF version

Theorem 0cn 10317
Description: Zero is a complex number. See also 0cnALT 10555. (Contributed by NM, 19-Feb-2005.)
Assertion
Ref Expression
0cn 0 ∈ ℂ

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 10289 . 2 ((i · i) + 1) = 0
2 ax-icn 10280 . . . 4 i ∈ ℂ
3 mulcl 10305 . . . 4 ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
42, 2, 3mp2an 675 . . 3 (i · i) ∈ ℂ
5 ax-1cn 10279 . . 3 1 ∈ ℂ
6 addcl 10303 . . 3 (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
74, 5, 6mp2an 675 . 2 ((i · i) + 1) ∈ ℂ
81, 7eqeltrri 2882 1 0 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  (class class class)co 6874  cc 10219  0cc0 10221  1c1 10222  ici 10223   + caddc 10224   · cmul 10226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-mulcl 10283  ax-i2m1 10289
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-clel 2802
This theorem is referenced by:  0cnd  10318  c0ex  10319  1re  10325  00id  10496  mul02lem1  10497  mul02  10499  mul01  10500  addid1  10501  addid2  10504  negcl  10566  subid  10585  subid1  10586  neg0  10612  negid  10613  negsub  10614  subneg  10615  negneg  10616  negeq0  10620  negsubdi  10622  renegcli  10627  mulneg1  10751  msqge0  10834  ixi  10941  muleqadd  10956  div0  11000  ofsubge0  11304  0m0e0  11412  elznn0  11658  ser0  13076  0exp0e1  13088  0exp  13118  sq0  13178  sqeqor  13201  binom2  13202  bcval5  13325  s1co  13803  shftval3  14039  shftidt2  14044  cjne0  14126  sqrt0  14205  abs0  14248  abs00bd  14254  abs2dif  14295  clim0  14460  climz  14503  serclim0  14531  rlimneg  14600  sumrblem  14665  fsumcvg  14666  summolem2a  14669  sumss  14678  fsumss  14679  fsumcvg2  14681  fsumsplit  14694  sumsplit  14722  fsumrelem  14761  fsumrlim  14765  fsumo1  14766  0fallfac  14988  0risefac  14989  binomfallfac  14992  fsumcube  15011  ef0  15041  eftlub  15059  sin0  15099  tan0  15101  divalglem9  15344  sadadd2lem2  15391  sadadd3  15402  bezout  15479  pcmpt2  15814  4sqlem11  15876  ramcl  15950  4001lem2  16060  odadd1  18452  cnaddablx  18472  cnaddabl  18473  cnaddid  18474  frgpnabllem1  18477  cncrng  19975  cnfld0  19978  cnbl0  22790  cnblcld  22791  cnfldnm  22795  xrge0gsumle  22849  xrge0tsms  22850  cnheibor  22967  cnlmod  23152  csscld  23260  clsocv  23261  cnflduss  23364  cnfldcusp  23365  rrxmvallem  23399  rrxmval  23400  mbfss  23627  mbfmulc2lem  23628  0plef  23653  0pledm  23654  itg1ge0  23667  itg1addlem4  23680  itg2splitlem  23729  itg2addlem  23739  ibl0  23767  iblcnlem  23769  iblss2  23786  itgss3  23795  dvconst  23894  dvcnp2  23897  dvrec  23932  dvexp3  23955  dveflem  23956  dvef  23957  dv11cn  23978  lhop1lem  23990  plyun0  24167  plyeq0lem  24180  coeeulem  24194  coeeu  24195  coef3  24202  dgrle  24213  0dgrb  24216  coefv0  24218  coemulc  24225  coe1termlem  24228  coe1term  24229  dgr0  24232  dgrmulc  24241  dgrcolem2  24244  vieta1lem2  24280  iaa  24294  aareccl  24295  aalioulem3  24303  taylthlem2  24342  psercn  24394  pserdvlem2  24396  abelthlem2  24400  abelthlem3  24401  abelthlem5  24403  abelthlem7  24406  abelth  24409  sin2kpi  24450  cos2kpi  24451  sinkpi  24486  efopn  24618  logtayl  24620  cxpval  24624  0cxp  24626  cxpexp  24628  cxpcl  24634  cxpge0  24643  mulcxplem  24644  mulcxp  24645  cxpmul2  24649  dvsqrt  24697  dvcnsqrt  24699  cxpcn3  24703  abscxpbnd  24708  efrlim  24910  ftalem2  25014  ftalem3  25015  ftalem4  25016  ftalem5  25017  ftalem7  25019  prmorcht  25118  muinv  25133  1sgm2ppw  25139  logfacbnd3  25162  logexprlim  25164  dchrelbas2  25176  dchrmulid2  25191  dchrfi  25194  dchrinv  25200  lgsdir2  25269  lgsdir  25271  dchrvmasumiflem1  25404  dchrvmasumiflem2  25405  rpvmasum2  25415  log2sumbnd  25447  selberg2lem  25453  logdivbnd  25459  ax5seglem8  26030  axlowdimlem6  26041  axlowdimlem13  26048  ex-co  27626  avril1  27650  vc0  27757  vcz  27758  cnaddabloOLD  27764  cnidOLD  27765  ipasslem8  28020  siilem2  28035  hvmul0  28209  hi01  28281  norm-iii  28325  h1de2ctlem  28742  pjmuli  28876  pjneli  28910  eigre  29022  eigorth  29025  elnlfn  29115  0cnfn  29167  0lnfn  29172  lnopunilem2  29198  xrge0tsmsd  30110  qqh0  30353  qqhcn  30360  eulerpartlemgs2  30767  sgnneg  30927  breprexpnat  31037  hgt750lem2  31055  subfacp1lem6  31490  sinccvglem  31888  abs2sqle  31896  abs2sqlt  31897  tan2h  33714  poimirlem16  33738  poimirlem19  33741  poimirlem31  33753  mblfinlem2  33760  ovoliunnfl  33764  voliunnfl  33766  dvtanlem  33771  ftc1anclem5  33801  cntotbnd  33906  flcidc  38245  dvconstbi  39033  expgrowth  39034  dvradcnv2  39046  binomcxplemdvbinom  39052  binomcxplemnotnn0  39055  xralrple3  40070  negcncfg  40574  ioodvbdlimc1  40628  ioodvbdlimc2  40630  itgsinexplem1  40649  stoweidlem26  40722  stoweidlem36  40732  stoweidlem55  40751  stirlinglem8  40777  fourierdlem103  40905  sqwvfoura  40924  sqwvfourb  40925  ovn0lem  41261  nn0sumshdiglemA  42981  nn0sumshdiglemB  42982  nn0sumshdiglem1  42983  sec0  43072
  Copyright terms: Public domain W3C validator