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

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

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 10593 . 2 ((i · i) + 1) = 0
2 ax-icn 10584 . . . 4 i ∈ ℂ
3 mulcl 10609 . . . 4 ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
42, 2, 3mp2an 688 . . 3 (i · i) ∈ ℂ
5 ax-1cn 10583 . . 3 1 ∈ ℂ
6 addcl 10607 . . 3 (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
74, 5, 6mp2an 688 . 2 ((i · i) + 1) ∈ ℂ
81, 7eqeltrri 2907 1 0 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  (class class class)co 7145  cc 10523  0cc0 10525  1c1 10526  ici 10527   + caddc 10528   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-i2m1 10593
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890
This theorem is referenced by:  0cnd  10622  c0ex  10623  1re  10629  00id  10803  mul02lem1  10804  mul02  10806  mul01  10807  addid1  10808  addid2  10811  negcl  10874  subid  10893  subid1  10894  neg0  10920  negid  10921  negsub  10922  subneg  10923  negneg  10924  negeq0  10928  negsubdi  10930  renegcli  10935  mulneg1  11064  msqge0  11149  ixi  11257  muleqadd  11272  div0  11316  ofsubge0  11625  0m0e0  11745  nn0sscn  11890  elznn0  11984  ser0  13410  0exp0e1  13422  0exp  13452  sq0  13543  sqeqor  13566  binom2  13567  bcval5  13666  s1co  14183  shftval3  14423  shftidt2  14428  cjne0  14510  sqrt0  14589  abs0  14633  abs00bd  14639  abs2dif  14680  clim0  14851  climz  14894  serclim0  14922  rlimneg  14991  sumrblem  15056  fsumcvg  15057  summolem2a  15060  sumss  15069  fsumss  15070  fsumcvg2  15072  fsumsplit  15085  sumsplit  15111  fsumrelem  15150  fsumrlim  15154  fsumo1  15155  0fallfac  15379  0risefac  15380  binomfallfac  15383  fsumcube  15402  ef0  15432  eftlub  15450  sin0  15490  tan0  15492  divalglem9  15740  sadadd2lem2  15787  sadadd3  15798  bezout  15879  pcmpt2  16217  4sqlem11  16279  ramcl  16353  4001lem2  16463  odadd1  18897  cnaddablx  18917  cnaddabl  18918  cnaddid  18919  frgpnabllem1  18922  cncrng  20494  cnfld0  20497  cnbl0  23309  cnblcld  23310  cnfldnm  23314  xrge0gsumle  23368  xrge0tsms  23369  cnheibor  23486  cnlmod  23671  csscld  23779  clsocv  23780  cnflduss  23886  cnfldcusp  23887  rrxmvallem  23934  rrxmval  23935  mbfss  24174  mbfmulc2lem  24175  0plef  24200  0pledm  24201  itg1ge0  24214  itg1addlem4  24227  itg2splitlem  24276  itg2addlem  24286  ibl0  24314  iblcnlem  24316  iblss2  24333  itgss3  24342  dvconst  24441  dvcnp2  24444  dvrec  24479  dvexp3  24502  dveflem  24503  dv11cn  24525  lhop1lem  24537  plyun0  24714  plyeq0lem  24727  coeeulem  24741  coeeu  24742  coef3  24749  dgrle  24760  0dgrb  24763  coefv0  24765  coemulc  24772  coe1termlem  24775  coe1term  24776  dgr0  24779  dgrmulc  24788  dgrcolem2  24791  vieta1lem2  24827  iaa  24841  aareccl  24842  aalioulem3  24850  taylthlem2  24889  psercn  24941  pserdvlem2  24943  abelthlem2  24947  abelthlem3  24948  abelthlem5  24950  abelthlem7  24953  abelth  24956  sin2kpi  24996  cos2kpi  24997  sinkpi  25034  efopn  25168  logtayl  25170  cxpval  25174  0cxp  25176  cxpexp  25178  cxpcl  25184  cxpge0  25193  mulcxplem  25194  mulcxp  25195  cxpmul2  25199  dvsqrt  25250  dvcnsqrt  25252  cxpcn3  25256  abscxpbnd  25261  efrlim  25474  ftalem2  25578  ftalem3  25579  ftalem4  25580  ftalem5  25581  ftalem7  25583  prmorcht  25682  muinv  25697  1sgm2ppw  25703  logfacbnd3  25726  logexprlim  25728  dchrelbas2  25740  dchrmulid2  25755  dchrfi  25758  dchrinv  25764  lgsdir2  25833  lgsdir  25835  addsqnreup  25946  dchrvmasumiflem1  26004  dchrvmasumiflem2  26005  rpvmasum2  26015  log2sumbnd  26047  selberg2lem  26053  logdivbnd  26059  ax5seglem8  26649  axlowdimlem6  26660  axlowdimlem13  26667  ex-co  28144  avril1  28169  vc0  28278  vcz  28279  cnaddabloOLD  28285  cnidOLD  28286  ipasslem8  28541  siilem2  28556  hvmul0  28728  hi01  28800  norm-iii  28844  h1de2ctlem  29259  pjmuli  29393  pjneli  29427  eigre  29539  eigorth  29542  elnlfn  29632  0cnfn  29684  0lnfn  29689  lnopunilem2  29715  xrge0tsmsd  30619  qqh0  31124  qqhcn  31131  eulerpartlemgs2  31537  sgnneg  31697  breprexpnat  31804  hgt750lem2  31822  subfacp1lem6  32329  sinccvglem  32812  abs2sqle  32820  abs2sqlt  32821  tan2h  34765  poimirlem16  34789  poimirlem19  34792  poimirlem31  34804  mblfinlem2  34811  ovoliunnfl  34815  voliunnfl  34817  dvtanlem  34822  ftc1anclem5  34852  cntotbnd  34955  sn-1ne2  39036  fltnltalem  39152  flcidc  39652  dvconstbi  40543  expgrowth  40544  dvradcnv2  40556  binomcxplemdvbinom  40562  binomcxplemnotnn0  40565  xralrple3  41518  negcncfg  42040  ioodvbdlimc1  42094  ioodvbdlimc2  42096  itgsinexplem1  42115  stoweidlem26  42188  stoweidlem36  42198  stoweidlem55  42217  stirlinglem8  42243  fourierdlem103  42371  sqwvfoura  42390  sqwvfourb  42391  ovn0lem  42724  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608  nn0sumshdiglem1  44609  sec0  44787
  Copyright terms: Public domain W3C validator