Theorem zcn 9483

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8029  ℤcz 9478

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020  df-neg 8352  df-z 9479

This theorem is referenced by:  zsscn  9486  zaddcllempos  9515  peano2zm  9516  zaddcllemneg  9517  zaddcl  9518  zsubcl  9519  zrevaddcl  9529  nzadd  9531  zlem1lt  9535  zltlem1  9536  zapne  9553  zdiv  9567  zdivadd  9568  zdivmul  9569  zextlt  9571  zneo  9580  zeo2  9585  peano5uzti  9587  zindd  9597  divfnzn  9854  qmulz  9856  zq  9859  qaddcl  9868  qnegcl  9869  qmulcl  9870  qreccl  9875  fzen  10277  uzsubsubfz  10281  fz01en  10287  fzmmmeqm  10292  fzsubel  10294  fztp  10312  fzsuc2  10313  fzrev2  10319  fzrev3  10321  elfzp1b  10331  fzrevral  10339  fzrevral2  10340  fzrevral3  10341  fzshftral  10342  fzo0addel  10432  fzo0addelr  10433  fzoaddel2  10434  fzosubel2  10439  eluzgtdifelfzo  10441  fzocatel  10443  elfzom1elp1fzo  10446  fzval3  10448  zpnn0elfzo1  10452  fzosplitprm1  10479  fzoshftral  10483  flqzadd  10557  2tnp1ge0ge0  10560  ceilid  10576  intfracq  10581  zmod10  10601  modqmuladdnn0  10629  addmodlteq  10659  frecfzen2  10688  seqshft2g  10743  ser3mono  10748  m1expeven  10847  expsubap  10848  zesq  10919  sqoddm1div8  10954  bccmpl  11015  swrd00g  11229  swrdswrd  11285  swrdpfx  11287  pfxccatin12lem4  11306  pfxccatin12lem1  11308  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12  11313  shftuz  11377  nnabscl  11660  climshftlemg  11862  climshft  11864  mptfzshft  12002  fsumrev  12003  fisum0diag2  12007  efexp  12242  efzval  12243  demoivre  12333  dvdsval2  12350  iddvds  12364  1dvds  12365  dvds0  12366  negdvdsb  12367  dvdsnegb  12368  0dvds  12371  dvdsmul1  12373  iddvdsexp  12375  muldvds1  12376  muldvds2  12377  dvdscmul  12378  dvdsmulc  12379  summodnegmod  12382  modmulconst  12383  dvds2ln  12384  dvds2add  12385  dvds2sub  12386  dvdstr  12388  dvdssub2  12395  dvdsadd  12396  dvdsaddr  12397  dvdssub  12398  dvdssubr  12399  dvdsadd2b  12400  dvdsabseq  12407  divconjdvds  12409  alzdvds  12414  addmodlteqALT  12419  zeo3  12428  odd2np1lem  12432  odd2np1  12433  even2n  12434  oddp1even  12436  mulsucdiv2z  12445  zob  12451  ltoddhalfle  12453  halfleoddlt  12454  opoe  12455  omoe  12456  opeo  12457  omeo  12458  m1exp1  12461  divalgb  12485  divalgmod  12487  modremain  12489  ndvdssub  12490  ndvdsadd  12491  flodddiv4  12496  flodddiv4t2lthalf  12499  bits0  12508  bitsp1e  12512  bitsp1o  12513  gcdneg  12552  gcdadd  12555  gcdid  12556  modgcd  12561  dvdsgcd  12582  mulgcd  12586  absmulgcd  12587  mulgcdr  12588  gcddiv  12589  gcdmultiplez  12591  dvdssqim  12594  dvdssq  12601  bezoutr1  12603  lcmneg  12645  lcmgcdlem  12648  lcmgcd  12649  lcmid  12651  lcm1  12652  coprmdvds  12663  coprmdvds2  12664  qredeq  12667  qredeu  12668  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  prmdvdsexp  12719  rpexp1i  12725  sqrt2irr  12733  divnumden  12767  phiprmpw  12793  nnnn0modprm0  12827  modprmn0modprm0  12828  coprimeprodsq2  12830  pclemub  12859  pcprendvds2  12863  pcmul  12873  pcneg  12897  fldivp1  12920  prmpwdvds  12927  zgz  12945  4sqexercise1  12970  4sqexercise2  12971  modxai  12988  mulgz  13736  mulgassr  13746  mulgmodid  13747  gsumfzconst  13927  zsubrg  14594  zsssubrg  14598  zringmulg  14611  zringinvg  14617  mulgrhm2  14623  znunit  14672  ef2kpi  15529  efper  15530  sinperlem  15531  sin2kpi  15534  cos2kpi  15535  abssinper  15569  sinkpi  15570  coskpi  15571  cxpexprp  15618  sgmval2  15707  lgslem3  15730  lgsneg  15752  lgsdir2lem2  15757  lgsdir2lem4  15759  lgsdir2  15761  lgssq  15768  lgsmulsqcoprm  15774  lgsdirnn0  15775  gausslemma2dlem3  15791  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2  15811  2lgslem1a2  15815  2lgsoddprmlem1  15833  2lgsoddprmlem2  15834  2sqlem2  15843  2sqlem7  15849  wlk1walkdom  16209