Theorem zcn 9474

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8020  ℤcz 9469

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8114

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016  df-neg 8343  df-z 9470

This theorem is referenced by:  zsscn  9477  zaddcllempos  9506  peano2zm  9507  zaddcllemneg  9508  zaddcl  9509  zsubcl  9510  zrevaddcl  9520  nzadd  9522  zlem1lt  9526  zltlem1  9527  zapne  9544  zdiv  9558  zdivadd  9559  zdivmul  9560  zextlt  9562  zneo  9571  zeo2  9576  peano5uzti  9578  zindd  9588  divfnzn  9845  qmulz  9847  zq  9850  qaddcl  9859  qnegcl  9860  qmulcl  9861  qreccl  9866  fzen  10268  uzsubsubfz  10272  fz01en  10278  fzmmmeqm  10283  fzsubel  10285  fztp  10303  fzsuc2  10304  fzrev2  10310  fzrev3  10312  elfzp1b  10322  fzrevral  10330  fzrevral2  10331  fzrevral3  10332  fzshftral  10333  fzo0addel  10423  fzo0addelr  10424  fzoaddel2  10425  fzosubel2  10430  eluzgtdifelfzo  10432  fzocatel  10434  elfzom1elp1fzo  10437  fzval3  10439  zpnn0elfzo1  10443  fzosplitprm1  10470  fzoshftral  10474  flqzadd  10548  2tnp1ge0ge0  10551  ceilid  10567  intfracq  10572  zmod10  10592  modqmuladdnn0  10620  addmodlteq  10650  frecfzen2  10679  seqshft2g  10734  ser3mono  10739  m1expeven  10838  expsubap  10839  zesq  10910  sqoddm1div8  10945  bccmpl  11006  swrd00g  11220  swrdswrd  11276  swrdpfx  11278  pfxccatin12lem4  11297  pfxccatin12lem1  11299  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12  11304  shftuz  11368  nnabscl  11651  climshftlemg  11853  climshft  11855  mptfzshft  11993  fsumrev  11994  fisum0diag2  11998  efexp  12233  efzval  12234  demoivre  12324  dvdsval2  12341  iddvds  12355  1dvds  12356  dvds0  12357  negdvdsb  12358  dvdsnegb  12359  0dvds  12362  dvdsmul1  12364  iddvdsexp  12366  muldvds1  12367  muldvds2  12368  dvdscmul  12369  dvdsmulc  12370  summodnegmod  12373  modmulconst  12374  dvds2ln  12375  dvds2add  12376  dvds2sub  12377  dvdstr  12379  dvdssub2  12386  dvdsadd  12387  dvdsaddr  12388  dvdssub  12389  dvdssubr  12390  dvdsadd2b  12391  dvdsabseq  12398  divconjdvds  12400  alzdvds  12405  addmodlteqALT  12410  zeo3  12419  odd2np1lem  12423  odd2np1  12424  even2n  12425  oddp1even  12427  mulsucdiv2z  12436  zob  12442  ltoddhalfle  12444  halfleoddlt  12445  opoe  12446  omoe  12447  opeo  12448  omeo  12449  m1exp1  12452  divalgb  12476  divalgmod  12478  modremain  12480  ndvdssub  12481  ndvdsadd  12482  flodddiv4  12487  flodddiv4t2lthalf  12490  bits0  12499  bitsp1e  12503  bitsp1o  12504  gcdneg  12543  gcdadd  12546  gcdid  12547  modgcd  12552  dvdsgcd  12573  mulgcd  12577  absmulgcd  12578  mulgcdr  12579  gcddiv  12580  gcdmultiplez  12582  dvdssqim  12585  dvdssq  12592  bezoutr1  12594  lcmneg  12636  lcmgcdlem  12639  lcmgcd  12640  lcmid  12642  lcm1  12643  coprmdvds  12654  coprmdvds2  12655  qredeq  12658  qredeu  12659  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  prmdvdsexp  12710  rpexp1i  12716  sqrt2irr  12724  divnumden  12758  phiprmpw  12784  nnnn0modprm0  12818  modprmn0modprm0  12819  coprimeprodsq2  12821  pclemub  12850  pcprendvds2  12854  pcmul  12864  pcneg  12888  fldivp1  12911  prmpwdvds  12918  zgz  12936  4sqexercise1  12961  4sqexercise2  12962  modxai  12979  mulgz  13727  mulgassr  13737  mulgmodid  13738  gsumfzconst  13918  zsubrg  14585  zsssubrg  14589  zringmulg  14602  zringinvg  14608  mulgrhm2  14614  znunit  14663  ef2kpi  15520  efper  15521  sinperlem  15522  sin2kpi  15525  cos2kpi  15526  abssinper  15560  sinkpi  15561  coskpi  15562  cxpexprp  15609  sgmval2  15698  lgslem3  15721  lgsneg  15743  lgsdir2lem2  15748  lgsdir2lem4  15750  lgsdir2  15752  lgssq  15759  lgsmulsqcoprm  15765  lgsdirnn0  15766  gausslemma2dlem3  15782  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2  15802  2lgslem1a2  15806  2lgsoddprmlem1  15824  2lgsoddprmlem2  15825  2sqlem2  15834  2sqlem7  15840  wlk1walkdom  16156