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

Theorem zcn 8437
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
zcn  |-  ( N  e.  ZZ  ->  N  e.  CC )

Proof of Theorem zcn
StepHypRef Expression
1 zre 8436 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 7209 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   CCcc 7041   ZZcz 8432
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 2064  ax-resscn 7130
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-rab 2358  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-iota 4897  df-fv 4940  df-ov 5546  df-neg 7349  df-z 8433
This theorem is referenced by:  zsscn  8440  zaddcllempos  8469  peano2zm  8470  zaddcllemneg  8471  zaddcl  8472  zsubcl  8473  zrevaddcl  8482  nzadd  8484  zlem1lt  8488  zltlem1  8489  zapne  8503  zdiv  8516  zdivadd  8517  zdivmul  8518  zextlt  8520  zneo  8529  zeo2  8534  peano5uzti  8536  zindd  8546  divfnzn  8787  qmulz  8789  zq  8792  qaddcl  8801  qnegcl  8802  qmulcl  8803  qreccl  8808  fzen  9138  uzsubsubfz  9142  fz01en  9148  fzmmmeqm  9152  fzsubel  9154  fztp  9171  fzsuc2  9172  fzrev2  9178  fzrev3  9180  elfzp1b  9190  fzrevral  9198  fzrevral2  9199  fzrevral3  9200  fzshftral  9201  fzoaddel2  9279  fzosubel2  9281  eluzgtdifelfzo  9283  fzocatel  9285  elfzom1elp1fzo  9288  fzval3  9290  zpnn0elfzo1  9294  fzosplitprm1  9320  fzoshftral  9324  flqzadd  9380  2tnp1ge0ge0  9383  ceilid  9397  intfracq  9402  zmod10  9422  modqmuladdnn0  9450  addmodlteq  9480  frecfzen2  9509  iseqshft2  9548  isermono  9553  m1expeven  9620  expsubap  9621  zesq  9688  sqoddm1div8  9722  bccmpl  9778  shftuz  9843  nnabscl  10124  climshftlemg  10279  climshft  10281  dvdsval2  10343  iddvds  10353  1dvds  10354  dvds0  10355  negdvdsb  10356  dvdsnegb  10357  0dvds  10360  dvdsmul1  10362  iddvdsexp  10364  muldvds1  10365  muldvds2  10366  dvdscmul  10367  dvdsmulc  10368  summodnegmod  10371  modmulconst  10372  dvds2ln  10373  dvds2add  10374  dvds2sub  10375  dvdstr  10377  dvdssub2  10382  dvdsadd  10383  dvdsaddr  10384  dvdssub  10385  dvdssubr  10386  dvdsadd2b  10387  dvdsabseq  10392  divconjdvds  10394  alzdvds  10399  addmodlteqALT  10404  zeo3  10412  odd2np1lem  10416  odd2np1  10417  even2n  10418  oddp1even  10420  mulsucdiv2z  10429  zob  10435  ltoddhalfle  10437  halfleoddlt  10438  opoe  10439  omoe  10440  opeo  10441  omeo  10442  m1exp1  10445  divalgb  10469  divalgmod  10471  modremain  10473  ndvdssub  10474  ndvdsadd  10475  flodddiv4  10478  flodddiv4t2lthalf  10481  gcdneg  10517  gcdadd  10520  gcdid  10521  modgcd  10526  dvdsgcd  10545  mulgcd  10549  absmulgcd  10550  mulgcdr  10551  gcddiv  10552  gcdmultiplez  10554  dvdssqim  10557  dvdssq  10564  bezoutr1  10566  lcmneg  10600  lcmgcdlem  10603  lcmgcd  10604  lcmid  10606  lcm1  10607  coprmdvds  10618  coprmdvds2  10619  qredeq  10622  qredeu  10623  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  prmdvdsexp  10671  rpexp1i  10677  sqrt2irr  10685  divnumden  10718
  Copyright terms: Public domain W3C validator