Theorem nnred 12098

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝcr 10980  ℕcn 12083

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5251  ax-nul 5258  ax-pr 5379  ax-un 7659  ax-1cn 11039  ax-icn 11040  ax-addcl 11041  ax-addrcl 11042  ax-mulcl 11043  ax-mulrcl 11044  ax-i2m1 11049  ax-1ne0 11050  ax-rrecex 11053  ax-cnre 11054

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3735  df-csb 3851  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3924  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5184  df-tr 5218  df-id 5525  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5582  df-we 5584  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-pred 6246  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7349  df-om 7790  df-2nd 7909  df-frecs 8176  df-wrecs 8207  df-recs 8281  df-rdg 8320  df-nn 12084

This theorem is referenced by:  nnne0  12117  uzwo3  12793  modmulnn  13719  bernneq3  14056  expmulnbnd  14060  expnngt1b  14067  facwordi  14113  faclbnd  14114  faclbnd2  14115  faclbnd3  14116  faclbnd5  14122  faclbnd6  14123  facubnd  14124  facavg  14125  bcp1nk  14141  hashf1  14280  swrds2  14757  isercolllem1  15480  isercoll  15483  o1fsum  15629  climcndslem1  15665  climcndslem2  15666  climcnds  15667  eftabs  15889  efcllem  15891  ege2le3  15903  efcj  15905  eftlub  15922  eflegeo  15934  eirrlem  16017  fzm1ndvds  16135  nno  16195  nnoddm1d2  16199  bitsfzolem  16245  bitsfzo  16246  bitsinv1lem  16252  sadcaddlem  16268  smueqlem  16301  bezoutlem3  16353  bezoutlem4  16354  sqgcd  16372  lcmgcdlem  16413  lcmf  16440  prmind2  16492  coprm  16518  prmfac1  16528  prmndvdsfaclt  16532  divdenle  16555  qnumgt0  16556  zsqrtelqelz  16564  hashdvds  16578  eulerthlem2  16585  odzdvds  16598  vfermltl  16604  modprm0  16608  pythagtriplem11  16628  pythagtriplem13  16630  pythagtriplem19  16636  pclem  16641  pcpre1  16645  pcidlem  16675  dvdsprmpweqle  16689  pcadd  16692  pcmpt  16695  pcmpt2  16696  pcfaclem  16701  pcfac  16702  qexpz  16704  pockthlem  16708  pockthg  16709  prmreclem1  16719  prmreclem3  16721  prmreclem4  16722  prmreclem5  16723  1arithlem4  16729  1arith  16730  4sqlem5  16745  4sqlem6  16746  4sqlem10  16750  mul4sqlem  16756  4sqlem11  16758  4sqlem12  16759  4sqlem13  16760  4sqlem14  16761  4sqlem15  16762  4sqlem16  16763  4sqlem17  16764  vdwlem1  16784  vdwlem3  16786  vdwlem6  16789  vdwlem9  16792  vdwlem10  16793  vdwlem12  16795  vdwnnlem3  16800  ramub1lem1  16829  prmolefac  16849  prmgaplem4  16857  prmgaplem5  16858  prmgaplem6  16859  prmgaplem8  16861  2expltfac  16896  cshwshashnsame  16907  setsstruct2  16977  psgnunilem4  19206  mndodconglem  19250  oddvds  19256  sylow1lem1  19304  sylow1lem5  19308  fislw  19331  efgredlem  19453  gexexlem  19553  zringlpirlem3  20796  prmirredlem  20804  fvmptnn04if  22108  fvmptnn04ifb  22110  fvmptnn04ifc  22111  fvmptnn04ifd  22112  chfacfisf  22113  chfacfisfcpmat  22114  chfacfscmulgsum  22119  chfacfpmmulgsum  22123  lebnumii  24239  lmnn  24537  ovolunlem1a  24770  ovoliunlem1  24776  ovolicc2lem3  24793  ovolicc2lem4  24794  iundisj  24822  voliunlem1  24824  uniioombllem3  24859  dyadf  24865  dyadovol  24867  dyaddisjlem  24869  dyadmaxlem  24871  opnmbllem  24875  vitalilem4  24885  mbfi1fseqlem1  24990  mbfi1fseqlem3  24992  mbfi1fseqlem4  24993  mbfi1fseqlem5  24994  mbfi1fseqlem6  24995  itg2gt0  25035  itg2cnlem2  25037  dgreq0  25536  dgrco  25546  elqaalem2  25590  aaliou3lem2  25613  aaliou3lem8  25615  aaliou3lem9  25620  leibpi  26202  log2tlbnd  26205  birthdaylem3  26213  amgm  26250  emcllem2  26256  harmonicbnd4  26270  lgamgulmlem1  26288  lgamgulmlem2  26289  lgamgulmlem3  26290  lgamgulmlem4  26291  lgamgulmlem5  26292  lgamgulmlem6  26293  lgamucov  26297  lgamcvg2  26314  wilthlem1  26327  ftalem5  26336  basellem1  26340  basellem2  26341  basellem3  26342  basellem4  26343  basellem5  26344  basellem6  26345  basellem8  26347  chtge0  26371  chtwordi  26415  vma1  26425  dvdsflf1o  26446  dvdsflsumcom  26447  fsumfldivdiaglem  26448  sgmmul  26459  chtublem  26469  fsumvma2  26472  logfac2  26475  chpchtsum  26477  chpub  26478  logfaclbnd  26480  logexprlim  26483  mersenne  26485  perfectlem2  26488  dchrelbas4  26501  bposlem1  26542  bposlem2  26543  bposlem3  26544  bposlem4  26545  bposlem5  26546  bposlem6  26547  bposlem7  26548  bposlem9  26550  lgslem1  26555  lgsval2lem  26565  lgsdirprm  26589  lgsdir  26590  lgsne0  26593  lgsqrlem2  26605  gausslemma2dlem0h  26621  gausslemma2dlem0i  26622  gausslemma2dlem1a  26623  gausslemma2dlem2  26625  gausslemma2dlem7  26631  gausslemma2d  26632  lgseisenlem1  26633  lgseisenlem2  26634  lgseisenlem3  26635  lgseisenlem4  26636  lgseisen  26637  lgsquadlem1  26638  lgsquadlem2  26639  lgsquadlem3  26640  2sqlem3  26678  2sqlem8  26684  2sqblem  26689  2sqmod  26694  chebbnd1lem1  26727  chebbnd1lem3  26729  chtppilimlem1  26731  rplogsumlem1  26742  rplogsumlem2  26743  dchrisum0lem1a  26744  rpvmasumlem  26745  dchrisumlema  26746  dchrisumlem1  26747  dchrisumlem2  26748  dchrisumlem3  26749  dchrvmasumiflem1  26759  dchrisum0flblem2  26767  dchrisum0re  26771  dchrisum0lem1b  26773  dchrisum0lem1  26774  dirith2  26786  selbergb  26807  selberg2lem  26808  logdivbnd  26814  selberg3lem2  26816  selberg4lem1  26818  pntrsumo1  26823  pntrsumbnd2  26825  pntrlog2bndlem1  26835  pntrlog2bndlem2  26836  pntrlog2bndlem3  26837  pntrlog2bndlem4  26838  pntrlog2bndlem5  26839  pntpbnd1a  26843  pntpbnd1  26844  pntibndlem2a  26848  pntibndlem2  26849  pntlemg  26856  pntlemh  26857  pntlemj  26861  pntlemf  26863  ostth2lem1  26876  padicabvf  26889  padicabvcxp  26890  ostth2lem2  26892  ostth2lem3  26893  ostth2lem4  26894  ostth2  26895  ostth3  26896  numclwwlk5  29106  numclwwlk7  29109  ubthlem2  29587  minvecolem4  29596  iundisjf  31279  ssnnssfz  31459  iundisjfi  31468  pfxlsw2ccat  31575  pmtrto1cl  31717  psgnfzto1stlem  31718  fzto1st1  31720  fzto1st  31721  psgnfzto1st  31723  cycpmco2lem6  31749  cycpmco2lem7  31750  smatrcl  32108  smattr  32111  smatbl  32112  smatbr  32113  1smat1  32116  submateqlem1  32119  submateqlem2  32120  submateq  32121  esumcst  32393  fiunelros  32504  oddpwdc  32685  eulerpartlems  32691  eulerpartlemgc  32693  fiblem  32729  dstfrvunirn  32805  dstfrvclim1  32808  ballotlemimin  32836  fsum2dsub  32951  reprinfz1  32966  hgt750lemd  32992  hgt750lemb  33000  hgt750leme  33002  tgoldbachgtde  33004  tgoldbachgt  33007  subfaclim  33513  subfacval3  33514  erdszelem7  33522  erdszelem8  33523  erdsze2lem2  33529  cvmliftlem2  33611  cvmliftlem6  33615  cvmliftlem7  33616  cvmliftlem8  33617  cvmliftlem9  33618  cvmliftlem10  33619  cvmliftlem13  33621  bcprod  34059  bccolsum  34060  faclimlem2  34065  faclim2  34069  nn0prpwlem  34650  knoppndvlem15  34845  knoppndvlem17  34847  knoppndvlem18  34848  knoppndvlem19  34849  knoppndvlem20  34850  knoppndvlem21  34851  poimirlem3  35936  poimirlem6  35939  poimirlem7  35940  poimirlem8  35941  poimirlem9  35942  poimirlem10  35943  poimirlem11  35944  poimirlem12  35945  poimirlem13  35946  poimirlem15  35948  poimirlem16  35949  poimirlem17  35950  poimirlem19  35952  poimirlem20  35953  poimirlem21  35954  poimirlem22  35955  poimirlem23  35956  poimirlem26  35959  poimirlem28  35961  opnmbllem0  35969  mblfinlem2  35971  incsequz  36062  nninfnub  36065  lcmineqlem4  40345  lcmineqlem10  40351  lcmineqlem11  40352  lcmineqlem15  40356  lcmineqlem18  40359  lcmineqlem19  40360  lcmineqlem20  40361  lcmineqlem21  40362  lcmineqlem22  40363  lcmineqlem23  40364  lcmineqlem  40365  3lexlogpow5ineq2  40368  3lexlogpow5ineq4  40369  3lexlogpow2ineq2  40372  3lexlogpow5ineq5  40373  aks4d1p1p3  40382  aks4d1p1p2  40383  aks4d1p1p4  40384  aks4d1p1p5  40388  aks4d1p1  40389  aks4d1p3  40391  aks4d1p4  40392  aks4d1p5  40393  aks4d1p6  40394  aks4d1p7  40396  aks4d1p8d2  40398  aks4d1p8  40400  aks4d1p9  40401  2ap1caineq  40409  sticksstones1  40410  sticksstones2  40411  sticksstones3  40412  sticksstones6  40415  sticksstones7  40416  sticksstones10  40419  sticksstones12a  40421  sticksstones12  40422  metakunt1  40433  metakunt2  40434  metakunt6  40438  metakunt7  40439  metakunt9  40441  metakunt10  40442  metakunt11  40443  metakunt12  40444  metakunt16  40448  metakunt18  40450  metakunt20  40452  metakunt22  40454  metakunt24  40456  metakunt27  40459  metakunt28  40460  metakunt29  40461  metakunt30  40462  nnadddir  40611  oexpreposd  40632  nn0expgcd  40646  rtprmirr  40658  flt4lem5e  40806  flt4lem6  40808  flt4lem7  40809  fltltc  40811  fltnltalem  40812  fltnlta  40813  3cubeslem3r  40822  irrapxlem3  40959  irrapxlem4  40960  irrapxlem5  40961  pellexlem2  40965  pellexlem6  40969  pell14qrgt0  40994  pell14qrgapw  41011  pellfundgt1  41018  rmspecsqrtnq  41041  ltrmxnn0  41085  jm3.1lem1  41153  jm3.1lem3  41155  dgraa0p  41288  hashnzfz2  42312  rfcnnnub  42952  nnxrd  42957  fzisoeu  43226  fsumnncl  43501  sumnnodd  43559  limsup10exlem  43701  stoweidlem1  43930  stoweidlem3  43932  stoweidlem11  43940  stoweidlem17  43946  stoweidlem20  43949  stoweidlem25  43954  stoweidlem26  43955  stoweidlem34  43963  stoweidlem38  43967  stoweidlem42  43971  stoweidlem44  43973  stoweidlem51  43980  stoweidlem59  43988  stoweidlem60  43989  wallispi  43999  wallispi2  44002  stirlinglem3  44005  stirlinglem4  44006  stirlinglem8  44010  stirlinglem10  44012  stirlinglem12  44014  stirlinglem15  44017  dirkertrigeqlem2  44028  dirkertrigeqlem3  44029  dirkercncflem2  44033  fourierdlem11  44047  fourierdlem14  44050  fourierdlem15  44051  fourierdlem20  44056  fourierdlem31  44067  fourierdlem64  44099  fourierdlem93  44128  fourierdlem95  44130  fourierdlem103  44138  fourierdlem104  44139  fourierdlem112  44147  sqwvfourb  44158  etransclem3  44166  etransclem19  44182  etransclem23  44186  etransclem24  44187  etransclem25  44188  etransclem32  44195  etransclem35  44198  etransclem41  44204  etransclem48  44211  qndenserrnbllem  44223  hoiqssbllem1  44549  hoiqssbllem2  44550  ovolval5lem1  44579  ovolval5lem2  44580  iccpartlt  45294  iccpartgt  45297  odz2prm2pw  45433  fmtnoprmfac1lem  45434  2pwp1prm  45459  sfprmdvdsmersenne  45473  lighneallem2  45476  proththdlem  45483  perfectALTVlem2  45592  gbowge7  45633  ztprmneprm  46101  pgrple2abl  46119  logbpw2m1  46331  nnpw2pmod  46347  nnolog2flm1  46354  blennngt2o2  46356  itcovalt2lem2lem1  46437