Theorem nnre 12153

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11026  ℕcn 12146

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-i2m1 11095  ax-1ne0 11096  ax-rrecex 11099  ax-cnre 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-nn 12147

This theorem is referenced by:  nnrei  12155  nnmulcl  12170  nn2ge  12173  nnge1  12174  nngt1ne1  12175  nnle1eq1  12176  nngt0  12177  nnnlt1  12178  nnnle0  12179  nndivre  12187  nnrecgt0  12189  nnsub  12190  nnunb  12398  arch  12399  nnrecl  12400  bndndx  12401  0mnnnnn0  12434  nnnegz  12492  elnnz  12499  elz2  12507  nnz  12510  gtndiv  12570  prime  12574  btwnz  12596  indstr  12830  qre  12867  elpq  12889  elpqb  12890  rpnnen1lem2  12891  rpnnen1lem1  12892  rpnnen1lem3  12893  rpnnen1lem5  12895  nnrp  12918  nnledivrp  13020  qbtwnre  13115  elfzo0le  13620  fzonmapblen  13625  fzo1fzo0n0  13632  ubmelfzo  13647  fzonn0p1p1  13661  ubmelm1fzo  13680  subfzo0  13709  adddivflid  13739  flltdivnn0lt  13754  quoremz  13776  quoremnn0ALT  13778  intfracq  13780  fldiv  13781  modmulnn  13810  m1modnnsub1  13841  addmodid  13843  modifeq2int  13857  modaddmodup  13858  modaddmodlo  13859  modfzo0difsn  13867  modsumfzodifsn  13868  addmodlteq  13870  nnlesq  14129  digit2  14160  digit1  14161  expnngt1  14165  facdiv  14211  facndiv  14212  faclbnd  14214  faclbnd3  14216  faclbnd4lem4  14220  faclbnd5  14222  bcval5  14242  seqcoll  14388  ccatval21sw  14510  cshwidxmod  14727  cshwidxm1  14731  repswcshw  14736  isercolllem1  15589  harmonic  15783  efaddlem  16017  rpnnen2lem9  16148  rpnnen2lem12  16151  sqrt2irr  16175  nndivdvds  16189  dvdsle  16238  fzm1ndvds  16250  nno  16310  nnoddm1d2  16314  divalg2  16333  divalgmod  16334  ndvdsadd  16338  modgcd  16460  gcdzeq  16480  nn0rppwr  16489  sqgcd  16490  nn0expgcd  16492  dvdssqlem  16494  lcmgcdlem  16534  lcmf  16561  coprmgcdb  16577  qredeq  16585  qredeu  16586  isprm3  16611  ge2nprmge4  16629  prmdvdsfz  16633  isprm5  16635  ncoprmlnprm  16656  divdenle  16677  phibndlem  16698  eulerthlem2  16710  hashgcdlem  16716  oddprm  16739  pythagtriplem10  16749  pythagtriplem12  16755  pythagtriplem14  16757  pythagtriplem16  16759  pythagtriplem19  16762  pclem  16767  pc2dvds  16808  pcmpt  16821  fldivp1  16826  pcbc  16829  infpnlem1  16839  infpn2  16842  prmreclem1  16845  prmreclem3  16847  vdwlem3  16912  ram0  16951  prmgaplem4  16983  prmgaplem7  16986  cshwshashlem1  17024  cshwshashlem2  17025  setsstruct2  17102  mulgnegnn  19018  mulgmodid  19047  odmodnn0  19473  gexdvds  19517  sylow3lem6  19565  prmirredlem  21429  znidomb  21518  chfacfisf  22797  chfacfisfcpmat  22798  chfacffsupp  22799  chfacfscmul0  22801  chfacfpmmul0  22805  ovolunlem1a  25441  ovoliunlem2  25448  ovolicc2lem3  25464  ovolicc2lem4  25465  iundisj2  25494  dyadss  25539  volsup2  25550  volivth  25552  vitali  25558  ismbf3d  25599  mbfi1fseqlem3  25662  mbfi1fseqlem4  25663  mbfi1fseqlem5  25664  itg2seq  25687  itg2gt0  25705  itg2cnlem1  25706  idomrootle  26119  plyeq0lem  26156  dgreq0  26211  dgrcolem2  26220  elqaalem2  26268  elqaalem3  26269  logtayllem  26608  leibpi  26892  birthdaylem3  26903  zetacvg  26965  eldmgm  26972  basellem1  27031  basellem2  27032  basellem3  27033  basellem6  27036  basellem9  27039  prmorcht  27128  dvdsflsumcom  27138  muinv  27143  vmalelog  27156  chtublem  27162  logfac2  27168  logfaclbnd  27173  pcbcctr  27227  bcmono  27228  bposlem1  27235  bposlem5  27239  bposlem6  27240  bpos  27244  lgsval4a  27270  gausslemma2dlem0c  27309  gausslemma2dlem0d  27310  gausslemma2dlem1a  27316  gausslemma2dlem2  27318  gausslemma2dlem3  27319  gausslemma2dlem5  27322  lgsquadlem1  27331  lgsquadlem2  27332  2lgslem1a1  27340  2sqreunnlem1  27400  2sqreunnltlem  27401  dchrisum0re  27464  dchrisum0lem1  27467  logdivbnd  27507  ostth2lem1  27569  ostth2lem3  27586  pthdlem2lem  29824  crctcshwlkn0lem1  29867  crctcshwlkn0lem3  29869  crctcshwlkn0lem4  29870  crctcshwlkn0lem5  29871  crctcshwlkn0lem6  29872  crctcshwlkn0lem7  29873  crctcshwlkn0  29878  clwlkclwwlkf1lem2  30064  clwwisshclwwslem  30073  clwwlkel  30105  clwwlkf  30106  clwwlkf1  30108  wwlksext2clwwlk  30116  wwlksubclwwlk  30117  eucrctshift  30302  eucrct2eupth  30304  numclwlk2lem2f  30436  nmounbseqi  30837  nmounbseqiALT  30838  nmobndseqi  30839  nmobndseqiALT  30840  ubthlem1  30930  minvecolem3  30936  lnconi  32093  iundisj2f  32649  nnmulge  32801  xrsmulgzz  33074  esumpmono  34229  eulerpartlemb  34518  fibp1  34551  subfaclim  35376  subfacval3  35377  snmlff  35517  fz0n  35919  bcprod  35926  nn0prpwlem  36510  nn0prpw  36511  nndivsub  36645  nndivlub  36646  knoppcnlem2  36752  knoppcnlem4  36754  knoppndvlem11  36780  knoppndvlem12  36781  knoppndvlem14  36783  poimirlem13  37945  poimirlem14  37946  poimirlem31  37963  poimirlem32  37964  mblfinlem2  37970  fzmul  38053  incsequz  38060  nnubfi  38062  nninfnub  38063  2ap1caineq  42576  sticksstones1  42577  unitscyglem5  42630  nnadddir  42701  nnmul1com  42702  sn-nnne0  42904  nn0addcom  42906  renegmulnnass  42909  nn0mulcom  42910  zmulcomlem  42911  fimgmcyc  42978  irrapxlem1  43253  irrapxlem2  43254  pellexlem1  43260  pellexlem5  43264  pellqrex  43310  monotoddzzfi  43373  jm2.24nn  43390  congabseq  43405  acongrep  43411  acongeq  43414  expdiophlem1  43452  idomodle  43622  relexpmulnn  44139  prmunb2  44741  hashnzfzclim  44752  fmuldfeq  46017  sumnnodd  46064  stoweidlem14  46446  stoweidlem17  46449  stoweidlem20  46452  stoweidlem49  46481  stoweidlem60  46492  wallispilem3  46499  wallispilem4  46500  wallispilem5  46501  wallispi  46502  wallispi2lem1  46503  wallispi2lem2  46504  stirlinglem1  46506  stirlinglem3  46508  stirlinglem4  46509  stirlinglem6  46511  stirlinglem7  46512  stirlinglem10  46515  stirlinglem11  46516  stirlinglem12  46517  stirlinglem13  46518  stirlingr  46522  dirker2re  46524  dirkerval2  46526  dirkerre  46527  dirkertrigeqlem1  46530  fourierdlem66  46604  fourierdlem73  46611  fourierdlem83  46621  fourierdlem87  46625  fourierdlem103  46641  fourierdlem104  46642  fourierdlem111  46649  fouriersw  46663  etransclem24  46690  sge0rpcpnf  46853  hoicvr  46980  hoicvrrex  46988  vonioolem2  47113  vonicclem2  47116  fsupdm  47274  finfdm  47278  smfinfdmmbllem  47280  subsubelfzo0  47760  ceilhalfelfzo1  47764  2tceilhalfelfzo1  47766  ceilhalfnn  47770  addmodne  47778  submodlt  47784  modn0mul  47791  m1modmmod  47792  difmodm1lt  47793  modlt0b  47797  fmtnodvds  47978  2pwp1prm  48023  lighneallem2  48040  nn0oALTV  48130  nneven  48132  nnsum4primes4  48223  nnsum4primesprm  48225  nnsum4primesgbe  48227  nnsum4primesle9  48229  bgoldbachlt  48247  tgoldbach  48251  gpgusgralem  48490  gpgedgvtx0  48495  gpg3kgrtriexlem1  48517  gpg3kgrtriexlem2  48518  gpg3kgrtriexlem3  48519  gpg3kgrtriexlem4  48520  gpg3kgrtriexlem6  48522  altgsumbcALT  48787  nnlog2ge0lt1  49000  logbpw2m1  49001  blennn  49009  blennnelnn  49010  nnpw2pmod  49017  nnolog2flm1  49024  digvalnn0  49033  dignn0fr  49035  dignn0ldlem  49036  dignnld  49037  dig2nn1st  49039