Theorem zcn 12146

Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
zcn	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Proof of Theorem zcn

Step	Hyp	Ref	Expression
1		zre 12145	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 10826	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2112  ℂcc 10692  ℤcz 12141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-resscn 10751

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194  df-neg 11030  df-z 12142

This theorem is referenced by:  zsscn  12149  zsubcl  12184  zrevaddcl  12187  nzadd  12190  zlem1lt  12194  zltlem1  12195  zdiv  12212  zdivadd  12213  zdivmul  12214  zextlt  12216  zneo  12225  zeo2  12229  peano5uzi  12231  zindd  12243  znnn0nn  12254  zriotaneg  12256  zmax  12506  rebtwnz  12508  qmulz  12512  zq  12515  qaddcl  12526  qnegcl  12527  qmulcl  12528  qreccl  12530  fzen  13094  uzsubsubfz  13099  fz01en  13105  fzmmmeqm  13110  fzsubel  13113  fztp  13133  fzsuc2  13135  fzrev2  13141  fzrev3  13143  elfzp1b  13154  fzrevral  13162  fzrevral2  13163  fzrevral3  13164  fzshftral  13165  fzo0addel  13261  fzo0addelr  13262  fzoaddel2  13263  elfzoext  13264  fzosubel2  13267  eluzgtdifelfzo  13269  fzocatel  13271  elfzom1elp1fzo  13274  fzval3  13276  zpnn0elfzo1  13281  fzosplitprm1  13317  fzoshftral  13324  flzadd  13366  2tnp1ge0ge0  13369  ceilid  13389  quoremz  13393  intfracq  13397  mulmod0  13415  zmod10  13425  modcyc  13444  modcyc2  13445  muladdmodid  13449  mulp1mod1  13450  modmuladdnn0  13453  modmul1  13462  modmulmodr  13475  modaddmulmod  13476  uzrdgxfr  13505  fzen2  13507  seqshft2  13567  sermono  13573  m1expeven  13647  expsub  13648  zesq  13758  modexp  13770  sqoddm1div8  13775  bccmpl  13840  swrd00  14174  addlenrevpfx  14220  swrdswrd  14235  swrdpfx  14237  pfxccatin12lem4  14256  pfxccatin12lem1  14258  swrdccatin2  14259  pfxccatin12lem2  14261  pfxccatin12  14263  repswrevw  14317  cshwsublen  14326  cshwidxmodr  14334  cshwidx0mod  14335  2cshw  14343  2cshwid  14344  2cshwcom  14346  cshweqdif2  14349  cshweqrep  14351  cshw1  14352  2cshwcshw  14355  shftuz  14597  seqshft  14613  nn0abscl  14841  nnabscl  14854  climshftlem  15100  climshft  15102  isershft  15192  mptfzshft  15305  fsumrev  15306  fsum0diag2  15310  efexp  15625  efzval  15626  demoivre  15724  sqrt2irr  15773  dvdsval2  15781  iddvds  15794  1dvds  15795  dvds0  15796  negdvdsb  15797  dvdsnegb  15798  0dvds  15801  dvdsmul1  15802  iddvdsexp  15804  muldvds1  15805  muldvds2  15806  dvdscmul  15807  dvdsmulc  15808  dvdscmulr  15809  dvdsmulcr  15810  summodnegmod  15811  modmulconst  15812  dvds2ln  15813  dvds2add  15814  dvds2sub  15815  dvdstr  15818  dvdssub2  15825  dvdsadd  15826  dvdsaddr  15827  dvdssub  15828  dvdssubr  15829  dvdsadd2b  15830  dvdsaddre2b  15831  dvdsabseq  15837  divconjdvds  15839  alzdvds  15844  addmodlteqALT  15849  dvdsexp2im  15851  odd2np1lem  15864  odd2np1  15865  even2n  15866  oddp1even  15868  mod2eq1n2dvds  15871  mulsucdiv2z  15877  zob  15883  ltoddhalfle  15885  halfleoddlt  15886  opoe  15887  omoe  15888  opeo  15889  omeo  15890  m1exp1  15900  divalglem0  15917  divalglem2  15919  divalglem4  15920  divalglem5  15921  divalglem9  15925  divalgb  15928  divalgmod  15930  modremain  15932  ndvdssub  15933  ndvdsadd  15934  flodddiv4  15937  flodddiv4t2lthalf  15940  bits0  15950  bitsp1e  15954  bitsp1o  15955  gcdneg  16044  gcdaddmlem  16046  gcdaddm  16047  gcdadd  16048  gcdid  16049  modgcd  16055  gcdmultiplez  16058  bezoutlem1  16062  bezoutlem2  16063  bezoutlem4  16065  dvdsgcd  16067  mulgcd  16071  absmulgcd  16072  mulgcdr  16073  gcddiv  16074  gcdmultiplezOLD  16076  dvdssqim  16079  dvdssq  16087  bezoutr1  16089  lcmcllem  16116  lcmneg  16123  lcmgcdlem  16126  lcmgcd  16127  lcmid  16129  lcm1  16130  coprmdvds  16173  coprmdvds2  16174  qredeq  16177  qredeu  16178  divgcdcoprmex  16186  cncongr1  16187  cncongr2  16188  prmdvdsexp  16235  prmdvdssqOLD  16239  rpexp1i  16243  divnumden  16267  zsqrtelqelz  16277  phiprmpw  16292  vfermltlALT  16318  nnnn0modprm0  16322  modprmn0modprm0  16323  coprimeprodsq2  16325  iserodd  16351  pclem  16354  pcprendvds2  16357  pcpremul  16359  pcmul  16367  pcneg  16390  fldivp1  16413  prmpwdvds  16420  zgz  16449  modxai  16584  mod2xnegi  16587  mulgfval  18444  mulgz  18473  mulgassr  18483  mulgmodid  18484  odmod  18892  odf1  18907  odf1o1  18915  gexdvds  18927  zaddablx  19211  cygablOLD  19230  ablfacrp  19407  pgpfac1lem3  19418  ablsimpgfindlem1  19448  zsubrg  20370  zsssubrg  20375  zringmulg  20397  zringinvg  20406  zringunit  20407  zringcyg  20410  prmirred  20415  mulgrhm2  20419  znunit  20482  degltp1le  24925  ef2kpi  25322  efper  25323  sinperlem  25324  sin2kpi  25327  cos2kpi  25328  abssinper  25364  sinkpi  25365  coskpi  25366  eflogeq  25444  cxpexpz  25509  root1eq1  25595  cxpeq  25597  relogbexp  25617  sgmval2  25979  ppiprm  25987  ppinprm  25988  chtprm  25989  chtnprm  25990  lgslem3  26134  lgsneg  26156  lgsdir2lem2  26161  lgsdir2lem4  26163  lgsdir2  26165  lgssq  26172  lgsmulsqcoprm  26178  lgsdirnn0  26179  gausslemma2dlem3  26203  lgsquadlem1  26215  lgsquadlem2  26216  lgsquad2  26221  2lgslem1a2  26225  2lgsoddprmlem1  26243  2lgsoddprmlem2  26244  2sqlem2  26253  2sqlem7  26259  rplogsumlem2  26320  axlowdimlem13  26999  wlk1walk  27680  clwwisshclwwslemlem  28050  ipasslem5  28870  rearchi  31214  znfermltl  31230  knoppndvlem9  34386  poimirlem19  35482  itg2addnclem2  35515  gcdaddmzz2nncomi  39687  metakunt16  39803  dvdsexpim  39977  zexpgcd  39985  zrtelqelz  39994  zrtdvds  39995  dffltz  40115  lzenom  40236  rexzrexnn0  40270  pell1234qrne0  40319  pell1234qrreccl  40320  pell1234qrmulcl  40321  pell1234qrdich  40327  pell14qrdich  40335  reglogexp  40360  reglogexpbas  40363  rmxm1  40400  rmym1  40401  rmxdbl  40405  rmydbl  40406  jm2.24  40429  congtr  40431  congadd  40432  congmul  40433  congsym  40434  congneg  40435  congid  40437  congabseq  40440  acongsym  40442  acongneg2  40443  acongtr  40444  acongrep  40446  jm2.19lem3  40457  jm2.19lem4  40458  jm2.19  40459  jm2.25  40465  jm2.26a  40466  oddfl  42429  coskpi2  43025  cosknegpi  43028  dvdsn1add  43098  itgsinexp  43114  fourierdlem42  43308  fourierdlem97  43362  fourierswlem  43389  2elfz2melfz  44426  sfprmdvdsmersenne  44671  proththd  44682  dfodd6  44705  dfeven4  44706  evenm1odd  44707  evenp1odd  44708  enege  44713  onego  44714  dfeven2  44717  bits0ALTV  44747  opoeALTV  44751  opeoALTV  44752  evensumeven  44775  fppr2odd  44799  sbgoldbwt  44845  nnsum3primesgbe  44860  0nodd  44980  2nodd  44982  1neven  45106  2zlidl  45108  2zrngamgm  45113  2zrngasgrp  45114  2zrngagrp  45117  2zrngmmgm  45120  2zrngmsgrp  45121  2zrngnmrid  45124  zlmodzxzsub  45312  flsubz  45479  mod0mul  45481  m1modmmod  45483  zofldiv2  45493  dignn0flhalflem1  45577  dignn0flhalflem2  45578