Theorem zcn 9377

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 9376	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 8101	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2176  ℂcc 7923  ℤcz 9372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8017

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-rab 2493  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947  df-neg 8246  df-z 9373

This theorem is referenced by:  zsscn  9380  zaddcllempos  9409  peano2zm  9410  zaddcllemneg  9411  zaddcl  9412  zsubcl  9413  zrevaddcl  9423  nzadd  9425  zlem1lt  9429  zltlem1  9430  zapne  9447  zdiv  9461  zdivadd  9462  zdivmul  9463  zextlt  9465  zneo  9474  zeo2  9479  peano5uzti  9481  zindd  9491  divfnzn  9742  qmulz  9744  zq  9747  qaddcl  9756  qnegcl  9757  qmulcl  9758  qreccl  9763  fzen  10165  uzsubsubfz  10169  fz01en  10175  fzmmmeqm  10180  fzsubel  10182  fztp  10200  fzsuc2  10201  fzrev2  10207  fzrev3  10209  elfzp1b  10219  fzrevral  10227  fzrevral2  10228  fzrevral3  10229  fzshftral  10230  fzo0addel  10317  fzo0addelr  10318  fzoaddel2  10319  fzosubel2  10324  eluzgtdifelfzo  10326  fzocatel  10328  elfzom1elp1fzo  10331  fzval3  10333  zpnn0elfzo1  10337  fzosplitprm1  10363  fzoshftral  10367  flqzadd  10441  2tnp1ge0ge0  10444  ceilid  10460  intfracq  10465  zmod10  10485  modqmuladdnn0  10513  addmodlteq  10543  frecfzen2  10572  seqshft2g  10627  ser3mono  10632  m1expeven  10731  expsubap  10732  zesq  10803  sqoddm1div8  10838  bccmpl  10899  swrd00g  11102  shftuz  11128  nnabscl  11411  climshftlemg  11613  climshft  11615  mptfzshft  11753  fsumrev  11754  fisum0diag2  11758  efexp  11993  efzval  11994  demoivre  12084  dvdsval2  12101  iddvds  12115  1dvds  12116  dvds0  12117  negdvdsb  12118  dvdsnegb  12119  0dvds  12122  dvdsmul1  12124  iddvdsexp  12126  muldvds1  12127  muldvds2  12128  dvdscmul  12129  dvdsmulc  12130  summodnegmod  12133  modmulconst  12134  dvds2ln  12135  dvds2add  12136  dvds2sub  12137  dvdstr  12139  dvdssub2  12146  dvdsadd  12147  dvdsaddr  12148  dvdssub  12149  dvdssubr  12150  dvdsadd2b  12151  dvdsabseq  12158  divconjdvds  12160  alzdvds  12165  addmodlteqALT  12170  zeo3  12179  odd2np1lem  12183  odd2np1  12184  even2n  12185  oddp1even  12187  mulsucdiv2z  12196  zob  12202  ltoddhalfle  12204  halfleoddlt  12205  opoe  12206  omoe  12207  opeo  12208  omeo  12209  m1exp1  12212  divalgb  12236  divalgmod  12238  modremain  12240  ndvdssub  12241  ndvdsadd  12242  flodddiv4  12247  flodddiv4t2lthalf  12250  bits0  12259  bitsp1e  12263  bitsp1o  12264  gcdneg  12303  gcdadd  12306  gcdid  12307  modgcd  12312  dvdsgcd  12333  mulgcd  12337  absmulgcd  12338  mulgcdr  12339  gcddiv  12340  gcdmultiplez  12342  dvdssqim  12345  dvdssq  12352  bezoutr1  12354  lcmneg  12396  lcmgcdlem  12399  lcmgcd  12400  lcmid  12402  lcm1  12403  coprmdvds  12414  coprmdvds2  12415  qredeq  12418  qredeu  12419  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  prmdvdsexp  12470  rpexp1i  12476  sqrt2irr  12484  divnumden  12518  phiprmpw  12544  nnnn0modprm0  12578  modprmn0modprm0  12579  coprimeprodsq2  12581  pclemub  12610  pcprendvds2  12614  pcmul  12624  pcneg  12648  fldivp1  12671  prmpwdvds  12678  zgz  12696  4sqexercise1  12721  4sqexercise2  12722  modxai  12739  mulgz  13486  mulgassr  13496  mulgmodid  13497  gsumfzconst  13677  zsubrg  14343  zsssubrg  14347  zringmulg  14360  zringinvg  14366  mulgrhm2  14372  znunit  14421  ef2kpi  15278  efper  15279  sinperlem  15280  sin2kpi  15283  cos2kpi  15284  abssinper  15318  sinkpi  15319  coskpi  15320  cxpexprp  15367  sgmval2  15456  lgslem3  15479  lgsneg  15501  lgsdir2lem2  15506  lgsdir2lem4  15508  lgsdir2  15510  lgssq  15517  lgsmulsqcoprm  15523  lgsdirnn0  15524  gausslemma2dlem3  15540  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2  15560  2lgslem1a2  15564  2lgsoddprmlem1  15582  2lgsoddprmlem2  15583  2sqlem2  15592  2sqlem7  15598