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

Theorem nnre 11024
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 11021 . 2 ℕ ⊆ ℝ
21sseli 3597 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  cr 9932  cn 11017
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-i2m1 10001  ax-1ne0 10002  ax-rrecex 10005  ax-cnre 10006
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-ov 6650  df-om 7063  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-nn 11018
This theorem is referenced by:  nnrei  11026  nn2ge  11042  nnge1  11043  nngt1ne1  11044  nnle1eq1  11045  nngt0  11046  nnnlt1  11047  nnnle0  11048  nndivre  11053  nnrecgt0  11055  nnsub  11056  nnunb  11285  arch  11286  nnrecl  11287  bndndx  11288  0mnnnnn0  11322  nnnegz  11377  elnnz  11384  elz2  11391  gtndiv  11451  prime  11455  btwnz  11476  indstr  11753  qre  11790  rpnnen1lem2  11811  rpnnen1lem1  11812  rpnnen1lem3  11813  rpnnen1lem5  11815  rpnnen1lem1OLD  11818  rpnnen1lem3OLD  11819  rpnnen1lem5OLD  11821  nnrp  11839  nnledivrp  11937  qbtwnre  12027  elfzo0le  12507  fzonmapblen  12509  fzo1fzo0n0  12514  ubmelfzo  12528  fzonn0p1p1  12542  elfzom1p1elfzo  12543  ubmelm1fzo  12560  subfzo0  12585  adddivflid  12614  flltdivnn0lt  12629  quoremz  12649  quoremnn0ALT  12651  intfracq  12653  fldiv  12654  modmulnn  12683  m1modnnsub1  12711  addmodid  12713  modifeq2int  12727  modaddmodup  12728  modaddmodlo  12729  modfzo0difsn  12737  modsumfzodifsn  12738  addmodlteq  12740  nnlesq  12963  digit2  12992  digit1  12993  facdiv  13069  facndiv  13070  faclbnd  13072  faclbnd3  13074  faclbnd4lem4  13078  faclbnd5  13080  bcval5  13100  seqcoll  13243  cshwidxmod  13543  cshwidxm1  13547  repswcshw  13552  isercolllem1  14389  harmonic  14585  efaddlem  14817  rpnnen2lem9  14945  rpnnen2lem12  14948  sqrt2irr  14973  nndivdvds  14983  dvdsle  15026  fzm1ndvds  15038  nno  15092  nnoddm1d2  15096  divalg2  15122  divalgmod  15123  divalgmodOLD  15124  ndvdsadd  15128  modgcd  15247  gcdmultiple  15263  gcdmultiplez  15264  gcdzeq  15265  sqgcd  15272  dvdssqlem  15273  lcmgcdlem  15313  lcmf  15340  coprmgcdb  15356  qredeq  15365  qredeu  15366  isprm3  15390  prmdvdsfz  15411  isprm5  15413  ncoprmlnprm  15430  divdenle  15451  phibndlem  15469  eulerthlem2  15481  hashgcdlem  15487  oddprm  15509  pythagtriplem10  15519  pythagtriplem12  15525  pythagtriplem14  15527  pythagtriplem16  15529  pythagtriplem19  15532  pclem  15537  pc2dvds  15577  pcmpt  15590  fldivp1  15595  pcbc  15598  infpnlem1  15608  infpn2  15611  prmreclem1  15614  prmreclem3  15616  vdwlem3  15681  ram0  15720  prmgaplem4  15752  prmgaplem7  15755  cshwshashlem1  15796  cshwshashlem2  15797  setsstruct2  15890  setsstructOLD  15893  mulgnegnn  17545  mulgmodid  17575  odmodnn0  17953  gexdvds  17993  sylow3lem6  18041  prmirredlem  19835  znidomb  19904  chfacfisf  20653  chfacfisfcpmat  20654  chfacffsupp  20655  chfacfscmul0  20657  chfacfpmmul0  20661  ovolunlem1a  23258  ovoliunlem2  23265  ovolicc2lem3  23281  ovolicc2lem4  23282  iundisj2  23311  dyadss  23356  volsup2  23367  volivth  23369  vitali  23376  ismbf3d  23415  mbfi1fseqlem3  23478  mbfi1fseqlem4  23479  mbfi1fseqlem5  23480  itg2seq  23503  itg2gt0  23521  itg2cnlem1  23522  plyeq0lem  23960  dgreq0  24015  dgrcolem2  24024  elqaalem2  24069  elqaalem3  24070  logtayllem  24399  leibpi  24663  birthdaylem3  24674  zetacvg  24735  eldmgm  24742  basellem1  24801  basellem2  24802  basellem3  24803  basellem6  24806  basellem9  24809  prmorcht  24898  dvdsflsumcom  24908  muinv  24913  vmalelog  24924  chtublem  24930  logfac2  24936  logfaclbnd  24941  pcbcctr  24995  bcmono  24996  bposlem1  25003  bposlem5  25007  bposlem6  25008  bpos  25012  lgsval4a  25038  gausslemma2dlem0c  25077  gausslemma2dlem0d  25078  gausslemma2dlem1a  25084  gausslemma2dlem2  25086  gausslemma2dlem3  25087  gausslemma2dlem5  25090  lgsquadlem1  25099  lgsquadlem2  25100  2lgslem1a1  25108  dchrisum0re  25196  dchrisum0lem1  25199  logdivbnd  25239  ostth2lem1  25301  ostth2lem3  25318  pthdlem2lem  26657  crctcshwlkn0lem1  26696  crctcshwlkn0lem3  26698  crctcshwlkn0lem4  26699  crctcshwlkn0lem5  26700  crctcshwlkn0lem6  26701  crctcshwlkn0lem7  26702  crctcshwlkn0  26707  clwwlksel  26907  clwwlksf  26908  clwwlksf1  26910  wwlksext2clwwlk  26917  wwlksubclwwlks  26918  clwwisshclwwslem  26920  eucrctshift  27096  eucrct2eupth  27098  numclwlk2lem2f  27220  nmounbseqi  27616  nmounbseqiALT  27617  nmobndseqi  27618  nmobndseqiALT  27619  ubthlem1  27710  minvecolem3  27716  lnconi  28876  iundisj2f  29387  nnmulge  29500  xrsmulgzz  29663  esumpmono  30126  eulerpartlemb  30415  fibp1  30448  subfaclim  31155  subfacval3  31156  snmlff  31296  fz0n  31602  bcprod  31610  nn0prpwlem  32301  nn0prpw  32302  nndivsub  32440  nndivlub  32441  knoppcnlem2  32468  knoppcnlem4  32470  knoppcnlem10  32476  knoppndvlem11  32497  knoppndvlem12  32498  knoppndvlem14  32500  poimirlem13  33402  poimirlem14  33403  poimirlem31  33420  poimirlem32  33421  mblfinlem2  33427  fzmul  33517  incsequz  33524  nnubfi  33526  nninfnub  33527  irrapxlem1  37212  irrapxlem2  37213  pellexlem1  37219  pellexlem5  37223  pellqrex  37269  monotoddzzfi  37333  jm2.24nn  37352  congabseq  37367  acongrep  37373  acongeq  37376  expdiophlem1  37414  idomrootle  37599  idomodle  37600  relexpmulnn  37827  prmunb2  38336  hashnzfzclim  38347  fmuldfeq  39621  sumnnodd  39668  stoweidlem14  40000  stoweidlem17  40003  stoweidlem20  40006  stoweidlem49  40035  stoweidlem60  40046  wallispilem3  40053  wallispilem4  40054  wallispilem5  40055  wallispi  40056  wallispi2lem1  40057  wallispi2lem2  40058  stirlinglem1  40060  stirlinglem3  40062  stirlinglem4  40063  stirlinglem6  40065  stirlinglem7  40066  stirlinglem10  40069  stirlinglem11  40070  stirlinglem12  40071  stirlinglem13  40072  stirlingr  40076  dirker2re  40078  dirkerval2  40080  dirkerre  40081  dirkertrigeqlem1  40084  fourierdlem66  40158  fourierdlem73  40165  fourierdlem83  40175  fourierdlem87  40179  fourierdlem103  40195  fourierdlem104  40196  fourierdlem111  40203  fouriersw  40217  etransclem24  40244  sge0rpcpnf  40407  hoicvr  40531  hoicvrrex  40539  vonioolem2  40664  vonicclem2  40667  subsubelfzo0  41105  fmtnodvds  41227  2pwp1prm  41274  lighneallem2  41294  nn0oALTV  41378  nnsum4primes4  41448  nnsum4primesprm  41450  nnsum4primesgbe  41452  nnsum4primesle9  41454  bgoldbachlt  41472  tgoldbach  41476  bgoldbachltOLD  41478  tgoldbachOLD  41483  altgsumbcALT  41902  modn0mul  42086  m1modmmod  42087  difmodm1lt  42088  nnlog2ge0lt1  42131  logbpw2m1  42132  blennn  42140  blennnelnn  42141  nnpw2pmod  42148  nnolog2flm1  42155  digvalnn0  42164  dignn0fr  42166  dignn0ldlem  42167  dignnld  42168  dig2nn1st  42170
  Copyright terms: Public domain W3C validator