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

Theorem nncn 8692
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 8689 . 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 8684
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 8685
This theorem is referenced by:  nn1m1nn  8702  nn1suc  8703  nnaddcl  8704  nnmulcl  8705  nnsub  8723  nndiv  8725  nndivtr  8726  nnnn0addcl  8965  nn0nnaddcl  8966  elnnnn0  8978  nnnegz  9015  zaddcllempos  9049  zaddcllemneg  9051  nnaddm1cl  9073  elz2  9080  zdiv  9097  zdivadd  9098  zdivmul  9099  nneoor  9111  nneo  9112  divfnzn  9369  qmulz  9371  qaddcl  9383  qnegcl  9384  qmulcl  9385  qreccl  9390  nnledivrp  9508  nn0ledivnn  9509  fseq1m1p1  9830  nnsplit  9869  ubmelm1fzo  9958  subfzo0  9974  flqdiv  10049  addmodidr  10101  modfzo0difsn  10123  nn0ennn  10161  expnegap0  10256  expm1t  10276  nnsqcl  10317  nnlesq  10351  facdiv  10439  facndiv  10440  faclbnd  10442  bcn1  10459  bcn2m1  10470  arisum  11222  arisum2  11223  expcnvap0  11226  mertenslem2  11260  ef0lem  11280  efexp  11302  nndivides  11412  modmulconst  11437  dvdsflip  11461  nn0enne  11511  nno  11515  divalgmod  11536  ndvdsadd  11540  modgcd  11591  gcddiv  11619  gcdmultiple  11620  gcdmultiplez  11621  rpmulgcd  11626  rplpwr  11627  sqgcd  11629  lcmgcdlem  11670  qredeq  11689  qredeu  11690  divgcdcoprm0  11694  cncongrcoprm  11699  prmind2  11713  isprm6  11737  sqrt2irr  11752  oddpwdclemodd  11761  divnumden  11785  divdenle  11786  nn0gcdsq  11789  hashgcdlem  11814  dvexp  12755
  Copyright terms: Public domain W3C validator