Theorem zcn 9325

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7872  ℤcz 9320

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7966

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-rab 2481  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922  df-neg 8195  df-z 9321

This theorem is referenced by:  zsscn  9328  zaddcllempos  9357  peano2zm  9358  zaddcllemneg  9359  zaddcl  9360  zsubcl  9361  zrevaddcl  9370  nzadd  9372  zlem1lt  9376  zltlem1  9377  zapne  9394  zdiv  9408  zdivadd  9409  zdivmul  9410  zextlt  9412  zneo  9421  zeo2  9426  peano5uzti  9428  zindd  9438  divfnzn  9689  qmulz  9691  zq  9694  qaddcl  9703  qnegcl  9704  qmulcl  9705  qreccl  9710  fzen  10112  uzsubsubfz  10116  fz01en  10122  fzmmmeqm  10127  fzsubel  10129  fztp  10147  fzsuc2  10148  fzrev2  10154  fzrev3  10156  elfzp1b  10166  fzrevral  10174  fzrevral2  10175  fzrevral3  10176  fzshftral  10177  fzoaddel2  10263  fzosubel2  10265  eluzgtdifelfzo  10267  fzocatel  10269  elfzom1elp1fzo  10272  fzval3  10274  zpnn0elfzo1  10278  fzosplitprm1  10304  fzoshftral  10308  flqzadd  10370  2tnp1ge0ge0  10373  ceilid  10389  intfracq  10394  zmod10  10414  modqmuladdnn0  10442  addmodlteq  10472  frecfzen2  10501  seqshft2g  10556  ser3mono  10561  m1expeven  10660  expsubap  10661  zesq  10732  sqoddm1div8  10767  bccmpl  10828  shftuz  10964  nnabscl  11247  climshftlemg  11448  climshft  11450  mptfzshft  11588  fsumrev  11589  fisum0diag2  11593  efexp  11828  efzval  11829  demoivre  11919  dvdsval2  11936  iddvds  11950  1dvds  11951  dvds0  11952  negdvdsb  11953  dvdsnegb  11954  0dvds  11957  dvdsmul1  11959  iddvdsexp  11961  muldvds1  11962  muldvds2  11963  dvdscmul  11964  dvdsmulc  11965  summodnegmod  11968  modmulconst  11969  dvds2ln  11970  dvds2add  11971  dvds2sub  11972  dvdstr  11974  dvdssub2  11981  dvdsadd  11982  dvdsaddr  11983  dvdssub  11984  dvdssubr  11985  dvdsadd2b  11986  dvdsabseq  11992  divconjdvds  11994  alzdvds  11999  addmodlteqALT  12004  zeo3  12012  odd2np1lem  12016  odd2np1  12017  even2n  12018  oddp1even  12020  mulsucdiv2z  12029  zob  12035  ltoddhalfle  12037  halfleoddlt  12038  opoe  12039  omoe  12040  opeo  12041  omeo  12042  m1exp1  12045  divalgb  12069  divalgmod  12071  modremain  12073  ndvdssub  12074  ndvdsadd  12075  flodddiv4  12078  flodddiv4t2lthalf  12081  gcdneg  12122  gcdadd  12125  gcdid  12126  modgcd  12131  dvdsgcd  12152  mulgcd  12156  absmulgcd  12157  mulgcdr  12158  gcddiv  12159  gcdmultiplez  12161  dvdssqim  12164  dvdssq  12171  bezoutr1  12173  lcmneg  12215  lcmgcdlem  12218  lcmgcd  12219  lcmid  12221  lcm1  12222  coprmdvds  12233  coprmdvds2  12234  qredeq  12237  qredeu  12238  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  prmdvdsexp  12289  rpexp1i  12295  sqrt2irr  12303  divnumden  12337  phiprmpw  12363  nnnn0modprm0  12396  modprmn0modprm0  12397  coprimeprodsq2  12399  pclemub  12428  pcprendvds2  12432  pcmul  12442  pcneg  12466  fldivp1  12489  prmpwdvds  12496  zgz  12514  4sqexercise1  12539  4sqexercise2  12540  mulgz  13223  mulgassr  13233  mulgmodid  13234  gsumfzconst  13414  zsubrg  14080  zsssubrg  14084  zringmulg  14097  zringinvg  14103  mulgrhm2  14109  znunit  14158  ef2kpi  14982  efper  14983  sinperlem  14984  sin2kpi  14987  cos2kpi  14988  abssinper  15022  sinkpi  15023  coskpi  15024  cxpexprp  15071  lgslem3  15159  lgsneg  15181  lgsdir2lem2  15186  lgsdir2lem4  15188  lgsdir2  15190  lgssq  15197  lgsmulsqcoprm  15203  lgsdirnn0  15204  gausslemma2dlem3  15220  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2  15240  2lgslem1a2  15244  2lgsoddprmlem1  15262  2lgsoddprmlem2  15263  2sqlem2  15272  2sqlem7  15278