Theorem nnre 12150

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11023  ℕcn 12143

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 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-i2m1 11092  ax-1ne0 11093  ax-rrecex 11096  ax-cnre 11097

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  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 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12144

This theorem is referenced by:  nnrei  12152  nnmulcl  12167  nn2ge  12170  nnge1  12171  nngt1ne1  12172  nnle1eq1  12173  nngt0  12174  nnnlt1  12175  nnnle0  12176  nndivre  12184  nnrecgt0  12186  nnsub  12187  nnunb  12395  arch  12396  nnrecl  12397  bndndx  12398  0mnnnnn0  12431  nnnegz  12489  elnnz  12496  elz2  12504  nnz  12507  gtndiv  12567  prime  12571  btwnz  12593  indstr  12827  qre  12864  elpq  12886  elpqb  12887  rpnnen1lem2  12888  rpnnen1lem1  12889  rpnnen1lem3  12890  rpnnen1lem5  12892  nnrp  12915  nnledivrp  13017  qbtwnre  13112  elfzo0le  13617  fzonmapblen  13622  fzo1fzo0n0  13629  ubmelfzo  13644  fzonn0p1p1  13658  ubmelm1fzo  13677  subfzo0  13706  adddivflid  13736  flltdivnn0lt  13751  quoremz  13773  quoremnn0ALT  13775  intfracq  13777  fldiv  13778  modmulnn  13807  m1modnnsub1  13838  addmodid  13840  modifeq2int  13854  modaddmodup  13855  modaddmodlo  13856  modfzo0difsn  13864  modsumfzodifsn  13865  addmodlteq  13867  nnlesq  14126  digit2  14157  digit1  14158  expnngt1  14162  facdiv  14208  facndiv  14209  faclbnd  14211  faclbnd3  14213  faclbnd4lem4  14217  faclbnd5  14219  bcval5  14239  seqcoll  14385  ccatval21sw  14507  cshwidxmod  14724  cshwidxm1  14728  repswcshw  14733  isercolllem1  15586  harmonic  15780  efaddlem  16014  rpnnen2lem9  16145  rpnnen2lem12  16148  sqrt2irr  16172  nndivdvds  16186  dvdsle  16235  fzm1ndvds  16247  nno  16307  nnoddm1d2  16311  divalg2  16330  divalgmod  16331  ndvdsadd  16335  modgcd  16457  gcdzeq  16477  nn0rppwr  16486  sqgcd  16487  nn0expgcd  16489  dvdssqlem  16491  lcmgcdlem  16531  lcmf  16558  coprmgcdb  16574  qredeq  16582  qredeu  16583  isprm3  16608  ge2nprmge4  16626  prmdvdsfz  16630  isprm5  16632  ncoprmlnprm  16653  divdenle  16674  phibndlem  16695  eulerthlem2  16707  hashgcdlem  16713  oddprm  16736  pythagtriplem10  16746  pythagtriplem12  16752  pythagtriplem14  16754  pythagtriplem16  16756  pythagtriplem19  16759  pclem  16764  pc2dvds  16805  pcmpt  16818  fldivp1  16823  pcbc  16826  infpnlem1  16836  infpn2  16839  prmreclem1  16842  prmreclem3  16844  vdwlem3  16909  ram0  16948  prmgaplem4  16980  prmgaplem7  16983  cshwshashlem1  17021  cshwshashlem2  17022  setsstruct2  17099  mulgnegnn  19012  mulgmodid  19041  odmodnn0  19467  gexdvds  19511  sylow3lem6  19559  prmirredlem  21425  znidomb  21514  chfacfisf  22796  chfacfisfcpmat  22797  chfacffsupp  22798  chfacfscmul0  22800  chfacfpmmul0  22804  ovolunlem1a  25451  ovoliunlem2  25458  ovolicc2lem3  25474  ovolicc2lem4  25475  iundisj2  25504  dyadss  25549  volsup2  25560  volivth  25562  vitali  25568  ismbf3d  25609  mbfi1fseqlem3  25672  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  itg2seq  25697  itg2gt0  25715  itg2cnlem1  25716  idomrootle  26132  plyeq0lem  26169  dgreq0  26225  dgrcolem2  26234  elqaalem2  26282  elqaalem3  26283  logtayllem  26622  leibpi  26906  birthdaylem3  26917  zetacvg  26979  eldmgm  26986  basellem1  27045  basellem2  27046  basellem3  27047  basellem6  27050  basellem9  27053  prmorcht  27142  dvdsflsumcom  27152  muinv  27157  vmalelog  27170  chtublem  27176  logfac2  27182  logfaclbnd  27187  pcbcctr  27241  bcmono  27242  bposlem1  27249  bposlem5  27253  bposlem6  27254  bpos  27258  lgsval4a  27284  gausslemma2dlem0c  27323  gausslemma2dlem0d  27324  gausslemma2dlem1a  27330  gausslemma2dlem2  27332  gausslemma2dlem3  27333  gausslemma2dlem5  27336  lgsquadlem1  27345  lgsquadlem2  27346  2lgslem1a1  27354  2sqreunnlem1  27414  2sqreunnltlem  27415  dchrisum0re  27478  dchrisum0lem1  27481  logdivbnd  27521  ostth2lem1  27583  ostth2lem3  27600  pthdlem2lem  29789  crctcshwlkn0lem1  29832  crctcshwlkn0lem3  29834  crctcshwlkn0lem4  29835  crctcshwlkn0lem5  29836  crctcshwlkn0lem6  29837  crctcshwlkn0lem7  29838  crctcshwlkn0  29843  clwlkclwwlkf1lem2  30029  clwwisshclwwslem  30038  clwwlkel  30070  clwwlkf  30071  clwwlkf1  30073  wwlksext2clwwlk  30081  wwlksubclwwlk  30082  eucrctshift  30267  eucrct2eupth  30269  numclwlk2lem2f  30401  nmounbseqi  30801  nmounbseqiALT  30802  nmobndseqi  30803  nmobndseqiALT  30804  ubthlem1  30894  minvecolem3  30900  lnconi  32057  iundisj2f  32614  nnmulge  32767  xrsmulgzz  33040  esumpmono  34185  eulerpartlemb  34474  fibp1  34507  subfaclim  35331  subfacval3  35332  snmlff  35472  fz0n  35874  bcprod  35881  nn0prpwlem  36465  nn0prpw  36466  nndivsub  36600  nndivlub  36601  knoppcnlem2  36637  knoppcnlem4  36639  knoppndvlem11  36665  knoppndvlem12  36666  knoppndvlem14  36668  poimirlem13  37773  poimirlem14  37774  poimirlem31  37791  poimirlem32  37792  mblfinlem2  37798  fzmul  37881  incsequz  37888  nnubfi  37890  nninfnub  37891  2ap1caineq  42338  sticksstones1  42339  unitscyglem5  42392  nnadddir  42467  nnmul1com  42468  sn-nnne0  42657  nn0addcom  42659  renegmulnnass  42662  nn0mulcom  42663  zmulcomlem  42664  fimgmcyc  42731  irrapxlem1  43006  irrapxlem2  43007  pellexlem1  43013  pellexlem5  43017  pellqrex  43063  monotoddzzfi  43126  jm2.24nn  43143  congabseq  43158  acongrep  43164  acongeq  43167  expdiophlem1  43205  idomodle  43375  relexpmulnn  43892  prmunb2  44494  hashnzfzclim  44505  fmuldfeq  45771  sumnnodd  45818  stoweidlem14  46200  stoweidlem17  46203  stoweidlem20  46206  stoweidlem49  46235  stoweidlem60  46246  wallispilem3  46253  wallispilem4  46254  wallispilem5  46255  wallispi  46256  wallispi2lem1  46257  wallispi2lem2  46258  stirlinglem1  46260  stirlinglem3  46262  stirlinglem4  46263  stirlinglem6  46265  stirlinglem7  46266  stirlinglem10  46269  stirlinglem11  46270  stirlinglem12  46271  stirlinglem13  46272  stirlingr  46276  dirker2re  46278  dirkerval2  46280  dirkerre  46281  dirkertrigeqlem1  46284  fourierdlem66  46358  fourierdlem73  46365  fourierdlem83  46375  fourierdlem87  46379  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  fouriersw  46417  etransclem24  46444  sge0rpcpnf  46607  hoicvr  46734  hoicvrrex  46742  vonioolem2  46867  vonicclem2  46870  fsupdm  47028  finfdm  47032  smfinfdmmbllem  47034  subsubelfzo0  47514  ceilhalfelfzo1  47518  2tceilhalfelfzo1  47520  ceilhalfnn  47524  addmodne  47532  submodlt  47538  modn0mul  47545  m1modmmod  47546  difmodm1lt  47547  modlt0b  47551  fmtnodvds  47732  2pwp1prm  47777  lighneallem2  47794  nn0oALTV  47884  nneven  47886  nnsum4primes4  47977  nnsum4primesprm  47979  nnsum4primesgbe  47981  nnsum4primesle9  47983  bgoldbachlt  48001  tgoldbach  48005  gpgusgralem  48244  gpgedgvtx0  48249  gpg3kgrtriexlem1  48271  gpg3kgrtriexlem2  48272  gpg3kgrtriexlem3  48273  gpg3kgrtriexlem4  48274  gpg3kgrtriexlem6  48276  altgsumbcALT  48541  nnlog2ge0lt1  48754  logbpw2m1  48755  blennn  48763  blennnelnn  48764  nnpw2pmod  48771  nnolog2flm1  48778  digvalnn0  48787  dignn0fr  48789  dignn0ldlem  48790  dignnld  48791  dig2nn1st  48793