Theorem nnre 12152

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  ℕcn 12145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146

This theorem is referenced by:  nnrei  12154  nnmulcl  12169  nn2ge  12172  nnge1  12173  nngt1ne1  12174  nnle1eq1  12175  nngt0  12176  nnnlt1  12177  nnnle0  12178  nndivre  12186  nnrecgt0  12188  nnsub  12189  nnunb  12397  arch  12398  nnrecl  12399  bndndx  12400  0mnnnnn0  12433  nnnegz  12491  elnnz  12498  elz2  12506  nnz  12509  gtndiv  12569  prime  12573  btwnz  12595  indstr  12829  qre  12866  elpq  12888  elpqb  12889  rpnnen1lem2  12890  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  nnrp  12917  nnledivrp  13019  qbtwnre  13114  elfzo0le  13619  fzonmapblen  13624  fzo1fzo0n0  13631  ubmelfzo  13646  fzonn0p1p1  13660  ubmelm1fzo  13679  subfzo0  13708  adddivflid  13738  flltdivnn0lt  13753  quoremz  13775  quoremnn0ALT  13777  intfracq  13779  fldiv  13780  modmulnn  13809  m1modnnsub1  13840  addmodid  13842  modifeq2int  13856  modaddmodup  13857  modaddmodlo  13858  modfzo0difsn  13866  modsumfzodifsn  13867  addmodlteq  13869  nnlesq  14128  digit2  14159  digit1  14160  expnngt1  14164  facdiv  14210  facndiv  14211  faclbnd  14213  faclbnd3  14215  faclbnd4lem4  14219  faclbnd5  14221  bcval5  14241  seqcoll  14387  ccatval21sw  14509  cshwidxmod  14726  cshwidxm1  14730  repswcshw  14735  isercolllem1  15588  harmonic  15782  efaddlem  16016  rpnnen2lem9  16147  rpnnen2lem12  16150  sqrt2irr  16174  nndivdvds  16188  dvdsle  16237  fzm1ndvds  16249  nno  16309  nnoddm1d2  16313  divalg2  16332  divalgmod  16333  ndvdsadd  16337  modgcd  16459  gcdzeq  16479  nn0rppwr  16488  sqgcd  16489  nn0expgcd  16491  dvdssqlem  16493  lcmgcdlem  16533  lcmf  16560  coprmgcdb  16576  qredeq  16584  qredeu  16585  isprm3  16610  ge2nprmge4  16628  prmdvdsfz  16632  isprm5  16634  ncoprmlnprm  16655  divdenle  16676  phibndlem  16697  eulerthlem2  16709  hashgcdlem  16715  oddprm  16738  pythagtriplem10  16748  pythagtriplem12  16754  pythagtriplem14  16756  pythagtriplem16  16758  pythagtriplem19  16761  pclem  16766  pc2dvds  16807  pcmpt  16820  fldivp1  16825  pcbc  16828  infpnlem1  16838  infpn2  16841  prmreclem1  16844  prmreclem3  16846  vdwlem3  16911  ram0  16950  prmgaplem4  16982  prmgaplem7  16985  cshwshashlem1  17023  cshwshashlem2  17024  setsstruct2  17101  mulgnegnn  19014  mulgmodid  19043  odmodnn0  19469  gexdvds  19513  sylow3lem6  19561  prmirredlem  21427  znidomb  21516  chfacfisf  22798  chfacfisfcpmat  22799  chfacffsupp  22800  chfacfscmul0  22802  chfacfpmmul0  22806  ovolunlem1a  25453  ovoliunlem2  25460  ovolicc2lem3  25476  ovolicc2lem4  25477  iundisj2  25506  dyadss  25551  volsup2  25562  volivth  25564  vitali  25570  ismbf3d  25611  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  itg2seq  25699  itg2gt0  25717  itg2cnlem1  25718  idomrootle  26134  plyeq0lem  26171  dgreq0  26227  dgrcolem2  26236  elqaalem2  26284  elqaalem3  26285  logtayllem  26624  leibpi  26908  birthdaylem3  26919  zetacvg  26981  eldmgm  26988  basellem1  27047  basellem2  27048  basellem3  27049  basellem6  27052  basellem9  27055  prmorcht  27144  dvdsflsumcom  27154  muinv  27159  vmalelog  27172  chtublem  27178  logfac2  27184  logfaclbnd  27189  pcbcctr  27243  bcmono  27244  bposlem1  27251  bposlem5  27255  bposlem6  27256  bpos  27260  lgsval4a  27286  gausslemma2dlem0c  27325  gausslemma2dlem0d  27326  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  gausslemma2dlem3  27335  gausslemma2dlem5  27338  lgsquadlem1  27347  lgsquadlem2  27348  2lgslem1a1  27356  2sqreunnlem1  27416  2sqreunnltlem  27417  dchrisum0re  27480  dchrisum0lem1  27483  logdivbnd  27523  ostth2lem1  27585  ostth2lem3  27602  pthdlem2lem  29840  crctcshwlkn0lem1  29883  crctcshwlkn0lem3  29885  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem6  29888  crctcshwlkn0lem7  29889  crctcshwlkn0  29894  clwlkclwwlkf1lem2  30080  clwwisshclwwslem  30089  clwwlkel  30121  clwwlkf  30122  clwwlkf1  30124  wwlksext2clwwlk  30132  wwlksubclwwlk  30133  eucrctshift  30318  eucrct2eupth  30320  numclwlk2lem2f  30452  nmounbseqi  30852  nmounbseqiALT  30853  nmobndseqi  30854  nmobndseqiALT  30855  ubthlem1  30945  minvecolem3  30951  lnconi  32108  iundisj2f  32665  nnmulge  32818  xrsmulgzz  33091  esumpmono  34236  eulerpartlemb  34525  fibp1  34558  subfaclim  35382  subfacval3  35383  snmlff  35523  fz0n  35925  bcprod  35932  nn0prpwlem  36516  nn0prpw  36517  nndivsub  36651  nndivlub  36652  knoppcnlem2  36694  knoppcnlem4  36696  knoppndvlem11  36722  knoppndvlem12  36723  knoppndvlem14  36725  poimirlem13  37834  poimirlem14  37835  poimirlem31  37852  poimirlem32  37853  mblfinlem2  37859  fzmul  37942  incsequz  37949  nnubfi  37951  nninfnub  37952  2ap1caineq  42409  sticksstones1  42410  unitscyglem5  42463  nnadddir  42535  nnmul1com  42536  sn-nnne0  42725  nn0addcom  42727  renegmulnnass  42730  nn0mulcom  42731  zmulcomlem  42732  fimgmcyc  42799  irrapxlem1  43074  irrapxlem2  43075  pellexlem1  43081  pellexlem5  43085  pellqrex  43131  monotoddzzfi  43194  jm2.24nn  43211  congabseq  43226  acongrep  43232  acongeq  43235  expdiophlem1  43273  idomodle  43443  relexpmulnn  43960  prmunb2  44562  hashnzfzclim  44573  fmuldfeq  45839  sumnnodd  45886  stoweidlem14  46268  stoweidlem17  46271  stoweidlem20  46274  stoweidlem49  46303  stoweidlem60  46314  wallispilem3  46321  wallispilem4  46322  wallispilem5  46323  wallispi  46324  wallispi2lem1  46325  wallispi2lem2  46326  stirlinglem1  46328  stirlinglem3  46330  stirlinglem4  46331  stirlinglem6  46333  stirlinglem7  46334  stirlinglem10  46337  stirlinglem11  46338  stirlinglem12  46339  stirlinglem13  46340  stirlingr  46344  dirker2re  46346  dirkerval2  46348  dirkerre  46349  dirkertrigeqlem1  46352  fourierdlem66  46426  fourierdlem73  46433  fourierdlem83  46443  fourierdlem87  46447  fourierdlem103  46463  fourierdlem104  46464  fourierdlem111  46471  fouriersw  46485  etransclem24  46512  sge0rpcpnf  46675  hoicvr  46802  hoicvrrex  46810  vonioolem2  46935  vonicclem2  46938  fsupdm  47096  finfdm  47100  smfinfdmmbllem  47102  subsubelfzo0  47582  ceilhalfelfzo1  47586  2tceilhalfelfzo1  47588  ceilhalfnn  47592  addmodne  47600  submodlt  47606  modn0mul  47613  m1modmmod  47614  difmodm1lt  47615  modlt0b  47619  fmtnodvds  47800  2pwp1prm  47845  lighneallem2  47862  nn0oALTV  47952  nneven  47954  nnsum4primes4  48045  nnsum4primesprm  48047  nnsum4primesgbe  48049  nnsum4primesle9  48051  bgoldbachlt  48069  tgoldbach  48073  gpgusgralem  48312  gpgedgvtx0  48317  gpg3kgrtriexlem1  48339  gpg3kgrtriexlem2  48340  gpg3kgrtriexlem3  48341  gpg3kgrtriexlem4  48342  gpg3kgrtriexlem6  48344  altgsumbcALT  48609  nnlog2ge0lt1  48822  logbpw2m1  48823  blennn  48831  blennnelnn  48832  nnpw2pmod  48839  nnolog2flm1  48846  digvalnn0  48855  dignn0fr  48857  dignn0ldlem  48858  dignnld  48859  dig2nn1st  48861