Theorem nnre 11365

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℝcr 10258  ℕcn 11357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-1cn 10317  ax-icn 10318  ax-addcl 10319  ax-addrcl 10320  ax-mulcl 10321  ax-mulrcl 10322  ax-i2m1 10327  ax-1ne0 10328  ax-rrecex 10331  ax-cnre 10332

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-ov 6913  df-om 7332  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-nn 11358

This theorem is referenced by:  nnrei  11367  nnmulcl  11382  nn2ge  11386  nnge1  11387  nngt1ne1  11388  nnle1eq1  11389  nngt0  11390  nnnlt1  11391  nnnle0  11392  nndivre  11399  nnrecgt0  11401  nnsub  11402  nnunb  11621  arch  11622  nnrecl  11623  bndndx  11624  0mnnnnn0  11659  nnnegz  11714  elnnz  11721  elz2  11728  nnssz  11731  gtndiv  11789  prime  11793  btwnz  11814  indstr  12046  qre  12083  elpq  12104  elpqb  12105  rpnnen1lem2  12106  rpnnen1lem1  12107  rpnnen1lem3  12108  rpnnen1lem5  12110  nnrp  12132  nnledivrp  12233  qbtwnre  12325  elfzo0le  12814  fzonmapblen  12816  fzo1fzo0n0  12821  ubmelfzo  12835  fzonn0p1p1  12849  elfzom1p1elfzo  12850  ubmelm1fzo  12866  subfzo0  12892  adddivflid  12921  flltdivnn0lt  12936  quoremz  12956  quoremnn0ALT  12958  intfracq  12960  fldiv  12961  modmulnn  12990  m1modnnsub1  13018  addmodid  13020  modifeq2int  13034  modaddmodup  13035  modaddmodlo  13036  modfzo0difsn  13044  modsumfzodifsn  13045  addmodlteq  13047  nnlesq  13269  digit2  13298  digit1  13299  expnngt1  13329  facdiv  13374  facndiv  13375  faclbnd  13377  faclbnd3  13379  faclbnd4lem4  13383  faclbnd5  13385  bcval5  13405  seqcoll  13544  ccatval21sw  13652  cshwidxmod  13931  cshwidxm1  13935  repswcshw  13940  isercolllem1  14779  harmonic  14972  efaddlem  15202  rpnnen2lem9  15332  rpnnen2lem12  15335  sqrt2irr  15359  nndivdvds  15373  dvdsle  15416  fzm1ndvds  15428  nno  15479  nnoddm1d2  15483  divalg2  15509  divalgmod  15510  ndvdsadd  15514  modgcd  15633  gcdmultiple  15649  gcdmultiplez  15650  gcdzeq  15651  sqgcd  15658  dvdssqlem  15659  lcmgcdlem  15699  lcmf  15726  coprmgcdb  15742  qredeq  15750  qredeu  15751  isprm3  15775  prmdvdsfz  15795  isprm5  15797  ncoprmlnprm  15814  divdenle  15835  phibndlem  15853  eulerthlem2  15865  hashgcdlem  15871  oddprm  15893  pythagtriplem10  15903  pythagtriplem12  15909  pythagtriplem14  15911  pythagtriplem16  15913  pythagtriplem19  15916  pclem  15921  pc2dvds  15961  pcmpt  15974  fldivp1  15979  pcbc  15982  infpnlem1  15992  infpn2  15995  prmreclem1  15998  prmreclem3  16000  vdwlem3  16065  ram0  16104  prmgaplem4  16136  prmgaplem7  16139  cshwshashlem1  16175  cshwshashlem2  16176  setsstruct2  16267  mulgnegnn  17912  mulgmodid  17939  odmodnn0  18317  gexdvds  18357  sylow3lem6  18405  prmirredlem  20208  znidomb  20276  chfacfisf  21036  chfacfisfcpmat  21037  chfacffsupp  21038  chfacfscmul0  21040  chfacfpmmul0  21044  ovolunlem1a  23669  ovoliunlem2  23676  ovolicc2lem3  23692  ovolicc2lem4  23693  iundisj2  23722  dyadss  23767  volsup2  23778  volivth  23780  vitali  23786  ismbf3d  23827  mbfi1fseqlem3  23890  mbfi1fseqlem4  23891  mbfi1fseqlem5  23892  itg2seq  23915  itg2gt0  23933  itg2cnlem1  23934  plyeq0lem  24372  dgreq0  24427  dgrcolem2  24436  elqaalem2  24481  elqaalem3  24482  logtayllem  24811  leibpi  25089  birthdaylem3  25100  zetacvg  25161  eldmgm  25168  basellem1  25227  basellem2  25228  basellem3  25229  basellem6  25232  basellem9  25235  prmorcht  25324  dvdsflsumcom  25334  muinv  25339  vmalelog  25350  chtublem  25356  logfac2  25362  logfaclbnd  25367  pcbcctr  25421  bcmono  25422  bposlem1  25429  bposlem5  25433  bposlem6  25434  bpos  25438  lgsval4a  25464  gausslemma2dlem0c  25503  gausslemma2dlem0d  25504  gausslemma2dlem1a  25510  gausslemma2dlem2  25512  gausslemma2dlem3  25513  gausslemma2dlem5  25516  lgsquadlem1  25525  lgsquadlem2  25526  2lgslem1a1  25534  dchrisum0re  25622  dchrisum0lem1  25625  logdivbnd  25665  ostth2lem1  25727  ostth2lem3  25744  pthdlem2lem  27076  crctcshwlkn0lem1  27116  crctcshwlkn0lem3  27118  crctcshwlkn0lem4  27119  crctcshwlkn0lem5  27120  crctcshwlkn0lem6  27121  crctcshwlkn0lem7  27122  crctcshwlkn0  27127  clwlkclwwlkf1lem2  27343  clwlkclwwlkf1lem2OLD  27344  clwwisshclwwslem  27359  clwwlkel  27392  clwwlkfOLD  27393  clwwlkf1OLD  27395  clwwlkf  27398  clwwlkf1  27400  wwlksext2clwwlk  27409  wwlksubclwwlk  27410  wwlksubclwwlkOLD  27411  eucrctshift  27616  eucrct2eupthOLD  27619  eucrct2eupth  27620  numclwlk2lem2f  27776  numclwlk2lem2fOLD  27779  numclwlk2lem2fOLDOLD  27787  nmounbseqi  28183  nmounbseqiALT  28184  nmobndseqi  28185  nmobndseqiALT  28186  ubthlem1  28277  minvecolem3  28283  lnconi  29443  iundisj2f  29946  nnmulge  30058  xrsmulgzz  30219  esumpmono  30682  eulerpartlemb  30971  fibp1  31005  subfaclim  31712  subfacval3  31713  snmlff  31853  fz0n  32154  bcprod  32162  nn0prpwlem  32850  nn0prpw  32851  nndivsub  32984  nndivlub  32985  knoppcnlem2  33012  knoppcnlem4  33014  knoppcnlem10  33020  knoppndvlem11  33040  knoppndvlem12  33041  knoppndvlem14  33043  poimirlem13  33961  poimirlem14  33962  poimirlem31  33979  poimirlem32  33980  mblfinlem2  33986  fzmul  34074  incsequz  34081  nnubfi  34083  nninfnub  34084  irrapxlem1  38225  irrapxlem2  38226  pellexlem1  38232  pellexlem5  38236  pellqrex  38282  monotoddzzfi  38345  jm2.24nn  38364  congabseq  38379  acongrep  38385  acongeq  38388  expdiophlem1  38426  idomrootle  38611  idomodle  38612  relexpmulnn  38837  prmunb2  39345  hashnzfzclim  39356  fmuldfeq  40604  sumnnodd  40651  stoweidlem14  41019  stoweidlem17  41022  stoweidlem20  41025  stoweidlem49  41054  stoweidlem60  41065  wallispilem3  41072  wallispilem4  41073  wallispilem5  41074  wallispi  41075  wallispi2lem1  41076  wallispi2lem2  41077  stirlinglem1  41079  stirlinglem3  41081  stirlinglem4  41082  stirlinglem6  41084  stirlinglem7  41085  stirlinglem10  41088  stirlinglem11  41089  stirlinglem12  41090  stirlinglem13  41091  stirlingr  41095  dirker2re  41097  dirkerval2  41099  dirkerre  41100  dirkertrigeqlem1  41103  fourierdlem66  41177  fourierdlem73  41184  fourierdlem83  41194  fourierdlem87  41198  fourierdlem103  41214  fourierdlem104  41215  fourierdlem111  41222  fouriersw  41236  etransclem24  41263  sge0rpcpnf  41423  hoicvr  41550  hoicvrrex  41558  vonioolem2  41683  vonicclem2  41686  subsubelfzo0  42218  fmtnodvds  42300  2pwp1prm  42347  lighneallem2  42367  nn0oALTV  42451  nnsum4primes4  42521  nnsum4primesprm  42523  nnsum4primesgbe  42525  nnsum4primesle9  42527  bgoldbachlt  42545  tgoldbach  42549  altgsumbcALT  42992  modn0mul  43176  m1modmmod  43177  difmodm1lt  43178  nnlog2ge0lt1  43221  logbpw2m1  43222  blennn  43230  blennnelnn  43231  nnpw2pmod  43238  nnolog2flm1  43245  digvalnn0  43254  dignn0fr  43256  dignn0ldlem  43257  dignnld  43258  dig2nn1st  43260