Theorem nnred 12189

Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem nnred

Step	Hyp	Ref	Expression
1		nnssre 12178	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3919	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℕcn 12174

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175

This theorem is referenced by:  nnne0  12211  nnadddir  12233  uzwo3  12893  modmulnn  13848  bernneq3  14193  expmulnbnd  14197  expnngt1b  14204  facwordi  14251  faclbnd  14252  faclbnd2  14253  faclbnd3  14254  faclbnd5  14260  faclbnd6  14261  facubnd  14262  facavg  14263  bcp1nk  14279  hashf1  14419  swrds2  14902  isercolllem1  15627  isercoll  15630  o1fsum  15776  climcndslem1  15814  climcndslem2  15815  climcnds  15816  eftabs  16040  efcllem  16042  ege2le3  16055  efcj  16057  eftlub  16076  eflegeo  16088  eirrlem  16171  fzm1ndvds  16291  nno  16351  nnoddm1d2  16355  bitsfzolem  16403  bitsfzo  16404  bitsinv1lem  16410  sadcaddlem  16426  smueqlem  16459  bezoutlem3  16510  bezoutlem4  16511  sqgcd  16531  nn0expgcd  16533  lcmgcdlem  16575  lcmf  16602  prmind2  16654  coprm  16681  prmfac1  16690  prmndvdsfaclt  16695  divdenle  16719  qnumgt0  16720  zsqrtelqelz  16728  hashdvds  16745  eulerthlem2  16752  odzdvds  16766  vfermltl  16772  modprm0  16776  pythagtriplem11  16796  pythagtriplem13  16798  pythagtriplem19  16804  pclem  16809  pcpre1  16813  pcidlem  16843  dvdsprmpweqle  16857  pcadd  16860  pcmpt  16863  pcmpt2  16864  pcfaclem  16869  pcfac  16870  qexpz  16872  pockthlem  16876  pockthg  16877  prmreclem1  16887  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  1arithlem4  16897  1arith  16898  4sqlem5  16913  4sqlem6  16914  4sqlem10  16918  mul4sqlem  16924  4sqlem11  16926  4sqlem12  16927  4sqlem13  16928  4sqlem14  16929  4sqlem15  16930  4sqlem16  16931  4sqlem17  16932  vdwlem1  16952  vdwlem3  16954  vdwlem6  16957  vdwlem9  16960  vdwlem10  16961  vdwlem12  16963  vdwnnlem3  16968  ramub1lem1  16997  prmolefac  17017  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  prmgaplem8  17029  2expltfac  17063  cshwshashnsame  17074  setsstruct2  17144  chnub  18588  psgnunilem4  19472  mndodconglem  19516  oddvds  19522  sylow1lem1  19573  sylow1lem5  19577  fislw  19600  efgredlem  19722  gexexlem  19827  zringlpirlem3  21444  prmirredlem  21452  fvmptnn04if  22814  fvmptnn04ifb  22816  fvmptnn04ifc  22817  fvmptnn04ifd  22818  chfacfisf  22819  chfacfisfcpmat  22820  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  lebnumii  24933  lmnn  25230  ovolunlem1a  25463  ovoliunlem1  25469  ovolicc2lem3  25486  ovolicc2lem4  25487  iundisj  25515  voliunlem1  25517  uniioombllem3  25552  dyadf  25558  dyadovol  25560  dyaddisjlem  25562  dyadmaxlem  25564  opnmbllem  25568  vitalilem4  25578  mbfi1fseqlem1  25682  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  itg2gt0  25727  itg2cnlem2  25729  dgreq0  26230  dgrco  26240  elqaalem2  26286  aaliou3lem2  26309  aaliou3lem8  26311  aaliou3lem9  26316  rtprmirr  26724  leibpi  26906  log2tlbnd  26909  birthdaylem3  26917  amgm  26954  emcllem2  26960  harmonicbnd4  26974  lgamgulmlem1  26992  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamucov  27001  lgamcvg2  27018  wilthlem1  27031  ftalem5  27040  basellem1  27044  basellem2  27045  basellem3  27046  basellem4  27047  basellem5  27048  basellem6  27049  basellem8  27051  chtge0  27075  chtwordi  27119  vma1  27129  dvdsflf1o  27150  dvdsflsumcom  27151  fsumfldivdiaglem  27152  sgmmul  27164  chtublem  27174  fsumvma2  27177  logfac2  27180  chpchtsum  27182  chpub  27183  logfaclbnd  27185  logexprlim  27188  mersenne  27190  perfectlem2  27193  dchrelbas4  27206  bposlem1  27247  bposlem2  27248  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem7  27253  bposlem9  27255  lgslem1  27260  lgsval2lem  27270  lgsdirprm  27294  lgsdir  27295  lgsne0  27298  lgsqrlem2  27310  gausslemma2dlem0h  27326  gausslemma2dlem0i  27327  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem7  27336  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgseisen  27342  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  2sqlem3  27383  2sqlem8  27389  2sqblem  27394  2sqmod  27399  chebbnd1lem1  27432  chebbnd1lem3  27434  chtppilimlem1  27436  rplogsumlem1  27447  rplogsumlem2  27448  dchrisum0lem1a  27449  rpvmasumlem  27450  dchrisumlema  27451  dchrisumlem1  27452  dchrisumlem2  27453  dchrisumlem3  27454  dchrvmasumiflem1  27464  dchrisum0flblem2  27472  dchrisum0re  27476  dchrisum0lem1b  27478  dchrisum0lem1  27479  dirith2  27491  selbergb  27512  selberg2lem  27513  logdivbnd  27519  selberg3lem2  27521  selberg4lem1  27523  pntrsumo1  27528  pntrsumbnd2  27530  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntpbnd1a  27548  pntpbnd1  27549  pntibndlem2a  27553  pntibndlem2  27554  pntlemg  27561  pntlemh  27562  pntlemj  27566  pntlemf  27568  ostth2lem1  27581  padicabvf  27594  padicabvcxp  27595  ostth2lem2  27597  ostth2lem3  27598  ostth2lem4  27599  ostth2  27600  ostth3  27601  numclwwlk5  30458  numclwwlk7  30461  nrt2irr  30543  ubthlem2  30942  minvecolem4  30951  iundisjf  32659  ssnnssfz  32860  iundisjfi  32869  nexple  32917  2exple2exp  32918  pfxlsw2ccat  33010  pmtrto1cl  33160  psgnfzto1stlem  33161  fzto1st1  33163  fzto1st  33164  psgnfzto1st  33166  cycpmco2lem6  33192  cycpmco2lem7  33193  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  fldext2rspun  33826  smatrcl  33940  smattr  33943  smatbl  33944  smatbr  33945  1smat1  33948  submateqlem1  33951  submateqlem2  33952  submateq  33953  esumcst  34207  fiunelros  34318  oddpwdc  34498  eulerpartlems  34504  eulerpartlemgc  34506  fiblem  34542  dstfrvunirn  34619  dstfrvclim1  34622  ballotlemimin  34650  fsum2dsub  34751  reprinfz1  34766  hgt750lemd  34792  hgt750lemb  34800  hgt750leme  34802  tgoldbachgtde  34804  tgoldbachgt  34807  subfaclim  35370  subfacval3  35371  erdszelem7  35379  erdszelem8  35380  erdsze2lem2  35386  cvmliftlem2  35468  cvmliftlem6  35472  cvmliftlem7  35473  cvmliftlem8  35474  cvmliftlem9  35475  cvmliftlem10  35476  cvmliftlem13  35478  bcprod  35920  bccolsum  35921  faclimlem2  35926  faclim2  35930  nn0prpwlem  36504  knoppcnlem10  36762  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem18  36789  knoppndvlem19  36790  knoppndvlem20  36791  knoppndvlem21  36792  poimirlem3  37944  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem26  37967  poimirlem28  37969  opnmbllem0  37977  mblfinlem2  37979  incsequz  38069  nninfnub  38072  lcmineqlem4  42471  lcmineqlem10  42477  lcmineqlem11  42478  lcmineqlem15  42482  lcmineqlem18  42485  lcmineqlem19  42486  lcmineqlem20  42487  lcmineqlem21  42488  lcmineqlem22  42489  lcmineqlem23  42490  lcmineqlem  42491  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p3  42517  aks4d1p4  42518  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7  42522  aks4d1p8d2  42524  aks4d1p8  42526  aks4d1p9  42527  posbezout  42539  primrootlekpowne0  42544  primrootspoweq0  42545  aks6d1c1  42555  hashscontpow1  42560  aks6d1c3  42562  aks6d1c4  42563  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5lem1  42575  2ap1caineq  42584  sticksstones1  42585  sticksstones2  42586  sticksstones3  42587  sticksstones6  42590  sticksstones7  42591  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  aks6d1c6lem4  42612  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  aks6d1c7lem2  42620  unitscyglem1  42634  unitscyglem2  42635  unitscyglem4  42637  unitscyglem5  42638  aks5lem8  42640  oexpreposd  42754  fimgmcyclem  42978  fimgmcyc  42979  flt4lem5e  43089  flt4lem6  43091  flt4lem7  43092  fltltc  43094  fltnltalem  43095  fltnlta  43096  3cubeslem3r  43119  irrapxlem3  43252  irrapxlem4  43253  irrapxlem5  43254  pellexlem2  43258  pellexlem6  43262  pell14qrgt0  43287  pell14qrgapw  43304  pellfundgt1  43311  rmspecsqrtnq  43334  ltrmxnn0  43377  jm3.1lem1  43445  jm3.1lem3  43447  dgraa0p  43577  hashnzfz2  44748  rfcnnnub  45467  nnxrd  45707  fzisoeu  45733  fsumnncl  46002  sumnnodd  46060  limsup10exlem  46200  stoweidlem1  46429  stoweidlem3  46431  stoweidlem11  46439  stoweidlem17  46445  stoweidlem20  46448  stoweidlem25  46453  stoweidlem26  46454  stoweidlem34  46462  stoweidlem38  46466  stoweidlem42  46470  stoweidlem44  46472  stoweidlem51  46479  stoweidlem59  46487  stoweidlem60  46488  wallispi  46498  wallispi2  46501  stirlinglem3  46504  stirlinglem4  46505  stirlinglem8  46509  stirlinglem10  46511  stirlinglem12  46513  stirlinglem15  46516  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkercncflem2  46532  fourierdlem11  46546  fourierdlem14  46549  fourierdlem15  46550  fourierdlem20  46555  fourierdlem31  46566  fourierdlem64  46598  fourierdlem93  46627  fourierdlem95  46629  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  sqwvfourb  46657  etransclem3  46665  etransclem19  46681  etransclem23  46685  etransclem24  46686  etransclem25  46687  etransclem32  46694  etransclem35  46697  etransclem41  46703  etransclem48  46710  qndenserrnbllem  46722  hoiqssbllem1  47050  hoiqssbllem2  47051  ovolval5lem1  47080  ovolval5lem2  47081  iccpartlt  47884  iccpartgt  47887  odz2prm2pw  48026  fmtnoprmfac1lem  48027  2pwp1prm  48052  sfprmdvdsmersenne  48066  lighneallem2  48069  proththdlem  48076  perfectALTVlem2  48198  gbowge7  48239  ztprmneprm  48823  pgrple2abl  48841  logbpw2m1  49043  nnpw2pmod  49059  nnolog2flm1  49066  blennngt2o2  49068  itcovalt2lem2lem1  49149