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

Theorem nncn 8748
Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
Assertion
Ref Expression
nncn (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)

Proof of Theorem nncn
StepHypRef Expression
1 nnsscn 8745 . 2 ℕ ⊆ ℂ
21sseli 3094 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1481  cc 7638  cn 8740
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4050  ax-cnex 7731  ax-resscn 7732  ax-1re 7734  ax-addrcl 7737
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2689  df-in 3078  df-ss 3085  df-int 3776  df-inn 8741
This theorem is referenced by:  nn1m1nn  8758  nn1suc  8759  nnaddcl  8760  nnmulcl  8761  nnsub  8779  nndiv  8781  nndivtr  8782  nnnn0addcl  9027  nn0nnaddcl  9028  elnnnn0  9040  nnnegz  9077  zaddcllempos  9111  zaddcllemneg  9113  nnaddm1cl  9135  elz2  9142  zdiv  9159  zdivadd  9160  zdivmul  9161  nneoor  9173  nneo  9174  divfnzn  9436  qmulz  9438  qaddcl  9450  qnegcl  9451  qmulcl  9452  qreccl  9457  nnledivrp  9579  nn0ledivnn  9580  fseq1m1p1  9902  nnsplit  9941  ubmelm1fzo  10030  subfzo0  10046  flqdiv  10121  addmodidr  10173  modfzo0difsn  10195  nn0ennn  10233  expnegap0  10328  expm1t  10348  nnsqcl  10389  nnlesq  10423  facdiv  10512  facndiv  10513  faclbnd  10515  bcn1  10532  bcn2m1  10543  arisum  11295  arisum2  11296  expcnvap0  11299  mertenslem2  11333  ef0lem  11394  efexp  11416  nndivides  11527  modmulconst  11552  dvdsflip  11576  nn0enne  11626  nno  11630  divalgmod  11651  ndvdsadd  11655  modgcd  11706  gcddiv  11734  gcdmultiple  11735  gcdmultiplez  11736  rpmulgcd  11741  rplpwr  11742  sqgcd  11744  lcmgcdlem  11785  qredeq  11804  qredeu  11805  divgcdcoprm0  11809  cncongrcoprm  11814  prmind2  11828  isprm6  11852  sqrt2irr  11867  oddpwdclemodd  11877  divnumden  11901  divdenle  11902  nn0gcdsq  11905  hashgcdlem  11930  dvexp  12874  rpcxproot  13033  logbgcd1irr  13083
  Copyright terms: Public domain W3C validator