Theorem zcn 9192

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 7747  ℤcz 9187

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7841

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-rab 2452  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844  df-neg 8068  df-z 9188

This theorem is referenced by:  zsscn  9195  zaddcllempos  9224  peano2zm  9225  zaddcllemneg  9226  zaddcl  9227  zsubcl  9228  zrevaddcl  9237  nzadd  9239  zlem1lt  9243  zltlem1  9244  zapne  9261  zdiv  9275  zdivadd  9276  zdivmul  9277  zextlt  9279  zneo  9288  zeo2  9293  peano5uzti  9295  zindd  9305  divfnzn  9555  qmulz  9557  zq  9560  qaddcl  9569  qnegcl  9570  qmulcl  9571  qreccl  9576  fzen  9974  uzsubsubfz  9978  fz01en  9984  fzmmmeqm  9989  fzsubel  9991  fztp  10009  fzsuc2  10010  fzrev2  10016  fzrev3  10018  elfzp1b  10028  fzrevral  10036  fzrevral2  10037  fzrevral3  10038  fzshftral  10039  fzoaddel2  10124  fzosubel2  10126  eluzgtdifelfzo  10128  fzocatel  10130  elfzom1elp1fzo  10133  fzval3  10135  zpnn0elfzo1  10139  fzosplitprm1  10165  fzoshftral  10169  flqzadd  10229  2tnp1ge0ge0  10232  ceilid  10246  intfracq  10251  zmod10  10271  modqmuladdnn0  10299  addmodlteq  10329  frecfzen2  10358  ser3mono  10409  m1expeven  10498  expsubap  10499  zesq  10569  sqoddm1div8  10604  bccmpl  10663  shftuz  10755  nnabscl  11038  climshftlemg  11239  climshft  11241  mptfzshft  11379  fsumrev  11380  fisum0diag2  11384  efexp  11619  efzval  11620  demoivre  11709  dvdsval2  11726  iddvds  11740  1dvds  11741  dvds0  11742  negdvdsb  11743  dvdsnegb  11744  0dvds  11747  dvdsmul1  11749  iddvdsexp  11751  muldvds1  11752  muldvds2  11753  dvdscmul  11754  dvdsmulc  11755  summodnegmod  11758  modmulconst  11759  dvds2ln  11760  dvds2add  11761  dvds2sub  11762  dvdstr  11764  dvdssub2  11771  dvdsadd  11772  dvdsaddr  11773  dvdssub  11774  dvdssubr  11775  dvdsadd2b  11776  dvdsabseq  11781  divconjdvds  11783  alzdvds  11788  addmodlteqALT  11793  zeo3  11801  odd2np1lem  11805  odd2np1  11806  even2n  11807  oddp1even  11809  mulsucdiv2z  11818  zob  11824  ltoddhalfle  11826  halfleoddlt  11827  opoe  11828  omoe  11829  opeo  11830  omeo  11831  m1exp1  11834  divalgb  11858  divalgmod  11860  modremain  11862  ndvdssub  11863  ndvdsadd  11864  flodddiv4  11867  flodddiv4t2lthalf  11870  gcdneg  11911  gcdadd  11914  gcdid  11915  modgcd  11920  dvdsgcd  11941  mulgcd  11945  absmulgcd  11946  mulgcdr  11947  gcddiv  11948  gcdmultiplez  11950  dvdssqim  11953  dvdssq  11960  bezoutr1  11962  lcmneg  12002  lcmgcdlem  12005  lcmgcd  12006  lcmid  12008  lcm1  12009  coprmdvds  12020  coprmdvds2  12021  qredeq  12024  qredeu  12025  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  prmdvdsexp  12076  rpexp1i  12082  sqrt2irr  12090  divnumden  12124  phiprmpw  12150  nnnn0modprm0  12183  modprmn0modprm0  12184  coprimeprodsq2  12186  pclemub  12215  pcprendvds2  12219  pcmul  12229  pcneg  12252  fldivp1  12274  prmpwdvds  12281  zgz  12299  ef2kpi  13327  efper  13328  sinperlem  13329  sin2kpi  13332  cos2kpi  13333  abssinper  13367  sinkpi  13368  coskpi  13369  cxpexprp  13416  lgslem3  13503  lgsneg  13525  lgsdir2lem2  13530  lgsdir2lem4  13532  lgsdir2  13534  lgssq  13541  lgsmulsqcoprm  13547  lgsdirnn0  13548  2sqlem2  13551  2sqlem7  13557