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

Theorem nncn 8365
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 8362 . 2  |-  NN  C_  CC
21sseli 3010 1  |-  ( A  e.  NN  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1436   CCcc 7292   NNcn 8357
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3932  ax-cnex 7380  ax-resscn 7381  ax-1re 7383  ax-addrcl 7386
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-v 2617  df-in 2994  df-ss 3001  df-int 3672  df-inn 8358
This theorem is referenced by:  nn1m1nn  8375  nn1suc  8376  nnaddcl  8377  nnmulcl  8378  nnsub  8395  nndiv  8397  nndivtr  8398  nnnn0addcl  8636  nn0nnaddcl  8637  elnnnn0  8649  nnnegz  8686  zaddcllempos  8720  zaddcllemneg  8722  nnaddm1cl  8744  elz2  8751  zdiv  8767  zdivadd  8768  zdivmul  8769  nneoor  8781  nneo  8782  divfnzn  9038  qmulz  9040  qaddcl  9052  qnegcl  9053  qmulcl  9054  qreccl  9059  nnledivrp  9169  nn0ledivnn  9170  fseq1m1p1  9439  nnsplit  9476  ubmelm1fzo  9565  subfzo0  9581  flqdiv  9656  addmodidr  9708  modfzo0difsn  9730  nn0ennn  9768  expnegap0  9862  expm1t  9882  nnsqcl  9923  nnlesq  9956  facdiv  10043  facndiv  10044  faclbnd  10046  bcn1  10063  bcn2m1  10074  nndivides  10685  modmulconst  10710  dvdsflip  10734  nn0enne  10784  nno  10788  divalgmod  10809  ndvdsadd  10813  modgcd  10864  gcddiv  10890  gcdmultiple  10891  gcdmultiplez  10892  rpmulgcd  10897  rplpwr  10898  sqgcd  10900  lcmgcdlem  10941  qredeq  10960  qredeu  10961  divgcdcoprm0  10965  cncongrcoprm  10970  prmind2  10984  isprm6  11008  sqrt2irr  11023  oddpwdclemodd  11032  divnumden  11056  divdenle  11057  nn0gcdsq  11060  hashgcdlem  11085
  Copyright terms: Public domain W3C validator