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

Theorem nncn 8696
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 8693 . 2  |-  NN  C_  CC
21sseli 3063 1  |-  ( A  e.  NN  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1465   CCcc 7586   NNcn 8688
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-cnex 7679  ax-resscn 7680  ax-1re 7682  ax-addrcl 7685
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-v 2662  df-in 3047  df-ss 3054  df-int 3742  df-inn 8689
This theorem is referenced by:  nn1m1nn  8706  nn1suc  8707  nnaddcl  8708  nnmulcl  8709  nnsub  8727  nndiv  8729  nndivtr  8730  nnnn0addcl  8975  nn0nnaddcl  8976  elnnnn0  8988  nnnegz  9025  zaddcllempos  9059  zaddcllemneg  9061  nnaddm1cl  9083  elz2  9090  zdiv  9107  zdivadd  9108  zdivmul  9109  nneoor  9121  nneo  9122  divfnzn  9381  qmulz  9383  qaddcl  9395  qnegcl  9396  qmulcl  9397  qreccl  9402  nnledivrp  9521  nn0ledivnn  9522  fseq1m1p1  9843  nnsplit  9882  ubmelm1fzo  9971  subfzo0  9987  flqdiv  10062  addmodidr  10114  modfzo0difsn  10136  nn0ennn  10174  expnegap0  10269  expm1t  10289  nnsqcl  10330  nnlesq  10364  facdiv  10452  facndiv  10453  faclbnd  10455  bcn1  10472  bcn2m1  10483  arisum  11235  arisum2  11236  expcnvap0  11239  mertenslem2  11273  ef0lem  11293  efexp  11315  nndivides  11427  modmulconst  11452  dvdsflip  11476  nn0enne  11526  nno  11530  divalgmod  11551  ndvdsadd  11555  modgcd  11606  gcddiv  11634  gcdmultiple  11635  gcdmultiplez  11636  rpmulgcd  11641  rplpwr  11642  sqgcd  11644  lcmgcdlem  11685  qredeq  11704  qredeu  11705  divgcdcoprm0  11709  cncongrcoprm  11714  prmind2  11728  isprm6  11752  sqrt2irr  11767  oddpwdclemodd  11777  divnumden  11801  divdenle  11802  nn0gcdsq  11805  hashgcdlem  11830  dvexp  12771
  Copyright terms: Public domain W3C validator