Theorem nnre 11632

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 10525  ℕcn 11625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-nn 11626

This theorem is referenced by:  nnrei  11634  nnmulcl  11649  nn2ge  11652  nnge1  11653  nngt1ne1  11654  nnle1eq1  11655  nngt0  11656  nnnlt1  11657  nnnle0  11658  nndivre  11666  nnrecgt0  11668  nnsub  11669  nnunb  11881  arch  11882  nnrecl  11883  bndndx  11884  0mnnnnn0  11917  nnnegz  11972  elnnz  11979  elz2  11987  nnssz  11990  gtndiv  12047  prime  12051  btwnz  12072  indstr  12304  qre  12341  elpq  12362  elpqb  12363  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  nnrp  12388  nnledivrp  12489  qbtwnre  12580  elfzo0le  13076  fzonmapblen  13078  fzo1fzo0n0  13083  ubmelfzo  13097  fzonn0p1p1  13111  ubmelm1fzo  13128  subfzo0  13154  adddivflid  13183  flltdivnn0lt  13198  quoremz  13218  quoremnn0ALT  13220  intfracq  13222  fldiv  13223  modmulnn  13252  m1modnnsub1  13280  addmodid  13282  modifeq2int  13296  modaddmodup  13297  modaddmodlo  13298  modfzo0difsn  13306  modsumfzodifsn  13307  addmodlteq  13309  nnlesq  13564  digit2  13593  digit1  13594  expnngt1  13598  facdiv  13643  facndiv  13644  faclbnd  13646  faclbnd3  13648  faclbnd4lem4  13652  faclbnd5  13654  bcval5  13674  seqcoll  13818  ccatval21sw  13930  cshwidxmod  14156  cshwidxm1  14160  repswcshw  14165  isercolllem1  15013  harmonic  15206  efaddlem  15438  rpnnen2lem9  15567  rpnnen2lem12  15570  sqrt2irr  15594  nndivdvds  15608  dvdsle  15652  fzm1ndvds  15664  nno  15723  nnoddm1d2  15727  divalg2  15746  divalgmod  15747  ndvdsadd  15751  modgcd  15870  gcdmultipleOLD  15890  gcdmultiplezOLD  15891  gcdzeq  15892  sqgcd  15899  dvdssqlem  15900  lcmgcdlem  15940  lcmf  15967  coprmgcdb  15983  qredeq  15991  qredeu  15992  isprm3  16017  ge2nprmge4  16035  prmdvdsfz  16039  isprm5  16041  ncoprmlnprm  16058  divdenle  16079  phibndlem  16097  eulerthlem2  16109  hashgcdlem  16115  oddprm  16137  pythagtriplem10  16147  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem16  16157  pythagtriplem19  16160  pclem  16165  pc2dvds  16205  pcmpt  16218  fldivp1  16223  pcbc  16226  infpnlem1  16236  infpn2  16239  prmreclem1  16242  prmreclem3  16244  vdwlem3  16309  ram0  16348  prmgaplem4  16380  prmgaplem7  16383  cshwshashlem1  16421  cshwshashlem2  16422  setsstruct2  16513  mulgnegnn  18230  mulgmodid  18258  odmodnn0  18660  gexdvds  18701  sylow3lem6  18749  prmirredlem  20186  znidomb  20253  chfacfisf  21459  chfacfisfcpmat  21460  chfacffsupp  21461  chfacfscmul0  21463  chfacfpmmul0  21467  ovolunlem1a  24100  ovoliunlem2  24107  ovolicc2lem3  24123  ovolicc2lem4  24124  iundisj2  24153  dyadss  24198  volsup2  24209  volivth  24211  vitali  24217  ismbf3d  24258  mbfi1fseqlem3  24321  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  itg2seq  24346  itg2gt0  24364  itg2cnlem1  24365  plyeq0lem  24807  dgreq0  24862  dgrcolem2  24871  elqaalem2  24916  elqaalem3  24917  logtayllem  25250  leibpi  25528  birthdaylem3  25539  zetacvg  25600  eldmgm  25607  basellem1  25666  basellem2  25667  basellem3  25668  basellem6  25671  basellem9  25674  prmorcht  25763  dvdsflsumcom  25773  muinv  25778  vmalelog  25789  chtublem  25795  logfac2  25801  logfaclbnd  25806  pcbcctr  25860  bcmono  25861  bposlem1  25868  bposlem5  25872  bposlem6  25873  bpos  25877  lgsval4a  25903  gausslemma2dlem0c  25942  gausslemma2dlem0d  25943  gausslemma2dlem1a  25949  gausslemma2dlem2  25951  gausslemma2dlem3  25952  gausslemma2dlem5  25955  lgsquadlem1  25964  lgsquadlem2  25965  2lgslem1a1  25973  2sqreunnlem1  26033  2sqreunnltlem  26034  dchrisum0re  26097  dchrisum0lem1  26100  logdivbnd  26140  ostth2lem1  26202  ostth2lem3  26219  pthdlem2lem  27556  crctcshwlkn0lem1  27596  crctcshwlkn0lem3  27598  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  crctcshwlkn0lem6  27601  crctcshwlkn0lem7  27602  crctcshwlkn0  27607  clwlkclwwlkf1lem2  27790  clwwisshclwwslem  27799  clwwlkel  27831  clwwlkf  27832  clwwlkf1  27834  wwlksext2clwwlk  27842  wwlksubclwwlk  27843  eucrctshift  28028  eucrct2eupth  28030  numclwlk2lem2f  28162  nmounbseqi  28560  nmounbseqiALT  28561  nmobndseqi  28562  nmobndseqiALT  28563  ubthlem1  28653  minvecolem3  28659  lnconi  29816  iundisj2f  30353  nnmulge  30500  xrsmulgzz  30712  esumpmono  31448  eulerpartlemb  31736  fibp1  31769  subfaclim  32548  subfacval3  32549  snmlff  32689  fz0n  33075  bcprod  33083  nn0prpwlem  33783  nn0prpw  33784  nndivsub  33918  nndivlub  33919  knoppcnlem2  33946  knoppcnlem4  33948  knoppcnlem10  33954  knoppndvlem11  33974  knoppndvlem12  33975  knoppndvlem14  33977  poimirlem13  35070  poimirlem14  35071  poimirlem31  35088  poimirlem32  35089  mblfinlem2  35095  fzmul  35179  incsequz  35186  nnubfi  35188  nninfnub  35189  2ap1caineq  39349  metakunt26  39375  metakunt29  39378  metakunt30  39379  factwoffsmonot  39388  nnadddir  39471  nnmul1com  39472  nn0rppwr  39490  nn0expgcd  39492  irrapxlem1  39763  irrapxlem2  39764  pellexlem1  39770  pellexlem5  39774  pellqrex  39820  monotoddzzfi  39883  jm2.24nn  39900  congabseq  39915  acongrep  39921  acongeq  39924  expdiophlem1  39962  idomrootle  40139  idomodle  40140  relexpmulnn  40410  prmunb2  41015  hashnzfzclim  41026  fmuldfeq  42225  sumnnodd  42272  stoweidlem14  42656  stoweidlem17  42659  stoweidlem20  42662  stoweidlem49  42691  stoweidlem60  42702  wallispilem3  42709  wallispilem4  42710  wallispilem5  42711  wallispi  42712  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem1  42716  stirlinglem3  42718  stirlinglem4  42719  stirlinglem6  42721  stirlinglem7  42722  stirlinglem10  42725  stirlinglem11  42726  stirlinglem12  42727  stirlinglem13  42728  stirlingr  42732  dirker2re  42734  dirkerval2  42736  dirkerre  42737  dirkertrigeqlem1  42740  fourierdlem66  42814  fourierdlem73  42821  fourierdlem83  42831  fourierdlem87  42835  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fouriersw  42873  etransclem24  42900  sge0rpcpnf  43060  hoicvr  43187  hoicvrrex  43195  vonioolem2  43320  vonicclem2  43323  subsubelfzo0  43883  fmtnodvds  44061  2pwp1prm  44106  lighneallem2  44124  nn0oALTV  44214  nneven  44216  nnsum4primes4  44307  nnsum4primesprm  44309  nnsum4primesgbe  44311  nnsum4primesle9  44313  bgoldbachlt  44331  tgoldbach  44335  altgsumbcALT  44755  modn0mul  44934  m1modmmod  44935  difmodm1lt  44936  nnlog2ge0lt1  44980  logbpw2m1  44981  blennn  44989  blennnelnn  44990  nnpw2pmod  44997  nnolog2flm1  45004  digvalnn0  45013  dignn0fr  45015  dignn0ldlem  45016  dignnld  45017  dig2nn1st  45019