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

Theorem nncn 8740
Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
Assertion
Ref Expression
nncn  |-  ( A  e.  NN  ->  A  e.  CC )

Proof of Theorem nncn
StepHypRef Expression
1 nnsscn 8737 . 2  |-  NN  C_  CC
21sseli 3093 1  |-  ( A  e.  NN  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1480   CCcc 7630   NNcn 8732
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-sep 4046  ax-cnex 7723  ax-resscn 7724  ax-1re 7726  ax-addrcl 7729
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-v 2688  df-in 3077  df-ss 3084  df-int 3772  df-inn 8733
This theorem is referenced by:  nn1m1nn  8750  nn1suc  8751  nnaddcl  8752  nnmulcl  8753  nnsub  8771  nndiv  8773  nndivtr  8774  nnnn0addcl  9019  nn0nnaddcl  9020  elnnnn0  9032  nnnegz  9069  zaddcllempos  9103  zaddcllemneg  9105  nnaddm1cl  9127  elz2  9134  zdiv  9151  zdivadd  9152  zdivmul  9153  nneoor  9165  nneo  9166  divfnzn  9425  qmulz  9427  qaddcl  9439  qnegcl  9440  qmulcl  9441  qreccl  9446  nnledivrp  9565  nn0ledivnn  9566  fseq1m1p1  9887  nnsplit  9926  ubmelm1fzo  10015  subfzo0  10031  flqdiv  10106  addmodidr  10158  modfzo0difsn  10180  nn0ennn  10218  expnegap0  10313  expm1t  10333  nnsqcl  10374  nnlesq  10408  facdiv  10496  facndiv  10497  faclbnd  10499  bcn1  10516  bcn2m1  10527  arisum  11279  arisum2  11280  expcnvap0  11283  mertenslem2  11317  ef0lem  11378  efexp  11400  nndivides  11511  modmulconst  11536  dvdsflip  11560  nn0enne  11610  nno  11614  divalgmod  11635  ndvdsadd  11639  modgcd  11690  gcddiv  11718  gcdmultiple  11719  gcdmultiplez  11720  rpmulgcd  11725  rplpwr  11726  sqgcd  11728  lcmgcdlem  11769  qredeq  11788  qredeu  11789  divgcdcoprm0  11793  cncongrcoprm  11798  prmind2  11812  isprm6  11836  sqrt2irr  11851  oddpwdclemodd  11861  divnumden  11885  divdenle  11886  nn0gcdsq  11889  hashgcdlem  11914  dvexp  12858
  Copyright terms: Public domain W3C validator