Theorem zcn 9206

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7761  ℤcz 9201

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 7855

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 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5854  df-neg 8082  df-z 9202

This theorem is referenced by:  zsscn  9209  zaddcllempos  9238  peano2zm  9239  zaddcllemneg  9240  zaddcl  9241  zsubcl  9242  zrevaddcl  9251  nzadd  9253  zlem1lt  9257  zltlem1  9258  zapne  9275  zdiv  9289  zdivadd  9290  zdivmul  9291  zextlt  9293  zneo  9302  zeo2  9307  peano5uzti  9309  zindd  9319  divfnzn  9569  qmulz  9571  zq  9574  qaddcl  9583  qnegcl  9584  qmulcl  9585  qreccl  9590  fzen  9988  uzsubsubfz  9992  fz01en  9998  fzmmmeqm  10003  fzsubel  10005  fztp  10023  fzsuc2  10024  fzrev2  10030  fzrev3  10032  elfzp1b  10042  fzrevral  10050  fzrevral2  10051  fzrevral3  10052  fzshftral  10053  fzoaddel2  10138  fzosubel2  10140  eluzgtdifelfzo  10142  fzocatel  10144  elfzom1elp1fzo  10147  fzval3  10149  zpnn0elfzo1  10153  fzosplitprm1  10179  fzoshftral  10183  flqzadd  10243  2tnp1ge0ge0  10246  ceilid  10260  intfracq  10265  zmod10  10285  modqmuladdnn0  10313  addmodlteq  10343  frecfzen2  10372  ser3mono  10423  m1expeven  10512  expsubap  10513  zesq  10583  sqoddm1div8  10618  bccmpl  10677  shftuz  10770  nnabscl  11053  climshftlemg  11254  climshft  11256  mptfzshft  11394  fsumrev  11395  fisum0diag2  11399  efexp  11634  efzval  11635  demoivre  11724  dvdsval2  11741  iddvds  11755  1dvds  11756  dvds0  11757  negdvdsb  11758  dvdsnegb  11759  0dvds  11762  dvdsmul1  11764  iddvdsexp  11766  muldvds1  11767  muldvds2  11768  dvdscmul  11769  dvdsmulc  11770  summodnegmod  11773  modmulconst  11774  dvds2ln  11775  dvds2add  11776  dvds2sub  11777  dvdstr  11779  dvdssub2  11786  dvdsadd  11787  dvdsaddr  11788  dvdssub  11789  dvdssubr  11790  dvdsadd2b  11791  dvdsabseq  11796  divconjdvds  11798  alzdvds  11803  addmodlteqALT  11808  zeo3  11816  odd2np1lem  11820  odd2np1  11821  even2n  11822  oddp1even  11824  mulsucdiv2z  11833  zob  11839  ltoddhalfle  11841  halfleoddlt  11842  opoe  11843  omoe  11844  opeo  11845  omeo  11846  m1exp1  11849  divalgb  11873  divalgmod  11875  modremain  11877  ndvdssub  11878  ndvdsadd  11879  flodddiv4  11882  flodddiv4t2lthalf  11885  gcdneg  11926  gcdadd  11929  gcdid  11930  modgcd  11935  dvdsgcd  11956  mulgcd  11960  absmulgcd  11961  mulgcdr  11962  gcddiv  11963  gcdmultiplez  11965  dvdssqim  11968  dvdssq  11975  bezoutr1  11977  lcmneg  12017  lcmgcdlem  12020  lcmgcd  12021  lcmid  12023  lcm1  12024  coprmdvds  12035  coprmdvds2  12036  qredeq  12039  qredeu  12040  divgcdcoprmex  12045  cncongr1  12046  cncongr2  12047  prmdvdsexp  12091  rpexp1i  12097  sqrt2irr  12105  divnumden  12139  phiprmpw  12165  nnnn0modprm0  12198  modprmn0modprm0  12199  coprimeprodsq2  12201  pclemub  12230  pcprendvds2  12234  pcmul  12244  pcneg  12267  fldivp1  12289  prmpwdvds  12296  zgz  12314  ef2kpi  13482  efper  13483  sinperlem  13484  sin2kpi  13487  cos2kpi  13488  abssinper  13522  sinkpi  13523  coskpi  13524  cxpexprp  13571  lgslem3  13658  lgsneg  13680  lgsdir2lem2  13685  lgsdir2lem4  13687  lgsdir2  13689  lgssq  13696  lgsmulsqcoprm  13702  lgsdirnn0  13703  2sqlem2  13706  2sqlem7  13712