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

Theorem zcn 11379
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
zcn (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Proof of Theorem zcn
StepHypRef Expression
1 zre 11378 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 10065 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  cc 9931  cz 11374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-resscn 9990
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-iota 5849  df-fv 5894  df-ov 6650  df-neg 10266  df-z 11375
This theorem is referenced by:  zsscn  11382  zsubcl  11416  zrevaddcl  11419  nzadd  11422  zlem1lt  11426  zltlem1  11427  zdiv  11444  zdivadd  11445  zdivmul  11446  zextlt  11448  zneo  11457  zeo2  11461  peano5uzi  11463  zindd  11475  znnn0nn  11486  zriotaneg  11488  zmax  11782  rebtwnz  11784  qmulz  11788  zq  11791  qaddcl  11801  qnegcl  11802  qmulcl  11803  qreccl  11805  fzen  12355  uzsubsubfz  12360  fz01en  12366  fzmmmeqm  12371  fzsubel  12374  fztp  12394  fzsuc2  12395  fzrev2  12401  fzrev3  12403  elfzp1b  12413  fzrevral  12421  fzrevral2  12422  fzrevral3  12423  fzshftral  12424  fzo0addel  12517  fzo0addelr  12518  fzoaddel2  12519  elfzoext  12520  fzosubel2  12523  eluzgtdifelfzo  12525  fzocatel  12527  elfzom1elp1fzo  12530  fzval3  12532  zpnn0elfzo1  12537  fzosplitprm1  12573  fzoshftral  12580  flzadd  12622  2tnp1ge0ge0  12625  ceilid  12645  quoremz  12649  intfracq  12653  mulmod0  12671  zmod10  12681  modcyc  12700  modcyc2  12701  muladdmodid  12705  mulp1mod1  12706  modmuladdnn0  12709  modmul1  12718  modmulmodr  12731  modaddmulmod  12732  uzrdgxfr  12761  fzen2  12763  seqshft2  12822  sermono  12828  m1expeven  12902  expsub  12903  zesq  12982  modexp  12994  sqoddm1div8  13023  bccmpl  13091  swrd00  13412  addlenrevswrd  13431  swrdswrd  13454  swrdswrd0  13456  swrdccatin12lem1  13478  swrdccatin12lem2b  13480  swrdccatin2  13481  swrdccatin12lem2  13483  swrdccatin12  13485  repswrevw  13527  cshwsublen  13536  cshwidxmodr  13544  cshwidx0mod  13545  2cshw  13553  2cshwid  13554  2cshwcom  13556  cshweqdif2  13559  cshweqrep  13561  cshw1  13562  2cshwcshw  13565  shftuz  13803  seqshft  13819  nn0abscl  14046  nnabscl  14059  climshftlem  14299  climshft  14301  isershft  14388  mptfzshft  14504  fsumrev  14505  fsum0diag2  14509  efexp  14825  efzval  14826  demoivre  14924  znnenlem  14934  sqrt2irr  14973  dvdsval2  14980  iddvds  14989  1dvds  14990  dvds0  14991  negdvdsb  14992  dvdsnegb  14993  0dvds  14996  dvdsmul1  14997  iddvdsexp  14999  muldvds1  15000  muldvds2  15001  dvdscmul  15002  dvdsmulc  15003  dvdscmulr  15004  dvdsmulcr  15005  summodnegmod  15006  modmulconst  15007  dvds2ln  15008  dvds2add  15009  dvds2sub  15010  dvdstr  15012  dvdssub2  15017  dvdsadd  15018  dvdsaddr  15019  dvdssub  15020  dvdssubr  15021  dvdsadd2b  15022  dvdsaddre2b  15023  dvdsabseq  15029  divconjdvds  15031  alzdvds  15036  addmodlteqALT  15041  mulmoddvds  15045  odd2np1lem  15058  odd2np1  15059  even2n  15060  oddp1even  15062  mod2eq1n2dvds  15065  mulsucdiv2z  15071  zob  15077  ltoddhalfle  15079  halfleoddlt  15080  opoe  15081  omoe  15082  opeo  15083  omeo  15084  m1exp1  15087  divalglem0  15110  divalglem2  15112  divalglem4  15113  divalglem5  15114  divalglem9  15118  divalgb  15121  divalgmod  15123  divalgmodOLD  15124  modremain  15126  ndvdssub  15127  ndvdsadd  15128  flodddiv4  15131  flodddiv4t2lthalf  15134  bits0  15144  bitsp1e  15148  bitsp1o  15149  gcdneg  15237  gcdaddmlem  15239  gcdaddm  15240  gcdadd  15241  gcdid  15242  modgcd  15247  bezoutlem1  15250  bezoutlem2  15251  bezoutlem4  15253  dvdsgcd  15255  mulgcd  15259  absmulgcd  15260  mulgcdr  15261  gcddiv  15262  gcdmultiplez  15264  dvdssqim  15267  dvdssq  15274  bezoutr1  15276  lcmcllem  15303  lcmneg  15310  lcmgcdlem  15313  lcmgcd  15314  lcmid  15316  lcm1  15317  coprmdvds  15360  coprmdvdsOLD  15361  coprmdvds2  15362  qredeq  15365  qredeu  15366  divgcdcoprmex  15374  cncongr1  15375  cncongr2  15376  prmdvdsexp  15421  rpexp1i  15427  divnumden  15450  zsqrtelqelz  15460  phiprmpw  15475  vfermltlALT  15501  nnnn0modprm0  15505  modprmn0modprm0  15506  coprimeprodsq2  15508  iserodd  15534  pclem  15537  pcprendvds2  15540  pcpremul  15542  pcmul  15550  pcneg  15572  fldivp1  15595  prmpwdvds  15602  zgz  15631  modxai  15766  mod2xnegi  15769  mulgz  17562  mulgassr  17574  mulgmodid  17575  odmod  17959  odf1  17973  odf1o1  17981  gexdvds  17993  zaddablx  18269  cygabl  18286  ablfacrp  18459  pgpfac1lem3  18470  zsubrg  19793  zsssubrg  19798  zringmulg  19820  zringinvg  19829  zringunit  19830  zringcyg  19833  prmirred  19837  mulgrhm2  19841  znunit  19906  degltp1le  23827  ef2kpi  24224  efper  24225  sinperlem  24226  sin2kpi  24229  cos2kpi  24230  abssinper  24264  sinkpi  24265  coskpi  24266  eflogeq  24342  cxpexpz  24407  root1eq1  24490  cxpeq  24492  relogbexp  24512  leibpilem1  24661  sgmval2  24863  ppiprm  24871  ppinprm  24872  chtprm  24873  chtnprm  24874  lgslem3  25018  lgsneg  25040  lgsdir2lem2  25045  lgsdir2lem4  25047  lgsdir2  25049  lgssq  25056  lgsmulsqcoprm  25062  lgsdirnn0  25063  gausslemma2dlem3  25087  lgsquadlem1  25099  lgsquadlem2  25100  lgsquad2  25105  2lgslem1a2  25109  2lgsoddprmlem1  25127  2lgsoddprmlem2  25128  2sqlem2  25137  2sqlem7  25143  rplogsumlem2  25168  axlowdimlem13  25828  wlk1walk  26529  clwwisshclwwslemlem  26919  ipasslem5  27674  rearchi  29827  pdivsq  31621  dvdspw  31622  knoppndvlem9  32495  poimirlem19  33408  itg2addnclem2  33442  lzenom  37159  rexzrexnn0  37194  pell1234qrne0  37243  pell1234qrreccl  37244  pell1234qrmulcl  37245  pell1234qrdich  37251  pell14qrdich  37259  reglogexp  37284  reglogexpbas  37287  rmxm1  37325  rmym1  37326  rmxdbl  37330  rmydbl  37331  jm2.24  37356  congtr  37358  congadd  37359  congmul  37360  congsym  37361  congneg  37362  congid  37364  congabseq  37367  acongsym  37369  acongneg2  37370  acongtr  37371  acongrep  37373  jm2.19lem3  37384  jm2.19lem4  37385  jm2.19  37386  jm2.25  37392  jm2.26a  37393  oddfl  39308  coskpi2  39846  cosknegpi  39849  dvdsn1add  39923  itgsinexp  39939  fourierdlem42  40135  fourierdlem97  40189  fourierswlem  40216  2elfz2melfz  41097  addlenrevpfx  41168  pfxccatin12lem1  41194  pfxccatin12lem2  41195  pfxccatin12  41196  sfprmdvdsmersenne  41291  proththd  41302  dfodd6  41321  dfeven4  41322  evenm1odd  41323  evenp1odd  41324  enege  41329  onego  41330  dfeven2  41333  bits0ALTV  41361  opoeALTV  41365  opeoALTV  41366  evensumeven  41387  sbgoldbwt  41436  nnsum3primesgbe  41451  0nodd  41581  2nodd  41583  1neven  41703  2zlidl  41705  2zrngamgm  41710  2zrngasgrp  41711  2zrngagrp  41714  2zrngmmgm  41717  2zrngmsgrp  41718  2zrngnmrid  41721  zlmodzxzsub  41909  flsubz  42083  mod0mul  42085  m1modmmod  42087  zofldiv2  42096  dignn0flhalflem1  42180  dignn0flhalflem2  42181
  Copyright terms: Public domain W3C validator