MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnre Structured version   Unicode version

Theorem nnre 10439
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
Assertion
Ref Expression
nnre  |-  ( A  e.  NN  ->  A  e.  RR )

Proof of Theorem nnre
StepHypRef Expression
1 nnssre 10436 . 2  |-  NN  C_  RR
21sseli 3459 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   RRcr 9391   NNcn 10432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-i2m1 9460  ax-1ne0 9461  ax-rrecex 9464  ax-cnre 9465
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-om 6586  df-recs 6941  df-rdg 6975  df-nn 10433
This theorem is referenced by:  nnrei  10441  nn2ge  10457  nnge1  10458  nngt1ne1  10459  nnle1eq1  10460  nngt0  10461  nnnlt1  10462  nndivre  10467  nnrecgt0  10469  nnsub  10470  nnunb  10685  arch  10686  nnrecl  10687  bndndx  10688  0mnnnnn0  10722  nnnegz  10759  elnnz  10766  elz2  10773  gtndiv  10829  prime  10832  btwnz  10854  indstr  11033  qre  11068  rpnnen1lem1  11089  rpnnen1lem2  11090  rpnnen1lem3  11091  rpnnen1lem5  11093  nnrp  11110  qbtwnre  11279  fzo1fzo0n0  11704  elfzo0le  11706  fzonmapblen  11708  ubmelfzo  11719  ubmelm1fzo  11739  flltdivnn0lt  11793  quoremz  11810  quoremnn0ALT  11812  intfracq  11814  fldiv  11815  modmulnn  11841  modidmul0  11850  addmodid  11864  modifeq2int  11877  modaddmodup  11878  modaddmodlo  11879  nnlesq  12085  digit2  12113  digit1  12114  facdiv  12179  facndiv  12180  faclbnd  12182  faclbnd3  12184  faclbnd4lem4  12188  faclbnd5  12190  bcval5  12210  seqcoll  12333  lswcl  12387  lswccatn0lsw  12404  swrdn0  12441  cshwidxmod  12557  cshwidxm1  12560  repswcshw  12563  isercolllem1  13259  harmonic  13438  efaddlem  13495  rpnnen2lem9  13622  rpnnen2  13625  sqr2irr  13648  nndivdvds  13658  dvdsle  13695  dvdseq  13697  fzm1ndvds  13702  divalg2  13726  divalgmod  13727  ndvdsadd  13729  modgcd  13837  gcdmultiple  13851  gcdmultiplez  13852  gcdeq  13853  sqgcd  13859  dvdssqlem  13860  isprm3  13889  qredeq  13909  qredeu  13910  isprm5  13915  divdenle  13944  phibndlem  13962  eulerthlem2  13974  oddprm  13999  pythagtriplem10  14004  pythagtriplem12  14010  pythagtriplem14  14012  pythagtriplem16  14014  pythagtriplem19  14017  pclem  14022  pc2dvds  14062  pcmpt  14071  fldivp1  14076  pcbc  14079  infpnlem1  14088  infpn2  14091  prmreclem1  14094  prmreclem3  14096  vdwlem3  14161  ram0  14200  cshwshashlem1  14239  cshwshashlem2  14240  mulgnegnn  15755  odmodnn0  16163  gexdvds  16203  sylow3lem6  16251  prmirredlem  18041  prmirredlemOLD  18044  znidomb  18118  ovolunlem1a  21110  ovoliunlem2  21117  ovolicc2lem3  21133  ovolicc2lem4  21134  iundisj2  21162  dyadss  21206  volsup2  21217  volivth  21219  vitali  21225  ismbf3d  21264  mbfi1fseqlem3  21327  mbfi1fseqlem4  21328  mbfi1fseqlem5  21329  itg2seq  21352  itg2gt0  21370  itg2cnlem1  21371  plyeq0lem  21810  dgreq0  21864  dgrcolem2  21873  elqaalem2  21918  elqaalem3  21919  logtayllem  22236  leibpi  22469  birthdaylem3  22479  basellem1  22550  basellem2  22551  basellem3  22552  basellem6  22555  basellem9  22558  prmorcht  22648  dvdsdivcl  22653  dvdsflsumcom  22660  muinv  22665  vmalelog  22676  chtublem  22682  logfac2  22688  logfaclbnd  22693  pcbcctr  22747  bcmono  22748  bposlem1  22755  bposlem5  22759  bposlem6  22760  bpos  22764  lgsval4a  22789  lgsquadlem1  22825  lgsquadlem2  22826  dchrisum0re  22894  dchrisum0lem1  22897  logdivbnd  22937  ostth2lem1  22999  ostth2lem3  23016  gxnn0neg  23901  gxmodid  23917  nmounbseqi  24328  nmounbseqiOLD  24329  nmobndseqi  24330  nmobndseqiOLD  24331  ubthlem1  24422  minvecolem3  24428  lnconi  25588  iundisj2f  26082  esumpmono  26672  eulerpartlemb  26894  fibp1  26927  zetacvg  27144  eldmgm  27151  subfaclim  27219  subfacval3  27220  snmlff  27361  fz0n  27532  nndivsub  28446  nndivlub  28447  mblfinlem2  28576  nn0prpwlem  28664  nn0prpw  28665  fzmul  28783  incsequz  28791  nnubfi  28793  nninfnub  28794  irrapxlem1  29310  irrapxlem2  29311  pellexlem1  29317  pellexlem5  29321  pellqrex  29367  monotoddzzfi  29430  jm2.24nn  29449  congabseq  29464  acongrep  29470  acongeq  29473  expdiophlem1  29517  idomrootle  29707  idomodle  29708  hashgcdlem  29712  fmuldfeq  29911  stoweidlem14  29956  stoweidlem17  29959  stoweidlem20  29962  stoweidlem49  29991  stoweidlem60  30002  wallispilem3  30009  wallispilem4  30010  wallispilem5  30011  wallispi  30012  wallispi2lem1  30013  wallispi2lem2  30014  stirlinglem1  30016  stirlinglem3  30018  stirlinglem4  30019  stirlinglem6  30021  stirlinglem7  30022  stirlinglem10  30025  stirlinglem11  30026  stirlinglem12  30027  stirlinglem13  30028  stirlingr  30032  subsubelfzo0  30357  elfzom1p1elfzo  30362  fzonn0p1p1  30363  clwwlkel  30602  clwwlkf  30603  clwwlkf1  30605  wwlkext2clwwlk  30612  wwlksubclwwlk  30613  clwwisshclwwlem  30617  numclwlk2lem2f  30843  altgsumbcALT  30897  chfacfisf  31325  chfacfisfcpmat  31326  chfacffsupp  31327  chfacfscmul0  31329  chfacfpmmul0  31333
  Copyright terms: Public domain W3C validator