ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zcn GIF version

Theorem zcn 9073
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
zcn (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Proof of Theorem zcn
StepHypRef Expression
1 zre 9072 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 7808 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1480  cc 7632  cz 9068
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 7726
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 7950  df-z 9069
This theorem is referenced by:  zsscn  9076  zaddcllempos  9105  peano2zm  9106  zaddcllemneg  9107  zaddcl  9108  zsubcl  9109  zrevaddcl  9118  nzadd  9120  zlem1lt  9124  zltlem1  9125  zapne  9139  zdiv  9153  zdivadd  9154  zdivmul  9155  zextlt  9157  zneo  9166  zeo2  9171  peano5uzti  9173  zindd  9183  divfnzn  9427  qmulz  9429  zq  9432  qaddcl  9441  qnegcl  9442  qmulcl  9443  qreccl  9448  fzen  9837  uzsubsubfz  9841  fz01en  9847  fzmmmeqm  9852  fzsubel  9854  fztp  9872  fzsuc2  9873  fzrev2  9879  fzrev3  9881  elfzp1b  9891  fzrevral  9899  fzrevral2  9900  fzrevral3  9901  fzshftral  9902  fzoaddel2  9984  fzosubel2  9986  eluzgtdifelfzo  9988  fzocatel  9990  elfzom1elp1fzo  9993  fzval3  9995  zpnn0elfzo1  9999  fzosplitprm1  10025  fzoshftral  10029  flqzadd  10085  2tnp1ge0ge0  10088  ceilid  10102  intfracq  10107  zmod10  10127  modqmuladdnn0  10155  addmodlteq  10185  frecfzen2  10214  ser3mono  10265  m1expeven  10354  expsubap  10355  zesq  10424  sqoddm1div8  10458  bccmpl  10514  shftuz  10603  nnabscl  10886  climshftlemg  11085  climshft  11087  mptfzshft  11225  fsumrev  11226  fisum0diag2  11230  efexp  11402  efzval  11403  demoivre  11492  dvdsval2  11509  iddvds  11519  1dvds  11520  dvds0  11521  negdvdsb  11522  dvdsnegb  11523  0dvds  11526  dvdsmul1  11528  iddvdsexp  11530  muldvds1  11531  muldvds2  11532  dvdscmul  11533  dvdsmulc  11534  summodnegmod  11537  modmulconst  11538  dvds2ln  11539  dvds2add  11540  dvds2sub  11541  dvdstr  11543  dvdssub2  11548  dvdsadd  11549  dvdsaddr  11550  dvdssub  11551  dvdssubr  11552  dvdsadd2b  11553  dvdsabseq  11558  divconjdvds  11560  alzdvds  11565  addmodlteqALT  11570  zeo3  11578  odd2np1lem  11582  odd2np1  11583  even2n  11584  oddp1even  11586  mulsucdiv2z  11595  zob  11601  ltoddhalfle  11603  halfleoddlt  11604  opoe  11605  omoe  11606  opeo  11607  omeo  11608  m1exp1  11611  divalgb  11635  divalgmod  11637  modremain  11639  ndvdssub  11640  ndvdsadd  11641  flodddiv4  11644  flodddiv4t2lthalf  11647  gcdneg  11683  gcdadd  11686  gcdid  11687  modgcd  11692  dvdsgcd  11713  mulgcd  11717  absmulgcd  11718  mulgcdr  11719  gcddiv  11720  gcdmultiplez  11722  dvdssqim  11725  dvdssq  11732  bezoutr1  11734  lcmneg  11768  lcmgcdlem  11771  lcmgcd  11772  lcmid  11774  lcm1  11775  coprmdvds  11786  coprmdvds2  11787  qredeq  11790  qredeu  11791  divgcdcoprmex  11796  cncongr1  11797  cncongr2  11798  prmdvdsexp  11839  rpexp1i  11845  sqrt2irr  11853  divnumden  11887  phiprmpw  11911  ef2kpi  12911  efper  12912  sinperlem  12913  sin2kpi  12916  cos2kpi  12917  abssinper  12951  sinkpi  12952  coskpi  12953  cxpexprp  12997
  Copyright terms: Public domain W3C validator