Theorem nnred 11918

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 11907	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3915	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 10801  ℕcn 11903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-nn 11904

This theorem is referenced by:  nnne0  11937  uzwo3  12612  modmulnn  13537  bernneq3  13874  expmulnbnd  13878  expnngt1b  13885  facwordi  13931  faclbnd  13932  faclbnd2  13933  faclbnd3  13934  faclbnd5  13940  faclbnd6  13941  facubnd  13942  facavg  13943  bcp1nk  13959  hashf1  14099  swrds2  14581  isercolllem1  15304  isercoll  15307  o1fsum  15453  climcndslem1  15489  climcndslem2  15490  climcnds  15491  eftabs  15713  efcllem  15715  ege2le3  15727  efcj  15729  eftlub  15746  eflegeo  15758  eirrlem  15841  fzm1ndvds  15959  nno  16019  nnoddm1d2  16023  bitsfzolem  16069  bitsfzo  16070  bitsinv1lem  16076  sadcaddlem  16092  smueqlem  16125  bezoutlem3  16177  bezoutlem4  16178  sqgcd  16198  lcmgcdlem  16239  lcmf  16266  prmind2  16318  coprm  16344  prmfac1  16354  prmndvdsfaclt  16358  divdenle  16381  qnumgt0  16382  zsqrtelqelz  16390  hashdvds  16404  eulerthlem2  16411  odzdvds  16424  vfermltl  16430  modprm0  16434  pythagtriplem11  16454  pythagtriplem13  16456  pythagtriplem19  16462  pclem  16467  pcpre1  16471  pcidlem  16501  dvdsprmpweqle  16515  pcadd  16518  pcmpt  16521  pcmpt2  16522  pcfaclem  16527  pcfac  16528  qexpz  16530  pockthlem  16534  pockthg  16535  prmreclem1  16545  prmreclem3  16547  prmreclem4  16548  prmreclem5  16549  1arithlem4  16555  1arith  16556  4sqlem5  16571  4sqlem6  16572  4sqlem10  16576  mul4sqlem  16582  4sqlem11  16584  4sqlem12  16585  4sqlem13  16586  4sqlem14  16587  4sqlem15  16588  4sqlem16  16589  4sqlem17  16590  vdwlem1  16610  vdwlem3  16612  vdwlem6  16615  vdwlem9  16618  vdwlem10  16619  vdwlem12  16621  vdwnnlem3  16626  ramub1lem1  16655  prmolefac  16675  prmgaplem4  16683  prmgaplem5  16684  prmgaplem6  16685  prmgaplem8  16687  2expltfac  16722  cshwshashnsame  16733  setsstruct2  16803  psgnunilem4  19020  mndodconglem  19064  oddvds  19070  sylow1lem1  19118  sylow1lem5  19122  fislw  19145  efgredlem  19268  gexexlem  19368  zringlpirlem3  20598  prmirredlem  20606  fvmptnn04if  21906  fvmptnn04ifb  21908  fvmptnn04ifc  21909  fvmptnn04ifd  21910  chfacfisf  21911  chfacfisfcpmat  21912  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  lebnumii  24035  lmnn  24332  ovolunlem1a  24565  ovoliunlem1  24571  ovolicc2lem3  24588  ovolicc2lem4  24589  iundisj  24617  voliunlem1  24619  uniioombllem3  24654  dyadf  24660  dyadovol  24662  dyaddisjlem  24664  dyadmaxlem  24666  opnmbllem  24670  vitalilem4  24680  mbfi1fseqlem1  24785  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  itg2gt0  24830  itg2cnlem2  24832  dgreq0  25331  dgrco  25341  elqaalem2  25385  aaliou3lem2  25408  aaliou3lem8  25410  aaliou3lem9  25415  leibpi  25997  log2tlbnd  26000  birthdaylem3  26008  amgm  26045  emcllem2  26051  harmonicbnd4  26065  lgamgulmlem1  26083  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem4  26086  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamucov  26092  lgamcvg2  26109  wilthlem1  26122  ftalem5  26131  basellem1  26135  basellem2  26136  basellem3  26137  basellem4  26138  basellem5  26139  basellem6  26140  basellem8  26142  chtge0  26166  chtwordi  26210  vma1  26220  dvdsflf1o  26241  dvdsflsumcom  26242  fsumfldivdiaglem  26243  sgmmul  26254  chtublem  26264  fsumvma2  26267  logfac2  26270  chpchtsum  26272  chpub  26273  logfaclbnd  26275  logexprlim  26278  mersenne  26280  perfectlem2  26283  dchrelbas4  26296  bposlem1  26337  bposlem2  26338  bposlem3  26339  bposlem4  26340  bposlem5  26341  bposlem6  26342  bposlem7  26343  bposlem9  26345  lgslem1  26350  lgsval2lem  26360  lgsdirprm  26384  lgsdir  26385  lgsne0  26388  lgsqrlem2  26400  gausslemma2dlem0h  26416  gausslemma2dlem0i  26417  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  gausslemma2dlem7  26426  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgseisen  26432  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  2sqlem3  26473  2sqlem8  26479  2sqblem  26484  2sqmod  26489  chebbnd1lem1  26522  chebbnd1lem3  26524  chtppilimlem1  26526  rplogsumlem1  26537  rplogsumlem2  26538  dchrisum0lem1a  26539  rpvmasumlem  26540  dchrisumlema  26541  dchrisumlem1  26542  dchrisumlem2  26543  dchrisumlem3  26544  dchrvmasumiflem1  26554  dchrisum0flblem2  26562  dchrisum0re  26566  dchrisum0lem1b  26568  dchrisum0lem1  26569  dirith2  26581  selbergb  26602  selberg2lem  26603  logdivbnd  26609  selberg3lem2  26611  selberg4lem1  26613  pntrsumo1  26618  pntrsumbnd2  26620  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntpbnd1a  26638  pntpbnd1  26639  pntibndlem2a  26643  pntibndlem2  26644  pntlemg  26651  pntlemh  26652  pntlemj  26656  pntlemf  26658  ostth2lem1  26671  padicabvf  26684  padicabvcxp  26685  ostth2lem2  26687  ostth2lem3  26688  ostth2lem4  26689  ostth2  26690  ostth3  26691  numclwwlk5  28653  numclwwlk7  28656  ubthlem2  29134  minvecolem4  29143  iundisjf  30829  ssnnssfz  31010  iundisjfi  31019  pfxlsw2ccat  31126  pmtrto1cl  31268  psgnfzto1stlem  31269  fzto1st1  31271  fzto1st  31272  psgnfzto1st  31274  cycpmco2lem6  31300  cycpmco2lem7  31301  smatrcl  31648  smattr  31651  smatbl  31652  smatbr  31653  1smat1  31656  submateqlem1  31659  submateqlem2  31660  submateq  31661  esumcst  31931  fiunelros  32042  oddpwdc  32221  eulerpartlems  32227  eulerpartlemgc  32229  fiblem  32265  dstfrvunirn  32341  dstfrvclim1  32344  ballotlemimin  32372  fsum2dsub  32487  reprinfz1  32502  hgt750lemd  32528  hgt750lemb  32536  hgt750leme  32538  tgoldbachgtde  32540  tgoldbachgt  32543  subfaclim  33050  subfacval3  33051  erdszelem7  33059  erdszelem8  33060  erdsze2lem2  33066  cvmliftlem2  33148  cvmliftlem6  33152  cvmliftlem7  33153  cvmliftlem8  33154  cvmliftlem9  33155  cvmliftlem10  33156  cvmliftlem13  33158  bcprod  33610  bccolsum  33611  faclimlem2  33616  faclim2  33620  nn0prpwlem  34438  knoppndvlem15  34633  knoppndvlem17  34635  knoppndvlem18  34636  knoppndvlem19  34637  knoppndvlem20  34638  knoppndvlem21  34639  poimirlem3  35707  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem26  35730  poimirlem28  35732  opnmbllem0  35740  mblfinlem2  35742  incsequz  35833  nninfnub  35836  lcmineqlem4  39968  lcmineqlem10  39974  lcmineqlem11  39975  lcmineqlem15  39979  lcmineqlem18  39982  lcmineqlem19  39983  lcmineqlem20  39984  lcmineqlem21  39985  lcmineqlem22  39986  lcmineqlem23  39987  lcmineqlem  39988  3lexlogpow5ineq2  39991  3lexlogpow5ineq4  39992  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p3  40014  aks4d1p4  40015  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8  40023  aks4d1p9  40024  2ap1caineq  40029  sticksstones1  40030  sticksstones2  40031  sticksstones3  40032  sticksstones6  40035  sticksstones7  40036  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  metakunt1  40053  metakunt2  40054  metakunt6  40058  metakunt7  40059  metakunt9  40061  metakunt10  40062  metakunt11  40063  metakunt12  40064  metakunt16  40068  metakunt18  40070  metakunt20  40072  metakunt22  40074  metakunt24  40076  metakunt27  40079  metakunt28  40080  metakunt29  40081  metakunt30  40082  nnadddir  40221  oexpreposd  40242  nn0expgcd  40256  rtprmirr  40268  flt4lem5e  40409  flt4lem6  40411  flt4lem7  40412  fltltc  40414  fltnltalem  40415  fltnlta  40416  3cubeslem3r  40425  irrapxlem3  40562  irrapxlem4  40563  irrapxlem5  40564  pellexlem2  40568  pellexlem6  40572  pell14qrgt0  40597  pell14qrgapw  40614  pellfundgt1  40621  rmspecsqrtnq  40644  ltrmxnn0  40687  jm3.1lem1  40755  jm3.1lem3  40757  dgraa0p  40890  hashnzfz2  41828  rfcnnnub  42468  nnxrd  42474  fzisoeu  42729  fsumnncl  43003  sumnnodd  43061  limsup10exlem  43203  stoweidlem1  43432  stoweidlem3  43434  stoweidlem11  43442  stoweidlem17  43448  stoweidlem20  43451  stoweidlem25  43456  stoweidlem26  43457  stoweidlem34  43465  stoweidlem38  43469  stoweidlem42  43473  stoweidlem44  43475  stoweidlem51  43482  stoweidlem59  43490  stoweidlem60  43491  wallispi  43501  wallispi2  43504  stirlinglem3  43507  stirlinglem4  43508  stirlinglem8  43512  stirlinglem10  43514  stirlinglem12  43516  stirlinglem15  43519  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkercncflem2  43535  fourierdlem11  43549  fourierdlem14  43552  fourierdlem15  43553  fourierdlem20  43558  fourierdlem31  43569  fourierdlem64  43601  fourierdlem93  43630  fourierdlem95  43632  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  sqwvfourb  43660  etransclem3  43668  etransclem19  43684  etransclem23  43688  etransclem24  43689  etransclem25  43690  etransclem32  43697  etransclem35  43700  etransclem41  43706  etransclem48  43713  qndenserrnbllem  43725  hoiqssbllem1  44050  hoiqssbllem2  44051  ovolval5lem1  44080  ovolval5lem2  44081  iccpartlt  44764  iccpartgt  44767  odz2prm2pw  44903  fmtnoprmfac1lem  44904  2pwp1prm  44929  sfprmdvdsmersenne  44943  lighneallem2  44946  proththdlem  44953  perfectALTVlem2  45062  gbowge7  45103  ztprmneprm  45571  pgrple2abl  45589  logbpw2m1  45801  nnpw2pmod  45817  nnolog2flm1  45824  blennngt2o2  45826  itcovalt2lem2lem1  45907