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

Theorem zcn 10971
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 10970 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9695 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   CCcc 9563   ZZcz 10966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-resscn 9622
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-iota 5565  df-fv 5609  df-ov 6318  df-neg 9889  df-z 10967
This theorem is referenced by:  zsscn  10974  zsubcl  11008  zrevaddcl  11011  zlem1lt  11017  zltlem1  11018  zdiv  11035  zdivadd  11036  zdivmul  11037  zextlt  11039  zneo  11047  zeo2  11051  peano5uzi  11053  zindd  11065  znnn0nn  11076  zriotaneg  11078  zmax  11290  rebtwnz  11292  qmulz  11296  zq  11299  qaddcl  11309  qnegcl  11310  qmulcl  11311  qreccl  11313  fzen  11845  uzsubsubfz  11850  fz01en  11856  fzmmmeqm  11861  fzsubel  11863  fztp  11881  fzsuc2  11882  fzrev2  11888  fzrev3  11890  elfzp1b  11900  fzrevral  11908  fzrevral2  11909  fzrevral3  11910  fzshftral  11911  fzo0addel  11999  fzo0addelr  12000  fzoaddel2  12001  elfzoext  12002  fzosubel2  12005  eluzgtdifelfzo  12007  fzocatel  12009  elfzom1elp1fzo  12012  fzval3  12014  zpnn0elfzo1  12018  fzosplitprm1  12049  fzoshftral  12053  flzadd  12091  ceilid  12110  quoremz  12114  intfracq  12118  mulmod0  12136  zmod10  12145  modcyc  12164  modcyc2  12165  muladdmodid  12169  modmul1  12175  modaddmulmod  12188  uzrdgxfr  12212  fzen2  12214  seqshft2  12271  sermono  12277  m1expeven  12351  expsub  12352  zesq  12427  modexp  12439  bccmpl  12526  swrd00  12811  addlenrevswrd  12830  swrdswrd  12853  swrdswrd0  12855  swrdccatin12lem1  12877  swrdccatin12lem2b  12879  swrdccatin2  12880  swrdccatin12lem2  12882  swrdccatin12  12884  repswrevw  12926  cshwsublen  12935  cshwidx0mod  12943  2cshw  12949  2cshwid  12950  2cshwcom  12952  cshweqdif2  12955  cshweqrep  12957  cshw1  12958  2cshwcshw  12961  shftuz  13181  seqshft  13197  nn0abscl  13424  nnabscl  13437  climshftlem  13687  climshft  13689  isershft  13776  mptfzshft  13888  fsumrev  13889  fsum0diag2  13893  efexp  14204  efzval  14205  demoivre  14303  znnenlem  14313  sqrt2irr  14350  dvdsval2  14357  iddvds  14365  1dvds  14366  dvds0  14367  negdvdsb  14368  dvdsnegb  14369  0dvds  14372  dvdsmul1  14373  iddvdsexp  14375  muldvds1  14376  muldvds2  14377  dvdscmul  14378  dvdsmulc  14379  dvdscmulr  14380  dvdsmulcr  14381  dvds2ln  14382  dvds2add  14383  dvds2sub  14384  dvdstr  14386  dvdssub2  14391  dvdsadd  14392  dvdsaddr  14393  dvdssub  14394  dvdssubr  14395  dvdsadd2b  14396  alzdvds  14404  mulmoddvds  14412  odd2np1lem  14413  odd2np1  14414  oddp1even  14416  fproddvdsd  14419  divalglem0  14420  divalglem2  14422  divalglem2OLD  14423  divalglem4  14424  divalglem5OLD  14425  divalglem5  14426  divalglem9  14430  divalglem9OLD  14431  divalgb  14434  divalgmod  14436  ndvdssub  14437  ndvdsadd  14438  bits0  14450  bitsp1e  14454  bitsp1o  14455  gcdneg  14539  gcdaddmlem  14541  gcdaddm  14542  gcdadd  14543  gcdid  14544  modgcd  14549  bezoutlem1  14552  bezoutlem2OLD  14553  bezoutlem4OLD  14555  bezoutlem2  14556  bezoutlem4  14558  dvdsgcd  14560  mulgcd  14563  absmulgcd  14564  mulgcdr  14565  gcddiv  14566  gcdmultiplez  14568  dvdssqim  14570  dvdssq  14577  lcmcllem  14610  lcmneg  14617  lcmgcdlem  14620  lcmgcd  14621  lcmid  14623  lcm1  14624  coprmdvds  14708  coprmdvds2  14709  qredeq  14712  qredeu  14713  prmdvdsexp  14716  rpexp1i  14722  divnumden  14746  zsqrtelqelz  14756  phiprmpw  14773  vfermltlALT  14802  nnnn0modprm0  14806  modprmn0modprm0  14807  coprimeprodsq2  14809  opoe  14810  omoe  14811  opeo  14812  omeo  14813  iserodd  14834  pclem  14837  pcprendvds2  14840  pcpremul  14842  pcmul  14850  pcneg  14872  fldivp1  14891  prmpwdvds  14897  zgz  14926  modxai  15089  mod2xnegi  15092  mulgz  16828  odmod  17244  odf1  17262  odf1o1  17270  gexdvds  17284  zaddablx  17557  cygabl  17574  ablfacrp  17748  pgpfac1lem3  17759  zsubrg  19070  zsssubrg  19075  zringmulg  19096  zringcyg  19109  zringinvg  19110  zringunit  19111  prmirred  19115  mulgrhm2  19119  znunit  19183  degltp1le  23071  ef2kpi  23482  efper  23483  sinperlem  23484  sin2kpi  23487  cos2kpi  23488  abssinper  23522  sinkpi  23523  coskpi  23524  eflogeq  23600  cxpexpz  23661  root1eq1  23744  cxpeq  23746  relogbexp  23766  leibpilem1  23915  sgmval2  24119  ppiprm  24127  ppinprm  24128  chtprm  24129  chtnprm  24130  lgslem3  24275  lgsneg  24296  lgsdir2lem2  24301  lgsdir2lem4  24303  lgsdir2  24305  lgsdirnn0  24316  lgsquadlem1  24331  lgsquadlem2  24332  lgsquad2  24337  2sqlem2  24341  2sqlem7  24347  rplogsumlem2  24372  axlowdimlem13  25033  wlkdvspthlem  25386  clwwisshclwwlem1  25582  gxneg  26043  gxsuc  26049  gxnn0add  26051  gxadd  26052  gxsub  26053  gxnn0mul  26054  gxmul  26055  zaddsubgo  26131  ipasslem5  26525  rearchi  28654  pdivsq  30434  dvdspw  30435  poimirlem19  32004  itg2addnclem2  32039  lzenom  35657  rexzrexnn0  35692  pell1234qrne0  35744  pell1234qrreccl  35745  pell1234qrmulcl  35746  pell1234qrdich  35752  pell14qrdich  35760  reglogexp  35787  reglogexpbas  35790  rmxm1  35827  rmym1  35828  rmxdbl  35832  rmydbl  35833  jm2.24  35858  congtr  35860  congadd  35861  congmul  35862  congsym  35863  congneg  35864  congid  35866  congabseq  35869  acongsym  35871  acongneg2  35872  acongtr  35873  acongrep  35875  bezoutr1  35881  dvdsabsmod0OLD  35886  jm2.19lem3  35891  jm2.19lem4  35892  jm2.19  35893  jm2.25  35899  jm2.26a  35900  oddfl  37525  coskpi2  37779  cosknegpi  37782  dvdsn1add  37852  itgsinexp  37869  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem97  38105  fourierswlem  38132  mod2eq1n2dvds  38763  elmod2OLD  38764  zob  38801  dfodd6  38805  dfeven4  38806  evenm1odd  38807  evenp1odd  38808  enege  38813  onego  38814  dfeven2  38817  bits0ALTV  38846  opoeALTV  38850  opeoALTV  38851  evensumeven  38872  bgoldbwt  38916  nnsum3primesgbe  38925  proththd  38952  addlenrevpfx  38978  pfxccatin12lem1  39004  pfxccatin12lem2  39005  pfxccatin12  39006  2elfz2melfz  39100  1wlk1walk  39697  0nodd  40083  2nodd  40085  1neven  40205  2zlidl  40207  2zrngamgm  40212  2zrngasgrp  40213  2zrngagrp  40216  2zrngmmgm  40219  2zrngmsgrp  40220  2zrngnmrid  40223  zlmodzxzsub  40414  flsubz  40593  mod0mul  40595  m1modmmod  40597  zofldiv2  40611  dignn0flhalflem1  40699  dignn0flhalflem2  40700
  Copyright terms: Public domain W3C validator