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

Theorem nnre 10871
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
Assertion
Ref Expression
nnre (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Proof of Theorem nnre
StepHypRef Expression
1 nnssre 10868 . 2 ℕ ⊆ ℝ
21sseli 3560 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cr 9788  cn 10864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-i2m1 9857  ax-1ne0 9858  ax-rrecex 9861  ax-cnre 9862
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-ov 6527  df-om 6932  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-nn 10865
This theorem is referenced by:  nnrei  10873  nn2ge  10889  nnge1  10890  nngt1ne1  10891  nnle1eq1  10892  nngt0  10893  nnnlt1  10894  nnnle0  10895  nndivre  10900  nnrecgt0  10902  nnsub  10903  nnunb  11132  arch  11133  nnrecl  11134  bndndx  11135  0mnnnnn0  11169  nnnegz  11210  elnnz  11217  elz2  11224  gtndiv  11283  prime  11287  btwnz  11308  indstr  11585  qre  11622  rpnnen1lem2  11643  rpnnen1lem1  11644  rpnnen1lem3  11645  rpnnen1lem5  11647  rpnnen1lem1OLD  11650  rpnnen1lem3OLD  11651  rpnnen1lem5OLD  11653  nnrp  11671  nnledivrp  11769  qbtwnre  11860  elfzo0le  12331  fzonmapblen  12333  fzo1fzo0n0  12338  ubmelfzo  12352  fzonn0p1p1  12365  elfzom1p1elfzo  12366  ubmelm1fzo  12382  subfzo0  12404  adddivflid  12433  flltdivnn0lt  12448  quoremz  12468  quoremnn0ALT  12470  intfracq  12472  fldiv  12473  modmulnn  12502  m1modnnsub1  12530  addmodid  12532  modifeq2int  12546  modaddmodup  12547  modaddmodlo  12548  modfzo0difsn  12556  modsumfzodifsn  12557  addmodlteq  12559  nnlesq  12782  digit2  12811  digit1  12812  facdiv  12888  facndiv  12889  faclbnd  12891  faclbnd3  12893  faclbnd4lem4  12897  faclbnd5  12899  bcval5  12919  seqcoll  13054  cshwidxmod  13343  cshwidxm1  13347  repswcshw  13352  isercolllem1  14186  harmonic  14373  efaddlem  14605  rpnnen2lem9  14733  rpnnen2lem12  14736  sqrt2irr  14760  nndivdvds  14770  dvdsle  14813  fzm1ndvds  14825  nno  14879  nnoddm1d2  14883  divalg2  14909  divalgmod  14910  divalgmodOLD  14911  ndvdsadd  14915  modgcd  15034  gcdmultiple  15050  gcdmultiplez  15051  gcdzeq  15052  sqgcd  15059  dvdssqlem  15060  lcmgcdlem  15100  lcmf  15127  coprmgcdb  15143  qredeq  15152  qredeu  15153  isprm3  15177  prmdvdsfz  15198  isprm5  15200  ncoprmlnprm  15217  divdenle  15238  phibndlem  15256  eulerthlem2  15268  hashgcdlem  15274  oddprm  15296  pythagtriplem10  15306  pythagtriplem12  15312  pythagtriplem14  15314  pythagtriplem16  15316  pythagtriplem19  15319  pclem  15324  pc2dvds  15364  pcmpt  15377  fldivp1  15382  pcbc  15385  infpnlem1  15395  infpn2  15398  prmreclem1  15401  prmreclem3  15403  vdwlem3  15468  ram0  15507  prmgaplem4  15539  prmgaplem7  15542  cshwshashlem1  15583  cshwshashlem2  15584  setsstruct  15670  mulgnegnn  17317  mulgmodid  17347  odmodnn0  17725  gexdvds  17765  sylow3lem6  17813  prmirredlem  19602  znidomb  19671  chfacfisf  20417  chfacfisfcpmat  20418  chfacffsupp  20419  chfacfscmul0  20421  chfacfpmmul0  20425  ovolunlem1a  22985  ovoliunlem2  22992  ovolicc2lem3  23008  ovolicc2lem4  23009  iundisj2  23038  dyadss  23082  volsup2  23093  volivth  23095  vitali  23102  ismbf3d  23141  mbfi1fseqlem3  23204  mbfi1fseqlem4  23205  mbfi1fseqlem5  23206  itg2seq  23229  itg2gt0  23247  itg2cnlem1  23248  plyeq0lem  23684  dgreq0  23739  dgrcolem2  23748  elqaalem2  23793  elqaalem3  23794  logtayllem  24119  leibpi  24383  birthdaylem3  24394  zetacvg  24455  eldmgm  24462  basellem1  24521  basellem2  24522  basellem3  24523  basellem6  24526  basellem9  24529  prmorcht  24618  dvdsflsumcom  24628  muinv  24633  vmalelog  24644  chtublem  24650  logfac2  24656  logfaclbnd  24661  pcbcctr  24715  bcmono  24716  bposlem1  24723  bposlem5  24727  bposlem6  24728  bpos  24732  lgsval4a  24758  gausslemma2dlem0c  24797  gausslemma2dlem0d  24798  gausslemma2dlem1a  24804  gausslemma2dlem2  24806  gausslemma2dlem3  24807  gausslemma2dlem5  24810  lgsquadlem1  24819  lgsquadlem2  24820  2lgslem1a1  24828  dchrisum0re  24916  dchrisum0lem1  24919  logdivbnd  24959  ostth2lem1  25021  ostth2lem3  25038  clwwlkel  26084  clwwlkf  26085  clwwlkf1  26087  wwlkext2clwwlk  26094  wwlksubclwwlk  26095  clwwisshclwwlem  26097  numclwlk2lem2f  26393  nmounbseqi  26819  nmounbseqiALT  26820  nmobndseqi  26821  nmobndseqiALT  26822  ubthlem1  26913  minvecolem3  26919  lnconi  28079  iundisj2f  28588  xrsmulgzz  28812  esumpmono  29271  eulerpartlemb  29560  fibp1  29593  subfaclim  30227  subfacval3  30228  snmlff  30368  fz0n  30672  bcprod  30680  nn0prpwlem  31290  nn0prpw  31291  nndivsub  31429  nndivlub  31430  knoppcnlem2  31457  knoppcnlem4  31459  knoppcnlem10  31465  knoppndvlem11  31486  knoppndvlem12  31487  knoppndvlem14  31489  poimirlem13  32392  poimirlem14  32393  poimirlem31  32410  poimirlem32  32411  mblfinlem2  32417  fzmul  32507  incsequz  32514  nnubfi  32516  nninfnub  32517  irrapxlem1  36204  irrapxlem2  36205  pellexlem1  36211  pellexlem5  36215  pellqrex  36261  monotoddzzfi  36325  jm2.24nn  36344  congabseq  36359  acongrep  36365  acongeq  36368  expdiophlem1  36406  idomrootle  36592  idomodle  36593  relexpmulnn  36820  prmunb2  37332  hashnzfzclim  37343  fmuldfeq  38451  sumnnodd  38498  stoweidlem14  38708  stoweidlem17  38711  stoweidlem20  38714  stoweidlem49  38743  stoweidlem60  38754  wallispilem3  38761  wallispilem4  38762  wallispilem5  38763  wallispi  38764  wallispi2lem1  38765  wallispi2lem2  38766  stirlinglem1  38768  stirlinglem3  38770  stirlinglem4  38771  stirlinglem6  38773  stirlinglem7  38774  stirlinglem10  38777  stirlinglem11  38778  stirlinglem12  38779  stirlinglem13  38780  stirlingr  38784  dirker2re  38786  dirkerval2  38788  dirkerre  38789  dirkertrigeqlem1  38792  fourierdlem66  38866  fourierdlem73  38873  fourierdlem83  38883  fourierdlem87  38887  fourierdlem103  38903  fourierdlem104  38904  fourierdlem111  38911  fouriersw  38925  etransclem24  38952  sge0rpcpnf  39115  hoicvr  39239  hoicvrrex  39247  vonioolem2  39373  vonicclem2  39376  fmtnodvds  39796  2pwp1prm  39843  lighneallem2  39863  nn0oALTV  39947  nnsum4primes4  40007  nnsum4primesprm  40009  nnsum4primesgbe  40011  nnsum4primesle9  40013  bgoldbachlt  40029  tgoldbach  40034  bgoldbachltOLD  40036  tgoldbachOLD  40041  subsubelfzo0  40183  pthdlem2lem  40972  crctcsh1wlkn0lem1  41012  crctcsh1wlkn0lem3  41014  crctcsh1wlkn0lem4  41015  crctcsh1wlkn0lem5  41016  crctcsh1wlkn0lem6  41017  crctcsh1wlkn0lem7  41018  crctcsh1wlkn0  41023  clwwlksel  41220  clwwlksf  41221  clwwlksf1  41223  wwlksext2clwwlk  41230  wwlksubclwwlks  41231  clwwisshclwwslem  41233  eucrctshift  41410  eucrct2eupth  41412  av-numclwlk2lem2f  41532  altgsumbcALT  41923  modn0mul  42108  m1modmmod  42109  difmodm1lt  42110  nnlog2ge0lt1  42157  logbpw2m1  42158  blennn  42166  blennnelnn  42167  nnpw2pmod  42174  nnolog2flm1  42181  digvalnn0  42190  dignn0fr  42192  dignn0ldlem  42193  dignnld  42194  dig2nn1st  42196
  Copyright terms: Public domain W3C validator