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

Theorem nnre 11637
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 11634 . 2 ℕ ⊆ ℝ
21sseli 3961 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 10528  cn 11630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-i2m1 10597  ax-1ne0 10598  ax-rrecex 10601  ax-cnre 10602
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-om 7573  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-nn 11631
This theorem is referenced by:  nnrei  11639  nnmulcl  11653  nn2ge  11656  nnge1  11657  nngt1ne1  11658  nnle1eq1  11659  nngt0  11660  nnnlt1  11661  nnnle0  11662  nndivre  11670  nnrecgt0  11672  nnsub  11673  nnunb  11885  arch  11886  nnrecl  11887  bndndx  11888  0mnnnnn0  11921  nnnegz  11976  elnnz  11983  elz2  11991  nnssz  11994  gtndiv  12051  prime  12055  btwnz  12076  indstr  12308  qre  12345  elpq  12366  elpqb  12367  rpnnen1lem2  12368  rpnnen1lem1  12369  rpnnen1lem3  12370  rpnnen1lem5  12372  nnrp  12392  nnledivrp  12493  qbtwnre  12584  elfzo0le  13073  fzonmapblen  13075  fzo1fzo0n0  13080  ubmelfzo  13094  fzonn0p1p1  13108  ubmelm1fzo  13125  subfzo0  13151  adddivflid  13180  flltdivnn0lt  13195  quoremz  13215  quoremnn0ALT  13217  intfracq  13219  fldiv  13220  modmulnn  13249  m1modnnsub1  13277  addmodid  13279  modifeq2int  13293  modaddmodup  13294  modaddmodlo  13295  modfzo0difsn  13303  modsumfzodifsn  13304  addmodlteq  13306  nnlesq  13560  digit2  13589  digit1  13590  expnngt1  13594  facdiv  13639  facndiv  13640  faclbnd  13642  faclbnd3  13644  faclbnd4lem4  13648  faclbnd5  13650  bcval5  13670  seqcoll  13814  ccatval21sw  13931  cshwidxmod  14157  cshwidxm1  14161  repswcshw  14166  isercolllem1  15013  harmonic  15206  efaddlem  15438  rpnnen2lem9  15567  rpnnen2lem12  15570  sqrt2irr  15594  nndivdvds  15608  dvdsle  15652  fzm1ndvds  15664  nno  15725  nnoddm1d2  15729  divalg2  15748  divalgmod  15749  ndvdsadd  15753  modgcd  15872  gcdmultipleOLD  15892  gcdmultiplezOLD  15893  gcdzeq  15894  sqgcd  15901  dvdssqlem  15902  lcmgcdlem  15942  lcmf  15969  coprmgcdb  15985  qredeq  15993  qredeu  15994  isprm3  16019  ge2nprmge4  16037  prmdvdsfz  16041  isprm5  16043  ncoprmlnprm  16060  divdenle  16081  phibndlem  16099  eulerthlem2  16111  hashgcdlem  16117  oddprm  16139  pythagtriplem10  16149  pythagtriplem12  16155  pythagtriplem14  16157  pythagtriplem16  16159  pythagtriplem19  16162  pclem  16167  pc2dvds  16207  pcmpt  16220  fldivp1  16225  pcbc  16228  infpnlem1  16238  infpn2  16241  prmreclem1  16244  prmreclem3  16246  vdwlem3  16311  ram0  16350  prmgaplem4  16382  prmgaplem7  16385  cshwshashlem1  16421  cshwshashlem2  16422  setsstruct2  16513  mulgnegnn  18230  mulgmodid  18258  odmodnn0  18660  gexdvds  18701  sylow3lem6  18749  prmirredlem  20632  znidomb  20700  chfacfisf  21454  chfacfisfcpmat  21455  chfacffsupp  21456  chfacfscmul0  21458  chfacfpmmul0  21462  ovolunlem1a  24089  ovoliunlem2  24096  ovolicc2lem3  24112  ovolicc2lem4  24113  iundisj2  24142  dyadss  24187  volsup2  24198  volivth  24200  vitali  24206  ismbf3d  24247  mbfi1fseqlem3  24310  mbfi1fseqlem4  24311  mbfi1fseqlem5  24312  itg2seq  24335  itg2gt0  24353  itg2cnlem1  24354  plyeq0lem  24792  dgreq0  24847  dgrcolem2  24856  elqaalem2  24901  elqaalem3  24902  logtayllem  25234  leibpi  25512  birthdaylem3  25523  zetacvg  25584  eldmgm  25591  basellem1  25650  basellem2  25651  basellem3  25652  basellem6  25655  basellem9  25658  prmorcht  25747  dvdsflsumcom  25757  muinv  25762  vmalelog  25773  chtublem  25779  logfac2  25785  logfaclbnd  25790  pcbcctr  25844  bcmono  25845  bposlem1  25852  bposlem5  25856  bposlem6  25857  bpos  25861  lgsval4a  25887  gausslemma2dlem0c  25926  gausslemma2dlem0d  25927  gausslemma2dlem1a  25933  gausslemma2dlem2  25935  gausslemma2dlem3  25936  gausslemma2dlem5  25939  lgsquadlem1  25948  lgsquadlem2  25949  2lgslem1a1  25957  2sqreunnlem1  26017  2sqreunnltlem  26018  dchrisum0re  26081  dchrisum0lem1  26084  logdivbnd  26124  ostth2lem1  26186  ostth2lem3  26203  pthdlem2lem  27540  crctcshwlkn0lem1  27580  crctcshwlkn0lem3  27582  crctcshwlkn0lem4  27583  crctcshwlkn0lem5  27584  crctcshwlkn0lem6  27585  crctcshwlkn0lem7  27586  crctcshwlkn0  27591  clwlkclwwlkf1lem2  27775  clwwisshclwwslem  27784  clwwlkel  27817  clwwlkf  27818  clwwlkf1  27820  wwlksext2clwwlk  27828  wwlksubclwwlk  27829  eucrctshift  28014  eucrct2eupth  28016  numclwlk2lem2f  28148  nmounbseqi  28546  nmounbseqiALT  28547  nmobndseqi  28548  nmobndseqiALT  28549  ubthlem1  28639  minvecolem3  28645  lnconi  29802  iundisj2f  30332  nnmulge  30466  xrsmulgzz  30658  esumpmono  31326  eulerpartlemb  31614  fibp1  31647  subfaclim  32423  subfacval3  32424  snmlff  32564  fz0n  32950  bcprod  32958  nn0prpwlem  33658  nn0prpw  33659  nndivsub  33793  nndivlub  33794  knoppcnlem2  33821  knoppcnlem4  33823  knoppcnlem10  33829  knoppndvlem11  33849  knoppndvlem12  33850  knoppndvlem14  33852  poimirlem13  34887  poimirlem14  34888  poimirlem31  34905  poimirlem32  34906  mblfinlem2  34912  fzmul  34998  incsequz  35005  nnubfi  35007  nninfnub  35008  nnadddir  39143  nnmul1com  39144  nn0rppwr  39162  nn0expgcd  39164  irrapxlem1  39399  irrapxlem2  39400  pellexlem1  39406  pellexlem5  39410  pellqrex  39456  monotoddzzfi  39519  jm2.24nn  39536  congabseq  39551  acongrep  39557  acongeq  39560  expdiophlem1  39598  idomrootle  39775  idomodle  39776  relexpmulnn  40034  prmunb2  40623  hashnzfzclim  40634  fmuldfeq  41843  sumnnodd  41890  stoweidlem14  42279  stoweidlem17  42282  stoweidlem20  42285  stoweidlem49  42314  stoweidlem60  42325  wallispilem3  42332  wallispilem4  42333  wallispilem5  42334  wallispi  42335  wallispi2lem1  42336  wallispi2lem2  42337  stirlinglem1  42339  stirlinglem3  42341  stirlinglem4  42342  stirlinglem6  42344  stirlinglem7  42345  stirlinglem10  42348  stirlinglem11  42349  stirlinglem12  42350  stirlinglem13  42351  stirlingr  42355  dirker2re  42357  dirkerval2  42359  dirkerre  42360  dirkertrigeqlem1  42363  fourierdlem66  42437  fourierdlem73  42444  fourierdlem83  42454  fourierdlem87  42458  fourierdlem103  42474  fourierdlem104  42475  fourierdlem111  42482  fouriersw  42496  etransclem24  42523  sge0rpcpnf  42683  hoicvr  42810  hoicvrrex  42818  vonioolem2  42943  vonicclem2  42946  subsubelfzo0  43506  fmtnodvds  43686  2pwp1prm  43731  lighneallem2  43751  nn0oALTV  43841  nneven  43843  nnsum4primes4  43934  nnsum4primesprm  43936  nnsum4primesgbe  43938  nnsum4primesle9  43940  bgoldbachlt  43958  tgoldbach  43962  altgsumbcALT  44381  modn0mul  44560  m1modmmod  44561  difmodm1lt  44562  nnlog2ge0lt1  44606  logbpw2m1  44607  blennn  44615  blennnelnn  44616  nnpw2pmod  44623  nnolog2flm1  44630  digvalnn0  44639  dignn0fr  44641  dignn0ldlem  44642  dignnld  44643  dig2nn1st  44645
  Copyright terms: Public domain W3C validator