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

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

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 9883 . 2 ((i · i) + 1) = 0
2 ax-icn 9874 . . . 4 i ∈ ℂ
3 mulcl 9899 . . . 4 ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
42, 2, 3mp2an 704 . . 3 (i · i) ∈ ℂ
5 ax-1cn 9873 . . 3 1 ∈ ℂ
6 addcl 9897 . . 3 (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
74, 5, 6mp2an 704 . 2 ((i · i) + 1) ∈ ℂ
81, 7eqeltrri 2685 1 0 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  (class class class)co 6549  cc 9813  0cc0 9815  1c1 9816  ici 9817   + caddc 9818   · cmul 9820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-i2m1 9883
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606
This theorem is referenced by:  0cnd  9912  c0ex  9913  1re  9918  00id  10090  mul02lem1  10091  mul02  10093  mul01  10094  addid1  10095  addid2  10098  negcl  10160  subid  10179  subid1  10180  neg0  10206  negid  10207  negsub  10208  subneg  10209  negneg  10210  negeq0  10214  negsubdi  10216  renegcli  10221  mulneg1  10345  msqge0  10428  ixi  10535  muleqadd  10550  div0  10594  ofsubge0  10896  0m0e0  11007  elznn0  11269  ser0  12715  0exp0e1  12727  0exp  12757  sq0  12817  sqeqor  12840  binom2  12841  bcval5  12967  s1co  13430  shftval3  13664  shftidt2  13669  cjne0  13751  sqrt0  13830  abs0  13873  abs00bd  13879  abs2dif  13920  clim0  14085  climz  14128  serclim0  14156  rlimneg  14225  sumrblem  14289  fsumcvg  14290  summolem2a  14293  sumss  14302  fsumss  14303  fsumcvg2  14305  fsumsplit  14318  sumsplit  14341  fsumrelem  14380  fsumrlim  14384  fsumo1  14385  0fallfac  14607  0risefac  14608  binomfallfac  14611  fsumcube  14630  ef0  14660  eftlub  14678  sin0  14718  tan0  14720  divalglem9  14962  sadadd2lem2  15010  sadadd3  15021  bezout  15098  pcmpt2  15435  4sqlem11  15497  ramcl  15571  4001lem2  15687  odadd1  18074  cnaddablx  18094  cnaddabl  18095  cnaddid  18096  frgpnabllem1  18099  cncrng  19586  cnfld0  19589  cnbl0  22387  cnblcld  22388  cnfldnm  22392  xrge0gsumle  22444  xrge0tsms  22445  cnheibor  22562  cnlmod  22748  csscld  22856  clsocv  22857  cnflduss  22960  cnfldcusp  22961  rrxmvallem  22995  rrxmval  22996  mbfss  23219  mbfmulc2lem  23220  0plef  23245  0pledm  23246  itg1ge0  23259  itg1addlem4  23272  itg2splitlem  23321  itg2addlem  23331  ibl0  23359  iblcnlem  23361  iblss2  23378  itgss3  23387  dvconst  23486  dvcnp2  23489  dvrec  23524  dvexp3  23545  dveflem  23546  dvef  23547  dv11cn  23568  lhop1lem  23580  plyun0  23757  plyeq0lem  23770  coeeulem  23784  coeeu  23785  coef3  23792  dgrle  23803  0dgrb  23806  coefv0  23808  coemulc  23815  coe1termlem  23818  coe1term  23819  dgr0  23822  dgrmulc  23831  dgrcolem2  23834  vieta1lem2  23870  iaa  23884  aareccl  23885  aalioulem3  23893  taylthlem2  23932  psercn  23984  pserdvlem2  23986  abelthlem2  23990  abelthlem3  23991  abelthlem5  23993  abelthlem7  23996  abelth  23999  sin2kpi  24039  cos2kpi  24040  sinkpi  24075  efopn  24204  logtayl  24206  cxpval  24210  0cxp  24212  cxpexp  24214  cxpcl  24220  cxpge0  24229  mulcxplem  24230  mulcxp  24231  cxpmul2  24235  dvsqrt  24283  dvcnsqrt  24285  cxpcn3  24289  abscxpbnd  24294  efrlim  24496  ftalem2  24600  ftalem3  24601  ftalem4  24602  ftalem5  24603  ftalem7  24605  prmorcht  24704  muinv  24719  1sgm2ppw  24725  logfacbnd3  24748  logexprlim  24750  dchrelbas2  24762  dchrmulid2  24777  dchrfi  24780  dchrinv  24786  lgsdir2  24855  lgsdir  24857  dchrvmasumiflem1  24990  dchrvmasumiflem2  24991  rpvmasum2  25001  log2sumbnd  25033  selberg2lem  25039  logdivbnd  25045  ax5seglem8  25616  axlowdimlem6  25627  axlowdimlem13  25634  ex-co  26687  avril1  26711  vc0  26813  vcz  26814  cnaddabloOLD  26820  cnidOLD  26821  ipasslem8  27076  siilem2  27091  hvmul0  27265  hi01  27337  norm-iii  27381  h1de2ctlem  27798  pjmuli  27932  pjneli  27966  eigre  28078  eigorth  28081  elnlfn  28171  0cnfn  28223  0lnfn  28228  lnopunilem2  28254  xrge0tsmsd  29116  qqh0  29356  qqhcn  29363  eulerpartlemgs2  29769  sgnneg  29929  subfacp1lem6  30421  sinccvglem  30820  abs2sqle  30828  abs2sqlt  30829  tan2h  32571  poimirlem16  32595  poimirlem19  32598  poimirlem31  32610  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  dvtanlem  32629  ftc1anclem5  32659  cntotbnd  32765  flcidc  36763  dvconstbi  37555  expgrowth  37556  dvradcnv2  37568  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  xralrple3  38531  negcncfg  38766  ioodvbdlimc1  38823  ioodvbdlimc2  38825  itgsinexplem1  38845  stoweidlem26  38919  stoweidlem36  38929  stoweidlem55  38948  stirlinglem8  38974  fourierdlem103  39102  sqwvfoura  39121  sqwvfourb  39122  ovn0lem  39455  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213  sec0  42300
  Copyright terms: Public domain W3C validator