Theorem zcn 8651

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

Syntax hints:   → wi 4   ∈ wcel 1434  ℂcc 7251  ℤcz 8646

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-resscn 7340

This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-rab 2362  df-v 2614  df-un 2988  df-in 2990  df-ss 2997  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-iota 4934  df-fv 4977  df-ov 5594  df-neg 7559  df-z 8647

This theorem is referenced by:  zsscn  8654  zaddcllempos  8683  peano2zm  8684  zaddcllemneg  8685  zaddcl  8686  zsubcl  8687  zrevaddcl  8696  nzadd  8698  zlem1lt  8702  zltlem1  8703  zapne  8717  zdiv  8730  zdivadd  8731  zdivmul  8732  zextlt  8734  zneo  8743  zeo2  8748  peano5uzti  8750  zindd  8760  divfnzn  9001  qmulz  9003  zq  9006  qaddcl  9015  qnegcl  9016  qmulcl  9017  qreccl  9022  fzen  9352  uzsubsubfz  9356  fz01en  9362  fzmmmeqm  9366  fzsubel  9368  fztp  9385  fzsuc2  9386  fzrev2  9392  fzrev3  9394  elfzp1b  9404  fzrevral  9412  fzrevral2  9413  fzrevral3  9414  fzshftral  9415  fzoaddel2  9493  fzosubel2  9495  eluzgtdifelfzo  9497  fzocatel  9499  elfzom1elp1fzo  9502  fzval3  9504  zpnn0elfzo1  9508  fzosplitprm1  9534  fzoshftral  9538  flqzadd  9594  2tnp1ge0ge0  9597  ceilid  9611  intfracq  9616  zmod10  9636  modqmuladdnn0  9664  addmodlteq  9694  frecfzen2  9723  iseqshft2  9767  isermono  9772  m1expeven  9839  expsubap  9840  zesq  9907  sqoddm1div8  9941  bccmpl  9997  shftuz  10079  nnabscl  10360  climshftlemg  10515  climshft  10517  dvdsval2  10579  iddvds  10589  1dvds  10590  dvds0  10591  negdvdsb  10592  dvdsnegb  10593  0dvds  10596  dvdsmul1  10598  iddvdsexp  10600  muldvds1  10601  muldvds2  10602  dvdscmul  10603  dvdsmulc  10604  summodnegmod  10607  modmulconst  10608  dvds2ln  10609  dvds2add  10610  dvds2sub  10611  dvdstr  10613  dvdssub2  10618  dvdsadd  10619  dvdsaddr  10620  dvdssub  10621  dvdssubr  10622  dvdsadd2b  10623  dvdsabseq  10628  divconjdvds  10630  alzdvds  10635  addmodlteqALT  10640  zeo3  10648  odd2np1lem  10652  odd2np1  10653  even2n  10654  oddp1even  10656  mulsucdiv2z  10665  zob  10671  ltoddhalfle  10673  halfleoddlt  10674  opoe  10675  omoe  10676  opeo  10677  omeo  10678  m1exp1  10681  divalgb  10705  divalgmod  10707  modremain  10709  ndvdssub  10710  ndvdsadd  10711  flodddiv4  10714  flodddiv4t2lthalf  10717  gcdneg  10753  gcdadd  10756  gcdid  10757  modgcd  10762  dvdsgcd  10781  mulgcd  10785  absmulgcd  10786  mulgcdr  10787  gcddiv  10788  gcdmultiplez  10790  dvdssqim  10793  dvdssq  10800  bezoutr1  10802  lcmneg  10836  lcmgcdlem  10839  lcmgcd  10840  lcmid  10842  lcm1  10843  coprmdvds  10854  coprmdvds2  10855  qredeq  10858  qredeu  10859  divgcdcoprmex  10864  cncongr1  10865  cncongr2  10866  prmdvdsexp  10907  rpexp1i  10913  sqrt2irr  10921  divnumden  10954  phiprmpw  10978