Theorem nnred 11810

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

Syntax hints:   → wi 4   ∈ wcel 2112  ℝcr 10693  ℕcn 11795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-i2m1 10762  ax-1ne0 10763  ax-rrecex 10766  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-nn 11796

This theorem is referenced by:  nnne0  11829  uzwo3  12504  modmulnn  13427  bernneq3  13763  expmulnbnd  13767  expnngt1b  13774  facwordi  13820  faclbnd  13821  faclbnd2  13822  faclbnd3  13823  faclbnd5  13829  faclbnd6  13830  facubnd  13831  facavg  13832  bcp1nk  13848  hashf1  13988  swrds2  14470  isercolllem1  15193  isercoll  15196  o1fsum  15340  climcndslem1  15376  climcndslem2  15377  climcnds  15378  eftabs  15600  efcllem  15602  ege2le3  15614  efcj  15616  eftlub  15633  eflegeo  15645  eirrlem  15728  fzm1ndvds  15846  nno  15906  nnoddm1d2  15910  bitsfzolem  15956  bitsfzo  15957  bitsinv1lem  15963  sadcaddlem  15979  smueqlem  16012  bezoutlem3  16064  bezoutlem4  16065  sqgcd  16085  lcmgcdlem  16126  lcmf  16153  prmind2  16205  coprm  16231  prmfac1  16241  prmndvdsfaclt  16245  divdenle  16268  qnumgt0  16269  zsqrtelqelz  16277  hashdvds  16291  eulerthlem2  16298  odzdvds  16311  vfermltl  16317  modprm0  16321  pythagtriplem11  16341  pythagtriplem13  16343  pythagtriplem19  16349  pclem  16354  pcpre1  16358  pcidlem  16388  dvdsprmpweqle  16402  pcadd  16405  pcmpt  16408  pcmpt2  16409  pcfaclem  16414  pcfac  16415  qexpz  16417  pockthlem  16421  pockthg  16422  prmreclem1  16432  prmreclem3  16434  prmreclem4  16435  prmreclem5  16436  1arithlem4  16442  1arith  16443  4sqlem5  16458  4sqlem6  16459  4sqlem10  16463  mul4sqlem  16469  4sqlem11  16471  4sqlem12  16472  4sqlem13  16473  4sqlem14  16474  4sqlem15  16475  4sqlem16  16476  4sqlem17  16477  vdwlem1  16497  vdwlem3  16499  vdwlem6  16502  vdwlem9  16505  vdwlem10  16506  vdwlem12  16508  vdwnnlem3  16513  ramub1lem1  16542  prmolefac  16562  prmgaplem4  16570  prmgaplem5  16571  prmgaplem6  16572  prmgaplem8  16574  2expltfac  16609  cshwshashnsame  16620  setsstruct2  16703  psgnunilem4  18843  mndodconglem  18887  oddvds  18893  sylow1lem1  18941  sylow1lem5  18945  fislw  18968  efgredlem  19091  gexexlem  19191  zringlpirlem3  20405  prmirredlem  20413  fvmptnn04if  21700  fvmptnn04ifb  21702  fvmptnn04ifc  21703  fvmptnn04ifd  21704  chfacfisf  21705  chfacfisfcpmat  21706  chfacfscmulgsum  21711  chfacfpmmulgsum  21715  lebnumii  23817  lmnn  24114  ovolunlem1a  24347  ovoliunlem1  24353  ovolicc2lem3  24370  ovolicc2lem4  24371  iundisj  24399  voliunlem1  24401  uniioombllem3  24436  dyadf  24442  dyadovol  24444  dyaddisjlem  24446  dyadmaxlem  24448  opnmbllem  24452  vitalilem4  24462  mbfi1fseqlem1  24567  mbfi1fseqlem3  24569  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  mbfi1fseqlem6  24572  itg2gt0  24612  itg2cnlem2  24614  dgreq0  25113  dgrco  25123  elqaalem2  25167  aaliou3lem2  25190  aaliou3lem8  25192  aaliou3lem9  25197  leibpi  25779  log2tlbnd  25782  birthdaylem3  25790  amgm  25827  emcllem2  25833  harmonicbnd4  25847  lgamgulmlem1  25865  lgamgulmlem2  25866  lgamgulmlem3  25867  lgamgulmlem4  25868  lgamgulmlem5  25869  lgamgulmlem6  25870  lgamucov  25874  lgamcvg2  25891  wilthlem1  25904  ftalem5  25913  basellem1  25917  basellem2  25918  basellem3  25919  basellem4  25920  basellem5  25921  basellem6  25922  basellem8  25924  chtge0  25948  chtwordi  25992  vma1  26002  dvdsflf1o  26023  dvdsflsumcom  26024  fsumfldivdiaglem  26025  sgmmul  26036  chtublem  26046  fsumvma2  26049  logfac2  26052  chpchtsum  26054  chpub  26055  logfaclbnd  26057  logexprlim  26060  mersenne  26062  perfectlem2  26065  dchrelbas4  26078  bposlem1  26119  bposlem2  26120  bposlem3  26121  bposlem4  26122  bposlem5  26123  bposlem6  26124  bposlem7  26125  bposlem9  26127  lgslem1  26132  lgsval2lem  26142  lgsdirprm  26166  lgsdir  26167  lgsne0  26170  lgsqrlem2  26182  gausslemma2dlem0h  26198  gausslemma2dlem0i  26199  gausslemma2dlem1a  26200  gausslemma2dlem2  26202  gausslemma2dlem7  26208  gausslemma2d  26209  lgseisenlem1  26210  lgseisenlem2  26211  lgseisenlem3  26212  lgseisenlem4  26213  lgseisen  26214  lgsquadlem1  26215  lgsquadlem2  26216  lgsquadlem3  26217  2sqlem3  26255  2sqlem8  26261  2sqblem  26266  2sqmod  26271  chebbnd1lem1  26304  chebbnd1lem3  26306  chtppilimlem1  26308  rplogsumlem1  26319  rplogsumlem2  26320  dchrisum0lem1a  26321  rpvmasumlem  26322  dchrisumlema  26323  dchrisumlem1  26324  dchrisumlem2  26325  dchrisumlem3  26326  dchrvmasumiflem1  26336  dchrisum0flblem2  26344  dchrisum0re  26348  dchrisum0lem1b  26350  dchrisum0lem1  26351  dirith2  26363  selbergb  26384  selberg2lem  26385  logdivbnd  26391  selberg3lem2  26393  selberg4lem1  26395  pntrsumo1  26400  pntrsumbnd2  26402  pntrlog2bndlem1  26412  pntrlog2bndlem2  26413  pntrlog2bndlem3  26414  pntrlog2bndlem4  26415  pntrlog2bndlem5  26416  pntpbnd1a  26420  pntpbnd1  26421  pntibndlem2a  26425  pntibndlem2  26426  pntlemg  26433  pntlemh  26434  pntlemj  26438  pntlemf  26440  ostth2lem1  26453  padicabvf  26466  padicabvcxp  26467  ostth2lem2  26469  ostth2lem3  26470  ostth2lem4  26471  ostth2  26472  ostth3  26473  numclwwlk5  28425  numclwwlk7  28428  ubthlem2  28906  minvecolem4  28915  iundisjf  30601  ssnnssfz  30782  iundisjfi  30791  pfxlsw2ccat  30898  pmtrto1cl  31039  psgnfzto1stlem  31040  fzto1st1  31042  fzto1st  31043  psgnfzto1st  31045  cycpmco2lem6  31071  cycpmco2lem7  31072  smatrcl  31414  smattr  31417  smatbl  31418  smatbr  31419  1smat1  31422  submateqlem1  31425  submateqlem2  31426  submateq  31427  esumcst  31697  fiunelros  31808  oddpwdc  31987  eulerpartlems  31993  eulerpartlemgc  31995  fiblem  32031  dstfrvunirn  32107  dstfrvclim1  32110  ballotlemimin  32138  fsum2dsub  32253  reprinfz1  32268  hgt750lemd  32294  hgt750lemb  32302  hgt750leme  32304  tgoldbachgtde  32306  tgoldbachgt  32309  subfaclim  32817  subfacval3  32818  erdszelem7  32826  erdszelem8  32827  erdsze2lem2  32833  cvmliftlem2  32915  cvmliftlem6  32919  cvmliftlem7  32920  cvmliftlem8  32921  cvmliftlem9  32922  cvmliftlem10  32923  cvmliftlem13  32925  bcprod  33373  bccolsum  33374  faclimlem2  33379  faclim2  33383  nn0prpwlem  34197  knoppndvlem15  34392  knoppndvlem17  34394  knoppndvlem18  34395  knoppndvlem19  34396  knoppndvlem20  34397  knoppndvlem21  34398  poimirlem3  35466  poimirlem6  35469  poimirlem7  35470  poimirlem8  35471  poimirlem9  35472  poimirlem10  35473  poimirlem11  35474  poimirlem12  35475  poimirlem13  35476  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem23  35486  poimirlem26  35489  poimirlem28  35491  opnmbllem0  35499  mblfinlem2  35501  incsequz  35592  nninfnub  35595  lcmineqlem4  39723  lcmineqlem10  39729  lcmineqlem11  39730  lcmineqlem15  39734  lcmineqlem18  39737  lcmineqlem19  39738  lcmineqlem20  39739  lcmineqlem21  39740  lcmineqlem22  39741  lcmineqlem23  39742  lcmineqlem  39743  3lexlogpow5ineq2  39746  3lexlogpow5ineq4  39747  3lexlogpow2ineq2  39750  3lexlogpow5ineq5  39751  aks4d1p1p3  39759  aks4d1p1p2  39760  aks4d1p1p4  39761  aks4d1p1p5  39765  aks4d1p1  39766  2ap1caineq  39770  sticksstones1  39771  sticksstones2  39772  sticksstones3  39773  sticksstones6  39776  sticksstones7  39777  sticksstones10  39780  sticksstones12a  39782  sticksstones12  39783  metakunt1  39788  metakunt2  39789  metakunt6  39793  metakunt7  39794  metakunt9  39796  metakunt10  39797  metakunt11  39798  metakunt12  39799  metakunt16  39803  metakunt18  39805  metakunt20  39807  metakunt22  39809  metakunt24  39811  metakunt27  39814  metakunt28  39815  metakunt29  39816  metakunt30  39817  nnadddir  39948  oexpreposd  39969  nn0expgcd  39984  rtprmirr  39996  flt4lem5e  40137  flt4lem6  40139  flt4lem7  40140  fltltc  40142  fltnltalem  40143  fltnlta  40144  3cubeslem3r  40153  irrapxlem3  40290  irrapxlem4  40291  irrapxlem5  40292  pellexlem2  40296  pellexlem6  40300  pell14qrgt0  40325  pell14qrgapw  40342  pellfundgt1  40349  rmspecsqrtnq  40372  ltrmxnn0  40415  jm3.1lem1  40483  jm3.1lem3  40485  dgraa0p  40618  hashnzfz2  41553  rfcnnnub  42193  nnxrd  42199  fzisoeu  42453  fsumnncl  42730  sumnnodd  42789  limsup10exlem  42931  stoweidlem1  43160  stoweidlem3  43162  stoweidlem11  43170  stoweidlem17  43176  stoweidlem20  43179  stoweidlem25  43184  stoweidlem26  43185  stoweidlem34  43193  stoweidlem38  43197  stoweidlem42  43201  stoweidlem44  43203  stoweidlem51  43210  stoweidlem59  43218  stoweidlem60  43219  wallispi  43229  wallispi2  43232  stirlinglem3  43235  stirlinglem4  43236  stirlinglem8  43240  stirlinglem10  43242  stirlinglem12  43244  stirlinglem15  43247  dirkertrigeqlem2  43258  dirkertrigeqlem3  43259  dirkercncflem2  43263  fourierdlem11  43277  fourierdlem14  43280  fourierdlem15  43281  fourierdlem20  43286  fourierdlem31  43297  fourierdlem64  43329  fourierdlem93  43358  fourierdlem95  43360  fourierdlem103  43368  fourierdlem104  43369  fourierdlem112  43377  sqwvfourb  43388  etransclem3  43396  etransclem19  43412  etransclem23  43416  etransclem24  43417  etransclem25  43418  etransclem32  43425  etransclem35  43428  etransclem41  43434  etransclem48  43441  qndenserrnbllem  43453  hoiqssbllem1  43778  hoiqssbllem2  43779  ovolval5lem1  43808  ovolval5lem2  43809  iccpartlt  44492  iccpartgt  44495  odz2prm2pw  44631  fmtnoprmfac1lem  44632  2pwp1prm  44657  sfprmdvdsmersenne  44671  lighneallem2  44674  proththdlem  44681  perfectALTVlem2  44790  gbowge7  44831  ztprmneprm  45299  pgrple2abl  45317  logbpw2m1  45529  nnpw2pmod  45545  nnolog2flm1  45552  blennngt2o2  45554  itcovalt2lem2lem1  45635