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

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

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 10594 . 2 ((i · i) + 1) = 0
2 ax-icn 10585 . . . 4 i ∈ ℂ
3 mulcl 10610 . . . 4 ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
42, 2, 3mp2an 691 . . 3 (i · i) ∈ ℂ
5 ax-1cn 10584 . . 3 1 ∈ ℂ
6 addcl 10608 . . 3 (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
74, 5, 6mp2an 691 . 2 ((i · i) + 1) ∈ ℂ
81, 7eqeltrri 2887 1 0 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2111  (class class class)co 7135  cc 10524  0cc0 10526  1c1 10527  ici 10528   + caddc 10529   · cmul 10531
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-i2m1 10594
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870
This theorem is referenced by:  0cnd  10623  c0ex  10624  1re  10630  00id  10804  mul02lem1  10805  mul02  10807  mul01  10808  addid1  10809  addid2  10812  negcl  10875  subid  10894  subid1  10895  neg0  10921  negid  10922  negsub  10923  subneg  10924  negneg  10925  negeq0  10929  negsubdi  10931  renegcli  10936  mulneg1  11065  msqge0  11150  ixi  11258  muleqadd  11273  div0  11317  ofsubge0  11624  0m0e0  11745  nn0sscn  11890  elznn0  11984  ser0  13418  0exp0e1  13430  0exp  13460  sq0  13551  sqeqor  13574  binom2  13575  bcval5  13674  s1co  14186  shftval3  14427  shftidt2  14432  cjne0  14514  sqrt0  14593  abs0  14637  abs00bd  14643  abs2dif  14684  clim0  14855  climz  14898  serclim0  14926  rlimneg  14995  sumrblem  15060  fsumcvg  15061  summolem2a  15064  sumss  15073  fsumss  15074  fsumcvg2  15076  fsumsplit  15089  sumsplit  15115  fsumrelem  15154  fsumrlim  15158  fsumo1  15159  0fallfac  15383  0risefac  15384  binomfallfac  15387  fsumcube  15406  ef0  15436  eftlub  15454  sin0  15494  tan0  15496  divalglem9  15742  sadadd2lem2  15789  sadadd3  15800  bezout  15881  pcmpt2  16219  4sqlem11  16281  ramcl  16355  4001lem2  16467  odadd1  18961  cnaddablx  18981  cnaddabl  18982  cnaddid  18983  frgpnabllem1  18986  cncrng  20112  cnfld0  20115  cnbl0  23379  cnblcld  23380  cnfldnm  23384  xrge0gsumle  23438  xrge0tsms  23439  cnheibor  23560  cnlmod  23745  csscld  23853  clsocv  23854  cnflduss  23960  cnfldcusp  23961  rrxmvallem  24008  rrxmval  24009  mbfss  24250  mbfmulc2lem  24251  0plef  24276  0pledm  24277  itg1ge0  24290  itg1addlem4  24303  itg2splitlem  24352  itg2addlem  24362  ibl0  24390  iblcnlem  24392  iblss2  24409  itgss3  24418  dvconst  24520  dvcnp2  24523  dvrec  24558  dvexp3  24581  dveflem  24582  dv11cn  24604  lhop1lem  24616  plyun0  24794  plyeq0lem  24807  coeeulem  24821  coeeu  24822  coef3  24829  dgrle  24840  0dgrb  24843  coefv0  24845  coemulc  24852  coe1termlem  24855  coe1term  24856  dgr0  24859  dgrmulc  24868  dgrcolem2  24871  vieta1lem2  24907  iaa  24921  aareccl  24922  aalioulem3  24930  taylthlem2  24969  psercn  25021  pserdvlem2  25023  abelthlem2  25027  abelthlem3  25028  abelthlem5  25030  abelthlem7  25033  abelth  25036  sin2kpi  25076  cos2kpi  25077  sinkpi  25114  efopn  25249  logtayl  25251  cxpval  25255  0cxp  25257  cxpexp  25259  cxpcl  25265  cxpge0  25274  mulcxplem  25275  mulcxp  25276  cxpmul2  25280  dvsqrt  25331  dvcnsqrt  25333  cxpcn3  25337  abscxpbnd  25342  efrlim  25555  ftalem2  25659  ftalem3  25660  ftalem4  25661  ftalem5  25662  ftalem7  25664  prmorcht  25763  muinv  25778  1sgm2ppw  25784  logfacbnd3  25807  logexprlim  25809  dchrelbas2  25821  dchrmulid2  25836  dchrfi  25839  dchrinv  25845  lgsdir2  25914  lgsdir  25916  addsqnreup  26027  dchrvmasumiflem1  26085  dchrvmasumiflem2  26086  rpvmasum2  26096  log2sumbnd  26128  selberg2lem  26134  logdivbnd  26140  ax5seglem8  26730  axlowdimlem6  26741  axlowdimlem13  26748  ex-co  28223  avril1  28248  vc0  28357  vcz  28358  cnaddabloOLD  28364  cnidOLD  28365  ipasslem8  28620  siilem2  28635  hvmul0  28807  hi01  28879  norm-iii  28923  h1de2ctlem  29338  pjmuli  29472  pjneli  29506  eigre  29618  eigorth  29621  elnlfn  29711  0cnfn  29763  0lnfn  29768  lnopunilem2  29794  xrge0tsmsd  30742  qqh0  31335  qqhcn  31342  eulerpartlemgs2  31748  sgnneg  31908  breprexpnat  32015  hgt750lem2  32033  subfacp1lem6  32542  sinccvglem  33025  abs2sqle  33033  abs2sqlt  33034  tan2h  35046  poimirlem16  35070  poimirlem19  35073  poimirlem31  35085  mblfinlem2  35092  ovoliunnfl  35096  voliunnfl  35098  dvtanlem  35103  ftc1anclem5  35131  cntotbnd  35231  60lcm7e420  39295  lcmineqlem10  39323  sn-1ne2  39461  sn-it0e0  39547  addinvcom  39563  sn-0tie0  39571  fltnltalem  39613  flcidc  40113  dvconstbi  41033  expgrowth  41034  dvradcnv2  41046  binomcxplemdvbinom  41052  binomcxplemnotnn0  41055  xralrple3  42001  negcncfg  42518  ioodvbdlimc1  42570  ioodvbdlimc2  42572  itgsinexplem1  42591  stoweidlem26  42663  stoweidlem36  42673  stoweidlem55  42692  stirlinglem8  42718  fourierdlem103  42846  sqwvfoura  42865  sqwvfourb  42866  ovn0lem  43199  nn0sumshdiglemA  45028  nn0sumshdiglemB  45029  nn0sumshdiglem1  45030  sec0  45281
  Copyright terms: Public domain W3C validator