Theorem nnre 12270

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 12267	. 2 ⊢ ℕ ⊆ ℝ
2	1	sseli 3990	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  ℕcn 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-nn 12264

This theorem is referenced by:  nnrei  12272  nnmulcl  12287  nn2ge  12290  nnge1  12291  nngt1ne1  12292  nnle1eq1  12293  nngt0  12294  nnnlt1  12295  nnnle0  12296  nndivre  12304  nnrecgt0  12306  nnsub  12307  nnunb  12519  arch  12520  nnrecl  12521  bndndx  12522  0mnnnnn0  12555  nnnegz  12613  elnnz  12620  elz2  12628  nnz  12631  gtndiv  12692  prime  12696  btwnz  12718  indstr  12955  qre  12992  elpq  13014  elpqb  13015  rpnnen1lem2  13016  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  nnrp  13043  nnledivrp  13144  qbtwnre  13237  elfzo0le  13739  fzonmapblen  13744  fzo1fzo0n0  13750  ubmelfzo  13765  fzonn0p1p1  13779  ubmelm1fzo  13798  subfzo0  13824  adddivflid  13854  flltdivnn0lt  13869  quoremz  13891  quoremnn0ALT  13893  intfracq  13895  fldiv  13896  modmulnn  13925  m1modnnsub1  13954  addmodid  13956  modifeq2int  13970  modaddmodup  13971  modaddmodlo  13972  modfzo0difsn  13980  modsumfzodifsn  13981  addmodlteq  13983  nnlesq  14240  digit2  14271  digit1  14272  expnngt1  14276  facdiv  14322  facndiv  14323  faclbnd  14325  faclbnd3  14327  faclbnd4lem4  14331  faclbnd5  14333  bcval5  14353  seqcoll  14499  ccatval21sw  14619  cshwidxmod  14837  cshwidxm1  14841  repswcshw  14846  isercolllem1  15697  harmonic  15891  efaddlem  16125  rpnnen2lem9  16254  rpnnen2lem12  16257  sqrt2irr  16281  nndivdvds  16295  dvdsle  16343  fzm1ndvds  16355  nno  16415  nnoddm1d2  16419  divalg2  16438  divalgmod  16439  ndvdsadd  16443  modgcd  16565  gcdzeq  16585  nn0rppwr  16594  sqgcd  16595  nn0expgcd  16597  dvdssqlem  16599  lcmgcdlem  16639  lcmf  16666  coprmgcdb  16682  qredeq  16690  qredeu  16691  isprm3  16716  ge2nprmge4  16734  prmdvdsfz  16738  isprm5  16740  ncoprmlnprm  16761  divdenle  16782  phibndlem  16803  eulerthlem2  16815  hashgcdlem  16821  oddprm  16843  pythagtriplem10  16853  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem16  16863  pythagtriplem19  16866  pclem  16871  pc2dvds  16912  pcmpt  16925  fldivp1  16930  pcbc  16933  infpnlem1  16943  infpn2  16946  prmreclem1  16949  prmreclem3  16951  vdwlem3  17016  ram0  17055  prmgaplem4  17087  prmgaplem7  17090  cshwshashlem1  17129  cshwshashlem2  17130  setsstruct2  17207  mulgnegnn  19114  mulgmodid  19143  odmodnn0  19572  gexdvds  19616  sylow3lem6  19664  prmirredlem  21500  znidomb  21597  chfacfisf  22875  chfacfisfcpmat  22876  chfacffsupp  22877  chfacfscmul0  22879  chfacfpmmul0  22883  ovolunlem1a  25544  ovoliunlem2  25551  ovolicc2lem3  25567  ovolicc2lem4  25568  iundisj2  25597  dyadss  25642  volsup2  25653  volivth  25655  vitali  25661  ismbf3d  25702  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  itg2seq  25791  itg2gt0  25809  itg2cnlem1  25810  idomrootle  26226  plyeq0lem  26263  dgreq0  26319  dgrcolem2  26328  elqaalem2  26376  elqaalem3  26377  logtayllem  26715  leibpi  26999  birthdaylem3  27010  zetacvg  27072  eldmgm  27079  basellem1  27138  basellem2  27139  basellem3  27140  basellem6  27143  basellem9  27146  prmorcht  27235  dvdsflsumcom  27245  muinv  27250  vmalelog  27263  chtublem  27269  logfac2  27275  logfaclbnd  27280  pcbcctr  27334  bcmono  27335  bposlem1  27342  bposlem5  27346  bposlem6  27347  bpos  27351  lgsval4a  27377  gausslemma2dlem0c  27416  gausslemma2dlem0d  27417  gausslemma2dlem1a  27423  gausslemma2dlem2  27425  gausslemma2dlem3  27426  gausslemma2dlem5  27429  lgsquadlem1  27438  lgsquadlem2  27439  2lgslem1a1  27447  2sqreunnlem1  27507  2sqreunnltlem  27508  dchrisum0re  27571  dchrisum0lem1  27574  logdivbnd  27614  ostth2lem1  27676  ostth2lem3  27693  pthdlem2lem  29799  crctcshwlkn0lem1  29839  crctcshwlkn0lem3  29841  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem6  29844  crctcshwlkn0lem7  29845  crctcshwlkn0  29850  clwlkclwwlkf1lem2  30033  clwwisshclwwslem  30042  clwwlkel  30074  clwwlkf  30075  clwwlkf1  30077  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  eucrctshift  30271  eucrct2eupth  30273  numclwlk2lem2f  30405  nmounbseqi  30805  nmounbseqiALT  30806  nmobndseqi  30807  nmobndseqiALT  30808  ubthlem1  30898  minvecolem3  30904  lnconi  32061  iundisj2f  32609  nnmulge  32755  xrsmulgzz  32993  esumpmono  34059  eulerpartlemb  34349  fibp1  34382  subfaclim  35172  subfacval3  35173  snmlff  35313  fz0n  35710  bcprod  35717  nn0prpwlem  36304  nn0prpw  36305  nndivsub  36439  nndivlub  36440  knoppcnlem2  36476  knoppcnlem4  36478  knoppndvlem11  36504  knoppndvlem12  36505  knoppndvlem14  36507  poimirlem13  37619  poimirlem14  37620  poimirlem31  37637  poimirlem32  37638  mblfinlem2  37644  fzmul  37727  incsequz  37734  nnubfi  37736  nninfnub  37737  2ap1caineq  42126  sticksstones1  42127  unitscyglem5  42180  metakunt26  42211  metakunt29  42214  metakunt30  42215  factwoffsmonot  42223  nnadddir  42283  nnmul1com  42284  sn-nnne0  42454  nn0addcom  42456  renegmulnnass  42459  nn0mulcom  42460  zmulcomlem  42461  fimgmcyc  42520  irrapxlem1  42809  irrapxlem2  42810  pellexlem1  42816  pellexlem5  42820  pellqrex  42866  monotoddzzfi  42930  jm2.24nn  42947  congabseq  42962  acongrep  42968  acongeq  42971  expdiophlem1  43009  idomodle  43179  relexpmulnn  43698  prmunb2  44306  hashnzfzclim  44317  fmuldfeq  45538  sumnnodd  45585  stoweidlem14  45969  stoweidlem17  45972  stoweidlem20  45975  stoweidlem49  46004  stoweidlem60  46015  wallispilem3  46022  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem1  46029  stirlinglem3  46031  stirlinglem4  46032  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlingr  46045  dirker2re  46047  dirkerval2  46049  dirkerre  46050  dirkertrigeqlem1  46053  fourierdlem66  46127  fourierdlem73  46134  fourierdlem83  46144  fourierdlem87  46148  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fouriersw  46186  etransclem24  46213  sge0rpcpnf  46376  hoicvr  46503  hoicvrrex  46511  vonioolem2  46636  vonicclem2  46639  fsupdm  46797  finfdm  46801  smfinfdmmbllem  46803  subsubelfzo0  47275  addmodne  47283  submodlt  47289  fmtnodvds  47468  2pwp1prm  47513  lighneallem2  47530  nn0oALTV  47620  nneven  47622  nnsum4primes4  47713  nnsum4primesprm  47715  nnsum4primesgbe  47717  nnsum4primesle9  47719  bgoldbachlt  47737  tgoldbach  47741  gpgusgralem  47945  ceilhalfelfzo1  47950  2tceilhalfelfzo1  47952  gpgedgvtx0  47953  altgsumbcALT  48197  modn0mul  48369  m1modmmod  48370  difmodm1lt  48371  nnlog2ge0lt1  48415  logbpw2m1  48416  blennn  48424  blennnelnn  48425  nnpw2pmod  48432  nnolog2flm1  48439  digvalnn0  48448  dignn0fr  48450  dignn0ldlem  48451  dignnld  48452  dig2nn1st  48454