Theorem zcn 9217

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7772  ℤcz 9212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-resscn 7866

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-rab 2457  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856  df-neg 8093  df-z 9213

This theorem is referenced by:  zsscn  9220  zaddcllempos  9249  peano2zm  9250  zaddcllemneg  9251  zaddcl  9252  zsubcl  9253  zrevaddcl  9262  nzadd  9264  zlem1lt  9268  zltlem1  9269  zapne  9286  zdiv  9300  zdivadd  9301  zdivmul  9302  zextlt  9304  zneo  9313  zeo2  9318  peano5uzti  9320  zindd  9330  divfnzn  9580  qmulz  9582  zq  9585  qaddcl  9594  qnegcl  9595  qmulcl  9596  qreccl  9601  fzen  9999  uzsubsubfz  10003  fz01en  10009  fzmmmeqm  10014  fzsubel  10016  fztp  10034  fzsuc2  10035  fzrev2  10041  fzrev3  10043  elfzp1b  10053  fzrevral  10061  fzrevral2  10062  fzrevral3  10063  fzshftral  10064  fzoaddel2  10149  fzosubel2  10151  eluzgtdifelfzo  10153  fzocatel  10155  elfzom1elp1fzo  10158  fzval3  10160  zpnn0elfzo1  10164  fzosplitprm1  10190  fzoshftral  10194  flqzadd  10254  2tnp1ge0ge0  10257  ceilid  10271  intfracq  10276  zmod10  10296  modqmuladdnn0  10324  addmodlteq  10354  frecfzen2  10383  ser3mono  10434  m1expeven  10523  expsubap  10524  zesq  10594  sqoddm1div8  10629  bccmpl  10688  shftuz  10781  nnabscl  11064  climshftlemg  11265  climshft  11267  mptfzshft  11405  fsumrev  11406  fisum0diag2  11410  efexp  11645  efzval  11646  demoivre  11735  dvdsval2  11752  iddvds  11766  1dvds  11767  dvds0  11768  negdvdsb  11769  dvdsnegb  11770  0dvds  11773  dvdsmul1  11775  iddvdsexp  11777  muldvds1  11778  muldvds2  11779  dvdscmul  11780  dvdsmulc  11781  summodnegmod  11784  modmulconst  11785  dvds2ln  11786  dvds2add  11787  dvds2sub  11788  dvdstr  11790  dvdssub2  11797  dvdsadd  11798  dvdsaddr  11799  dvdssub  11800  dvdssubr  11801  dvdsadd2b  11802  dvdsabseq  11807  divconjdvds  11809  alzdvds  11814  addmodlteqALT  11819  zeo3  11827  odd2np1lem  11831  odd2np1  11832  even2n  11833  oddp1even  11835  mulsucdiv2z  11844  zob  11850  ltoddhalfle  11852  halfleoddlt  11853  opoe  11854  omoe  11855  opeo  11856  omeo  11857  m1exp1  11860  divalgb  11884  divalgmod  11886  modremain  11888  ndvdssub  11889  ndvdsadd  11890  flodddiv4  11893  flodddiv4t2lthalf  11896  gcdneg  11937  gcdadd  11940  gcdid  11941  modgcd  11946  dvdsgcd  11967  mulgcd  11971  absmulgcd  11972  mulgcdr  11973  gcddiv  11974  gcdmultiplez  11976  dvdssqim  11979  dvdssq  11986  bezoutr1  11988  lcmneg  12028  lcmgcdlem  12031  lcmgcd  12032  lcmid  12034  lcm1  12035  coprmdvds  12046  coprmdvds2  12047  qredeq  12050  qredeu  12051  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  prmdvdsexp  12102  rpexp1i  12108  sqrt2irr  12116  divnumden  12150  phiprmpw  12176  nnnn0modprm0  12209  modprmn0modprm0  12210  coprimeprodsq2  12212  pclemub  12241  pcprendvds2  12245  pcmul  12255  pcneg  12278  fldivp1  12300  prmpwdvds  12307  zgz  12325  ef2kpi  13521  efper  13522  sinperlem  13523  sin2kpi  13526  cos2kpi  13527  abssinper  13561  sinkpi  13562  coskpi  13563  cxpexprp  13610  lgslem3  13697  lgsneg  13719  lgsdir2lem2  13724  lgsdir2lem4  13726  lgsdir2  13728  lgssq  13735  lgsmulsqcoprm  13741  lgsdirnn0  13742  2sqlem2  13745  2sqlem7  13751