Theorem nnre 10904

Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)

Assertion

Ref	Expression
nnre	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Proof of Theorem nnre

Step	Hyp	Ref	Expression
1		nnssre 10901	. 2 ⊢ ℕ ⊆ ℝ
2	1	sseli 3564	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1977  ℝcr 9814  ℕcn 10897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898

This theorem is referenced by:  nnrei  10906  nn2ge  10922  nnge1  10923  nngt1ne1  10924  nnle1eq1  10925  nngt0  10926  nnnlt1  10927  nnnle0  10928  nndivre  10933  nnrecgt0  10935  nnsub  10936  nnunb  11165  arch  11166  nnrecl  11167  bndndx  11168  0mnnnnn0  11202  nnnegz  11257  elnnz  11264  elz2  11271  gtndiv  11330  prime  11334  btwnz  11355  indstr  11632  qre  11669  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  nnrp  11718  nnledivrp  11816  qbtwnre  11904  elfzo0le  12379  fzonmapblen  12381  fzo1fzo0n0  12386  ubmelfzo  12400  fzonn0p1p1  12413  elfzom1p1elfzo  12414  ubmelm1fzo  12430  subfzo0  12452  adddivflid  12481  flltdivnn0lt  12496  quoremz  12516  quoremnn0ALT  12518  intfracq  12520  fldiv  12521  modmulnn  12550  m1modnnsub1  12578  addmodid  12580  modifeq2int  12594  modaddmodup  12595  modaddmodlo  12596  modfzo0difsn  12604  modsumfzodifsn  12605  addmodlteq  12607  nnlesq  12830  digit2  12859  digit1  12860  facdiv  12936  facndiv  12937  faclbnd  12939  faclbnd3  12941  faclbnd4lem4  12945  faclbnd5  12947  bcval5  12967  seqcoll  13105  cshwidxmod  13400  cshwidxm1  13404  repswcshw  13409  isercolllem1  14243  harmonic  14430  efaddlem  14662  rpnnen2lem9  14790  rpnnen2lem12  14793  sqrt2irr  14817  nndivdvds  14827  dvdsle  14870  fzm1ndvds  14882  nno  14936  nnoddm1d2  14940  divalg2  14966  divalgmod  14967  divalgmodOLD  14968  ndvdsadd  14972  modgcd  15091  gcdmultiple  15107  gcdmultiplez  15108  gcdzeq  15109  sqgcd  15116  dvdssqlem  15117  lcmgcdlem  15157  lcmf  15184  coprmgcdb  15200  qredeq  15209  qredeu  15210  isprm3  15234  prmdvdsfz  15255  isprm5  15257  ncoprmlnprm  15274  divdenle  15295  phibndlem  15313  eulerthlem2  15325  hashgcdlem  15331  oddprm  15353  pythagtriplem10  15363  pythagtriplem12  15369  pythagtriplem14  15371  pythagtriplem16  15373  pythagtriplem19  15376  pclem  15381  pc2dvds  15421  pcmpt  15434  fldivp1  15439  pcbc  15442  infpnlem1  15452  infpn2  15455  prmreclem1  15458  prmreclem3  15460  vdwlem3  15525  ram0  15564  prmgaplem4  15596  prmgaplem7  15599  cshwshashlem1  15640  cshwshashlem2  15641  setsstruct  15727  mulgnegnn  17374  mulgmodid  17404  odmodnn0  17782  gexdvds  17822  sylow3lem6  17870  prmirredlem  19660  znidomb  19729  chfacfisf  20478  chfacfisfcpmat  20479  chfacffsupp  20480  chfacfscmul0  20482  chfacfpmmul0  20486  ovolunlem1a  23071  ovoliunlem2  23078  ovolicc2lem3  23094  ovolicc2lem4  23095  iundisj2  23124  dyadss  23168  volsup2  23179  volivth  23181  vitali  23188  ismbf3d  23227  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  itg2seq  23315  itg2gt0  23333  itg2cnlem1  23334  plyeq0lem  23770  dgreq0  23825  dgrcolem2  23834  elqaalem2  23879  elqaalem3  23880  logtayllem  24205  leibpi  24469  birthdaylem3  24480  zetacvg  24541  eldmgm  24548  basellem1  24607  basellem2  24608  basellem3  24609  basellem6  24612  basellem9  24615  prmorcht  24704  dvdsflsumcom  24714  muinv  24719  vmalelog  24730  chtublem  24736  logfac2  24742  logfaclbnd  24747  pcbcctr  24801  bcmono  24802  bposlem1  24809  bposlem5  24813  bposlem6  24814  bpos  24818  lgsval4a  24844  gausslemma2dlem0c  24883  gausslemma2dlem0d  24884  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  gausslemma2dlem3  24893  gausslemma2dlem5  24896  lgsquadlem1  24905  lgsquadlem2  24906  2lgslem1a1  24914  dchrisum0re  25002  dchrisum0lem1  25005  logdivbnd  25045  ostth2lem1  25107  ostth2lem3  25124  clwwlkel  26321  clwwlkf  26322  clwwlkf1  26324  wwlkext2clwwlk  26331  wwlksubclwwlk  26332  clwwisshclwwlem  26334  numclwlk2lem2f  26630  nmounbseqi  27016  nmounbseqiALT  27017  nmobndseqi  27018  nmobndseqiALT  27019  ubthlem1  27110  minvecolem3  27116  lnconi  28276  iundisj2f  28785  xrsmulgzz  29009  esumpmono  29468  eulerpartlemb  29757  fibp1  29790  subfaclim  30424  subfacval3  30425  snmlff  30565  fz0n  30869  bcprod  30877  nn0prpwlem  31487  nn0prpw  31488  nndivsub  31626  nndivlub  31627  knoppcnlem2  31654  knoppcnlem4  31656  knoppcnlem10  31662  knoppndvlem11  31683  knoppndvlem12  31684  knoppndvlem14  31686  poimirlem13  32592  poimirlem14  32593  poimirlem31  32610  poimirlem32  32611  mblfinlem2  32617  fzmul  32707  incsequz  32714  nnubfi  32716  nninfnub  32717  irrapxlem1  36404  irrapxlem2  36405  pellexlem1  36411  pellexlem5  36415  pellqrex  36461  monotoddzzfi  36525  jm2.24nn  36544  congabseq  36559  acongrep  36565  acongeq  36568  expdiophlem1  36606  idomrootle  36792  idomodle  36793  relexpmulnn  37020  prmunb2  37532  hashnzfzclim  37543  fmuldfeq  38650  sumnnodd  38697  stoweidlem14  38907  stoweidlem17  38910  stoweidlem20  38913  stoweidlem49  38942  stoweidlem60  38953  wallispilem3  38960  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem1  38967  stirlinglem3  38969  stirlinglem4  38970  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlingr  38983  dirker2re  38985  dirkerval2  38987  dirkerre  38988  dirkertrigeqlem1  38991  fourierdlem66  39065  fourierdlem73  39072  fourierdlem83  39082  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fouriersw  39124  etransclem24  39151  sge0rpcpnf  39314  hoicvr  39438  hoicvrrex  39446  vonioolem2  39572  vonicclem2  39575  fmtnodvds  39994  2pwp1prm  40041  lighneallem2  40061  nn0oALTV  40145  nnsum4primes4  40205  nnsum4primesprm  40207  nnsum4primesgbe  40209  nnsum4primesle9  40211  bgoldbachlt  40227  tgoldbach  40232  bgoldbachltOLD  40234  tgoldbachOLD  40239  subsubelfzo0  40359  pthdlem2lem  40973  crctcsh1wlkn0lem1  41013  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem6  41018  crctcsh1wlkn0lem7  41019  crctcsh1wlkn0  41024  clwwlksel  41221  clwwlksf  41222  clwwlksf1  41224  wwlksext2clwwlk  41231  wwlksubclwwlks  41232  clwwisshclwwslem  41234  eucrctshift  41411  eucrct2eupth  41413  av-numclwlk2lem2f  41533  altgsumbcALT  41924  modn0mul  42109  m1modmmod  42110  difmodm1lt  42111  nnlog2ge0lt1  42158  logbpw2m1  42159  blennn  42167  blennnelnn  42168  nnpw2pmod  42175  nnolog2flm1  42182  digvalnn0  42191  dignn0fr  42193  dignn0ldlem  42194  dignnld  42195  dig2nn1st  42197