MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zcn Structured version   Unicode version

Theorem zcn 10870
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
zcn  |-  ( N  e.  ZZ  ->  N  e.  CC )

Proof of Theorem zcn
StepHypRef Expression
1 zre 10869 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9620 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   CCcc 9488   ZZcz 10865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-resscn 9547
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-ov 6280  df-neg 9808  df-z 10866
This theorem is referenced by:  zsscn  10873  zsubcl  10907  zrevaddcl  10910  zlem1lt  10916  zltlem1  10917  zdiv  10934  zdivadd  10935  zdivmul  10936  zextlt  10938  zneo  10946  zeo2  10950  peano5uzi  10952  uzindOLD  10958  zindd  10965  zriotaneg  10977  zmax  11183  rebtwnz  11185  qmulz  11189  zq  11192  qaddcl  11202  qnegcl  11203  qmulcl  11204  qreccl  11206  fzen  11707  uzsubsubfz  11711  fz01en  11717  fzmmmeqm  11721  fzsubel  11723  fztp  11740  fzsuc2  11741  fzrev2  11747  fzrev3  11749  elfzp1b  11759  fzrevral  11766  fzrevral2  11767  fzrevral3  11768  fzshftral  11769  fzoaddel2  11848  fzosubel2  11850  eluzgtdifelfzo  11852  fzocatel  11854  elfzom1elp1fzo  11857  fzval3  11859  zpnn0elfzo1  11863  fzosplitprm1  11893  fzoshftral  11897  flzadd  11933  ceilid  11952  quoremz  11956  intfracq  11960  zmod10  11986  modcyc  12005  modcyc2  12006  modmul1  12014  modaddmulmod  12027  uzrdgxfr  12051  fzen2  12053  seqshft2  12107  sermono  12113  expsub  12187  zesq  12263  modexp  12275  bccmpl  12361  swrd00  12619  addlenrevswrd  12635  swrdswrd  12659  swrdswrd0  12661  swrdccatin12lem1  12683  swrdccatin12lem2b  12685  swrdccatin2  12686  swrdccatin12lem2  12688  swrdccatin12  12690  repswrevw  12732  cshwsublen  12741  cshwidx0mod  12749  2cshw  12755  2cshwid  12756  2cshwcom  12758  cshweqdif2  12761  cshweqrep  12763  cshw1  12764  2cshwcshw  12767  shftuz  12876  seqshft  12892  nn0abscl  13119  nnabscl  13132  climshftlem  13371  climshft  13373  isershft  13460  mptfzshft  13567  fsumrev  13568  fsum0diag2  13572  efexp  13708  efzval  13709  demoivre  13807  znnenlem  13817  sqrt2irr  13854  dvdsval2  13861  iddvds  13869  1dvds  13870  dvds0  13871  negdvdsb  13872  dvdsnegb  13873  0dvds  13876  dvdsmul1  13877  iddvdsexp  13879  muldvds1  13880  muldvds2  13881  dvdscmul  13882  dvdsmulc  13883  dvdscmulr  13884  dvdsmulcr  13885  dvds2ln  13886  dvds2add  13887  dvds2sub  13888  dvdstr  13890  dvdssub2  13895  dvdsadd  13896  dvdsaddr  13897  dvdssub  13898  dvdssubr  13899  dvdsadd2b  13900  alzdvds  13908  mulmoddvds  13916  odd2np1lem  13917  odd2np1  13918  oddp1even  13920  divalglem0  13923  divalglem2  13925  divalglem4  13926  divalglem5  13927  divalglem9  13931  divalgb  13934  divalgmod  13936  ndvdssub  13937  ndvdsadd  13938  bits0  13950  bitsp1e  13954  bitsp1o  13955  gcdneg  14036  gcdaddmlem  14038  gcdaddm  14039  gcdadd  14040  gcdid  14041  modgcd  14046  bezoutlem1  14048  bezoutlem2  14049  bezoutlem4  14051  dvdsgcd  14053  mulgcd  14056  absmulgcd  14057  mulgcdr  14058  gcddiv  14059  gcdmultiplez  14061  dvdssqim  14063  dvdssq  14070  coprmdvds  14115  coprmdvds2  14116  qredeq  14119  qredeu  14120  prmdvdsexp  14127  rpexp1i  14134  divnumden  14153  zsqrtelqelz  14163  phiprmpw  14178  nnnn0modprm0  14203  modprmn0modprm0  14204  coprimeprodsq2  14206  opoe  14207  omoe  14208  opeo  14209  omeo  14210  iserodd  14231  pclem  14234  pcprendvds2  14237  pcpremul  14239  pcmul  14247  pcneg  14269  fldivp1  14288  prmpwdvds  14294  zgz  14323  modxai  14426  mod2xnegi  14429  mulgz  16032  odmod  16439  odf1  16453  odf1o1  16461  gexdvds  16473  zaddablx  16745  cygabl  16762  ablfacrp  16985  pgpfac1lem3  16996  zsubrg  18339  zsssubrg  18344  zringmulg  18364  zrngmulg  18370  zringcyg  18380  zcyg  18385  zringinvg  18386  zringunit  18387  zrngunit  18388  prmirred  18392  prmirredOLD  18395  mulgrhm2  18400  mulgrhm2OLD  18403  znunit  18469  degltp1le  22339  ef2kpi  22736  efper  22737  sinperlem  22738  sin2kpi  22741  cos2kpi  22742  abssinper  22776  sinkpi  22777  coskpi  22778  eflogeq  22851  cxpexpz  22913  root1eq1  22994  cxpeq  22996  leibpilem1  23136  sgmval2  23282  ppiprm  23290  ppinprm  23291  chtprm  23292  chtnprm  23293  lgslem3  23438  lgsneg  23459  lgsdir2lem2  23464  lgsdir2lem4  23466  lgsdir2  23468  lgsdirnn0  23479  lgsquadlem1  23494  lgsquadlem2  23495  lgsquad2  23500  2sqlem2  23504  2sqlem7  23510  rplogsumlem2  23535  axlowdimlem13  24122  wlkdvspthlem  24474  clwwisshclwwlem1  24670  gxneg  25133  gxsuc  25139  gxnn0add  25141  gxadd  25142  gxsub  25143  gxnn0mul  25144  gxmul  25145  zaddsubgo  25221  ipasslem5  25615  rearchi  27698  m1expevenALT  28529  pdivsq  29142  dvdspw  29143  itg2addnclem2  30035  lzenom  30671  rexzrexnn0  30705  pell1234qrne0  30757  pell1234qrreccl  30758  pell1234qrmulcl  30759  pell1234qrdich  30765  pell14qrdich  30773  reglogexp  30798  reglogexpbas  30801  rmxm1  30838  rmym1  30839  rmxdbl  30843  rmydbl  30844  jm2.24  30869  congtr  30871  congadd  30872  congmul  30873  congsym  30874  congneg  30875  congid  30877  congabseq  30880  acongsym  30882  acongneg2  30883  acongtr  30884  acongrep  30886  bezoutr1  30892  dvdsabsmod0  30896  jm2.19lem3  30901  jm2.19lem4  30902  jm2.19  30903  jm2.25  30909  jm2.26a  30910  lcmcllem  31171  lcmneg  31178  lcmgcdlem  31181  lcmgcd  31182  lcmid  31184  oddfl  31404  znnn0nn  31434  coskpi2  31569  cosknegpi  31572  itgsinexp  31639  fourierdlem42  31816  fourierdlem97  31871  fourierswlem  31898  2elfz2melfz  32168  0nodd  32331  2nodd  32333  1neven  32438  2zlidl  32440  2zrngamgm  32445  2zrngasgrp  32446  2zrngagrp  32449  2zrngmmgm  32452  2zrngmsgrp  32453  2zrngnmrid  32456  zlmodzxzsub  32657
  Copyright terms: Public domain W3C validator