Theorem zcn 9258

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7809  ℤcz 9253

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7903

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-rab 2464  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878  df-neg 8131  df-z 9254

This theorem is referenced by:  zsscn  9261  zaddcllempos  9290  peano2zm  9291  zaddcllemneg  9292  zaddcl  9293  zsubcl  9294  zrevaddcl  9303  nzadd  9305  zlem1lt  9309  zltlem1  9310  zapne  9327  zdiv  9341  zdivadd  9342  zdivmul  9343  zextlt  9345  zneo  9354  zeo2  9359  peano5uzti  9361  zindd  9371  divfnzn  9621  qmulz  9623  zq  9626  qaddcl  9635  qnegcl  9636  qmulcl  9637  qreccl  9642  fzen  10043  uzsubsubfz  10047  fz01en  10053  fzmmmeqm  10058  fzsubel  10060  fztp  10078  fzsuc2  10079  fzrev2  10085  fzrev3  10087  elfzp1b  10097  fzrevral  10105  fzrevral2  10106  fzrevral3  10107  fzshftral  10108  fzoaddel2  10193  fzosubel2  10195  eluzgtdifelfzo  10197  fzocatel  10199  elfzom1elp1fzo  10202  fzval3  10204  zpnn0elfzo1  10208  fzosplitprm1  10234  fzoshftral  10238  flqzadd  10298  2tnp1ge0ge0  10301  ceilid  10315  intfracq  10320  zmod10  10340  modqmuladdnn0  10368  addmodlteq  10398  frecfzen2  10427  ser3mono  10478  m1expeven  10567  expsubap  10568  zesq  10639  sqoddm1div8  10674  bccmpl  10734  shftuz  10826  nnabscl  11109  climshftlemg  11310  climshft  11312  mptfzshft  11450  fsumrev  11451  fisum0diag2  11455  efexp  11690  efzval  11691  demoivre  11780  dvdsval2  11797  iddvds  11811  1dvds  11812  dvds0  11813  negdvdsb  11814  dvdsnegb  11815  0dvds  11818  dvdsmul1  11820  iddvdsexp  11822  muldvds1  11823  muldvds2  11824  dvdscmul  11825  dvdsmulc  11826  summodnegmod  11829  modmulconst  11830  dvds2ln  11831  dvds2add  11832  dvds2sub  11833  dvdstr  11835  dvdssub2  11842  dvdsadd  11843  dvdsaddr  11844  dvdssub  11845  dvdssubr  11846  dvdsadd2b  11847  dvdsabseq  11853  divconjdvds  11855  alzdvds  11860  addmodlteqALT  11865  zeo3  11873  odd2np1lem  11877  odd2np1  11878  even2n  11879  oddp1even  11881  mulsucdiv2z  11890  zob  11896  ltoddhalfle  11898  halfleoddlt  11899  opoe  11900  omoe  11901  opeo  11902  omeo  11903  m1exp1  11906  divalgb  11930  divalgmod  11932  modremain  11934  ndvdssub  11935  ndvdsadd  11936  flodddiv4  11939  flodddiv4t2lthalf  11942  gcdneg  11983  gcdadd  11986  gcdid  11987  modgcd  11992  dvdsgcd  12013  mulgcd  12017  absmulgcd  12018  mulgcdr  12019  gcddiv  12020  gcdmultiplez  12022  dvdssqim  12025  dvdssq  12032  bezoutr1  12034  lcmneg  12074  lcmgcdlem  12077  lcmgcd  12078  lcmid  12080  lcm1  12081  coprmdvds  12092  coprmdvds2  12093  qredeq  12096  qredeu  12097  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  prmdvdsexp  12148  rpexp1i  12154  sqrt2irr  12162  divnumden  12196  phiprmpw  12222  nnnn0modprm0  12255  modprmn0modprm0  12256  coprimeprodsq2  12258  pclemub  12287  pcprendvds2  12291  pcmul  12301  pcneg  12324  fldivp1  12346  prmpwdvds  12353  zgz  12371  mulgz  13011  mulgassr  13021  mulgmodid  13022  zsubrg  13478  zsssubrg  13482  zringmulg  13491  zringinvg  13497  ef2kpi  14230  efper  14231  sinperlem  14232  sin2kpi  14235  cos2kpi  14236  abssinper  14270  sinkpi  14271  coskpi  14272  cxpexprp  14319  lgslem3  14406  lgsneg  14428  lgsdir2lem2  14433  lgsdir2lem4  14435  lgsdir2  14437  lgssq  14444  lgsmulsqcoprm  14450  lgsdirnn0  14451  2lgsoddprmlem1  14456  2lgsoddprmlem2  14457  2sqlem2  14465  2sqlem7  14471