Theorem zcn 9447

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 7993  ℤcz 9442

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8087

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003  df-neg 8316  df-z 9443

This theorem is referenced by:  zsscn  9450  zaddcllempos  9479  peano2zm  9480  zaddcllemneg  9481  zaddcl  9482  zsubcl  9483  zrevaddcl  9493  nzadd  9495  zlem1lt  9499  zltlem1  9500  zapne  9517  zdiv  9531  zdivadd  9532  zdivmul  9533  zextlt  9535  zneo  9544  zeo2  9549  peano5uzti  9551  zindd  9561  divfnzn  9812  qmulz  9814  zq  9817  qaddcl  9826  qnegcl  9827  qmulcl  9828  qreccl  9833  fzen  10235  uzsubsubfz  10239  fz01en  10245  fzmmmeqm  10250  fzsubel  10252  fztp  10270  fzsuc2  10271  fzrev2  10277  fzrev3  10279  elfzp1b  10289  fzrevral  10297  fzrevral2  10298  fzrevral3  10299  fzshftral  10300  fzo0addel  10389  fzo0addelr  10390  fzoaddel2  10391  fzosubel2  10396  eluzgtdifelfzo  10398  fzocatel  10400  elfzom1elp1fzo  10403  fzval3  10405  zpnn0elfzo1  10409  fzosplitprm1  10435  fzoshftral  10439  flqzadd  10513  2tnp1ge0ge0  10516  ceilid  10532  intfracq  10537  zmod10  10557  modqmuladdnn0  10585  addmodlteq  10615  frecfzen2  10644  seqshft2g  10699  ser3mono  10704  m1expeven  10803  expsubap  10804  zesq  10875  sqoddm1div8  10910  bccmpl  10971  swrd00g  11176  swrdswrd  11232  swrdpfx  11234  pfxccatin12lem4  11253  pfxccatin12lem1  11255  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12  11260  shftuz  11323  nnabscl  11606  climshftlemg  11808  climshft  11810  mptfzshft  11948  fsumrev  11949  fisum0diag2  11953  efexp  12188  efzval  12189  demoivre  12279  dvdsval2  12296  iddvds  12310  1dvds  12311  dvds0  12312  negdvdsb  12313  dvdsnegb  12314  0dvds  12317  dvdsmul1  12319  iddvdsexp  12321  muldvds1  12322  muldvds2  12323  dvdscmul  12324  dvdsmulc  12325  summodnegmod  12328  modmulconst  12329  dvds2ln  12330  dvds2add  12331  dvds2sub  12332  dvdstr  12334  dvdssub2  12341  dvdsadd  12342  dvdsaddr  12343  dvdssub  12344  dvdssubr  12345  dvdsadd2b  12346  dvdsabseq  12353  divconjdvds  12355  alzdvds  12360  addmodlteqALT  12365  zeo3  12374  odd2np1lem  12378  odd2np1  12379  even2n  12380  oddp1even  12382  mulsucdiv2z  12391  zob  12397  ltoddhalfle  12399  halfleoddlt  12400  opoe  12401  omoe  12402  opeo  12403  omeo  12404  m1exp1  12407  divalgb  12431  divalgmod  12433  modremain  12435  ndvdssub  12436  ndvdsadd  12437  flodddiv4  12442  flodddiv4t2lthalf  12445  bits0  12454  bitsp1e  12458  bitsp1o  12459  gcdneg  12498  gcdadd  12501  gcdid  12502  modgcd  12507  dvdsgcd  12528  mulgcd  12532  absmulgcd  12533  mulgcdr  12534  gcddiv  12535  gcdmultiplez  12537  dvdssqim  12540  dvdssq  12547  bezoutr1  12549  lcmneg  12591  lcmgcdlem  12594  lcmgcd  12595  lcmid  12597  lcm1  12598  coprmdvds  12609  coprmdvds2  12610  qredeq  12613  qredeu  12614  divgcdcoprmex  12619  cncongr1  12620  cncongr2  12621  prmdvdsexp  12665  rpexp1i  12671  sqrt2irr  12679  divnumden  12713  phiprmpw  12739  nnnn0modprm0  12773  modprmn0modprm0  12774  coprimeprodsq2  12776  pclemub  12805  pcprendvds2  12809  pcmul  12819  pcneg  12843  fldivp1  12866  prmpwdvds  12873  zgz  12891  4sqexercise1  12916  4sqexercise2  12917  modxai  12934  mulgz  13682  mulgassr  13692  mulgmodid  13693  gsumfzconst  13873  zsubrg  14539  zsssubrg  14543  zringmulg  14556  zringinvg  14562  mulgrhm2  14568  znunit  14617  ef2kpi  15474  efper  15475  sinperlem  15476  sin2kpi  15479  cos2kpi  15480  abssinper  15514  sinkpi  15515  coskpi  15516  cxpexprp  15563  sgmval2  15652  lgslem3  15675  lgsneg  15697  lgsdir2lem2  15702  lgsdir2lem4  15704  lgsdir2  15706  lgssq  15713  lgsmulsqcoprm  15719  lgsdirnn0  15720  gausslemma2dlem3  15736  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2  15756  2lgslem1a2  15760  2lgsoddprmlem1  15778  2lgsoddprmlem2  15779  2sqlem2  15788  2sqlem7  15794