Theorem zcn 9059

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

Syntax hints:   → wi 4   ∈ wcel 1480  ℂcc 7618  ℤcz 9054

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-resscn 7712

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-rab 2425  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777  df-neg 7936  df-z 9055

This theorem is referenced by:  zsscn  9062  zaddcllempos  9091  peano2zm  9092  zaddcllemneg  9093  zaddcl  9094  zsubcl  9095  zrevaddcl  9104  nzadd  9106  zlem1lt  9110  zltlem1  9111  zapne  9125  zdiv  9139  zdivadd  9140  zdivmul  9141  zextlt  9143  zneo  9152  zeo2  9157  peano5uzti  9159  zindd  9169  divfnzn  9413  qmulz  9415  zq  9418  qaddcl  9427  qnegcl  9428  qmulcl  9429  qreccl  9434  fzen  9823  uzsubsubfz  9827  fz01en  9833  fzmmmeqm  9838  fzsubel  9840  fztp  9858  fzsuc2  9859  fzrev2  9865  fzrev3  9867  elfzp1b  9877  fzrevral  9885  fzrevral2  9886  fzrevral3  9887  fzshftral  9888  fzoaddel2  9970  fzosubel2  9972  eluzgtdifelfzo  9974  fzocatel  9976  elfzom1elp1fzo  9979  fzval3  9981  zpnn0elfzo1  9985  fzosplitprm1  10011  fzoshftral  10015  flqzadd  10071  2tnp1ge0ge0  10074  ceilid  10088  intfracq  10093  zmod10  10113  modqmuladdnn0  10141  addmodlteq  10171  frecfzen2  10200  ser3mono  10251  m1expeven  10340  expsubap  10341  zesq  10410  sqoddm1div8  10444  bccmpl  10500  shftuz  10589  nnabscl  10872  climshftlemg  11071  climshft  11073  mptfzshft  11211  fsumrev  11212  fisum0diag2  11216  efexp  11388  efzval  11389  demoivre  11479  dvdsval2  11496  iddvds  11506  1dvds  11507  dvds0  11508  negdvdsb  11509  dvdsnegb  11510  0dvds  11513  dvdsmul1  11515  iddvdsexp  11517  muldvds1  11518  muldvds2  11519  dvdscmul  11520  dvdsmulc  11521  summodnegmod  11524  modmulconst  11525  dvds2ln  11526  dvds2add  11527  dvds2sub  11528  dvdstr  11530  dvdssub2  11535  dvdsadd  11536  dvdsaddr  11537  dvdssub  11538  dvdssubr  11539  dvdsadd2b  11540  dvdsabseq  11545  divconjdvds  11547  alzdvds  11552  addmodlteqALT  11557  zeo3  11565  odd2np1lem  11569  odd2np1  11570  even2n  11571  oddp1even  11573  mulsucdiv2z  11582  zob  11588  ltoddhalfle  11590  halfleoddlt  11591  opoe  11592  omoe  11593  opeo  11594  omeo  11595  m1exp1  11598  divalgb  11622  divalgmod  11624  modremain  11626  ndvdssub  11627  ndvdsadd  11628  flodddiv4  11631  flodddiv4t2lthalf  11634  gcdneg  11670  gcdadd  11673  gcdid  11674  modgcd  11679  dvdsgcd  11700  mulgcd  11704  absmulgcd  11705  mulgcdr  11706  gcddiv  11707  gcdmultiplez  11709  dvdssqim  11712  dvdssq  11719  bezoutr1  11721  lcmneg  11755  lcmgcdlem  11758  lcmgcd  11759  lcmid  11761  lcm1  11762  coprmdvds  11773  coprmdvds2  11774  qredeq  11777  qredeu  11778  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  prmdvdsexp  11826  rpexp1i  11832  sqrt2irr  11840  divnumden  11874  phiprmpw  11898  ef2kpi  12887  efper  12888  sinperlem  12889  sin2kpi  12892  cos2kpi  12893  abssinper  12927  sinkpi  12928  coskpi  12929