Theorem nnred 12276

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11127  ℕcn 12261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-i2m1 11196  ax-1ne0 11197  ax-rrecex 11200  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-nn 12262

This theorem is used by:  nnne0  12298  nnadddir  12320  uzwo3  12996  modmulnn  13954  bernneq3  14299  expmulnbnd  14303  expnngt1b  14310  facwordi  14357  faclbnd  14358  faclbnd2  14359  faclbnd3  14360  faclbnd5  14366  faclbnd6  14367  facubnd  14368  facavg  14369  bcp1nk  14385  hashf1  14526  swrds2  15015  isercolllem1  15756  isercoll  15759  o1fsum  15904  climcndslem1  15942  climcndslem2  15943  climcnds  15944  eftabs  16167  efcllem  16169  ege2le3  16182  efcj  16184  eftlub  16203  eflegeo  16215  eirrlem  16298  fzm1ndvds  16418  nno  16478  nnoddm1d2  16482  bitsfzolem  16530  bitsfzo  16531  bitsinv1lem  16537  sadcaddlem  16553  smueqlem  16586  bezoutlem3  16637  bezoutlem4  16638  sqgcd  16658  nn0expgcd  16660  lcmgcdlem  16702  lcmf  16729  prmind2  16781  coprm  16808  prmfac1  16817  prmndvdsfaclt  16822  divdenle  16846  qnumgt0  16847  zsqrtelqelz  16855  hashdvds  16872  eulerthlem2  16879  odzdvds  16893  vfermltl  16899  modprm0  16903  pythagtriplem11  16923  pythagtriplem13  16925  pythagtriplem19  16931  pclem  16936  pcpre1  16940  pcidlem  16970  dvdsprmpweqle  16984  pcadd  16987  pcmpt  16990  pcmpt2  16991  pcfaclem  16996  pcfac  16997  qexpz  16999  pockthlem  17003  pockthg  17004  prmreclem1  17014  prmreclem3  17016  prmreclem4  17017  prmreclem5  17018  1arithlem4  17024  1arith  17025  4sqlem5  17040  4sqlem6  17041  4sqlem10  17045  mul4sqlem  17051  4sqlem11  17053  4sqlem12  17054  4sqlem13  17055  4sqlem14  17056  4sqlem15  17057  4sqlem16  17058  4sqlem17  17059  vdwlem1  17079  vdwlem3  17081  vdwlem6  17084  vdwlem9  17087  vdwlem10  17088  vdwlem12  17090  vdwnnlem3  17095  ramub1lem1  17124  prmolefac  17144  prmgaplem4  17152  prmgaplem5  17153  prmgaplem6  17154  prmgaplem8  17156  2expltfac  17190  cshwshashnsame  17201  setsstruct2  17272  chnub  18716  psgnunilem4  19630  mndodconglem  19674  oddvds  19680  sylow1lem1  19731  sylow1lem5  19735  fislw  19758  efgredlem  19880  gexexlem  19985  zringlpirlem3  21683  prmirredlem  21691  fvmptnn04if  23080  fvmptnn04ifb  23082  fvmptnn04ifc  23083  fvmptnn04ifd  23084  chfacfisf  23085  chfacfisfcpmat  23086  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  lebnumii  25200  lmnn  25497  ovolunlem1a  25730  ovoliunlem1  25736  ovolicc2lem3  25753  ovolicc2lem4  25754  iundisj  25782  voliunlem1  25784  uniioombllem3  25819  dyadf  25825  dyadovol  25827  dyaddisjlem  25829  dyadmaxlem  25831  opnmbllem  25835  vitalilem4  25845  mbfi1fseqlem1  25949  mbfi1fseqlem3  25951  mbfi1fseqlem4  25952  mbfi1fseqlem5  25953  mbfi1fseqlem6  25954  itg2gt0  25994  itg2cnlem2  25996  dgreq0  26498  dgrco  26508  elqaalem2  26559  aaliou3lem2  26586  aaliou3lem8  26588  aaliou3lem9  26593  rtprmirr  27005  leibpi  27187  log2tlbnd  27190  birthdaylem3  27198  amgm  27235  emcllem2  27241  harmonicbnd4  27255  lgamgulmlem1  27273  lgamgulmlem2  27274  lgamgulmlem3  27275  lgamgulmlem4  27276  lgamgulmlem5  27277  lgamgulmlem6  27278  lgamucov  27282  lgamcvg2  27299  wilthlem1  27312  ftalem5  27321  basellem1  27325  basellem2  27326  basellem3  27327  basellem4  27328  basellem5  27329  basellem6  27330  basellem8  27332  chtge0  27356  chtwordi  27400  vma1  27410  dvdsflf1o  27431  dvdsflsumcom  27432  fsumfldivdiaglem  27433  sgmmul  27445  chtublem  27455  fsumvma2  27458  logfac2  27461  chpchtsum  27463  chpub  27464  logfaclbnd  27466  logexprlim  27469  mersenne  27471  perfectlem2  27474  dchrelbas4  27487  bposlem1  27528  bposlem2  27529  bposlem3  27530  bposlem4  27531  bposlem5  27532  bposlem6  27533  bposlem7  27534  bposlem9  27536  lgslem1  27541  lgsval2lem  27551  lgsdirprm  27575  lgsdir  27576  lgsne0  27579  lgsqrlem2  27591  gausslemma2dlem0h  27607  gausslemma2dlem0i  27608  gausslemma2dlem1a  27609  gausslemma2dlem2  27611  gausslemma2dlem7  27617  gausslemma2d  27618  lgseisenlem1  27619  lgseisenlem2  27620  lgseisenlem3  27621  lgseisenlem4  27622  lgseisen  27623  lgsquadlem1  27624  lgsquadlem2  27625  lgsquadlem3  27626  2sqlem3  27664  2sqlem8  27670  2sqblem  27675  2sqmod  27680  chebbnd1lem1  27713  chebbnd1lem3  27715  chtppilimlem1  27717  rplogsumlem1  27728  rplogsumlem2  27729  dchrisum0lem1a  27730  rpvmasumlem  27731  dchrisumlema  27732  dchrisumlem1  27733  dchrisumlem2  27734  dchrisumlem3  27735  dchrvmasumiflem1  27745  dchrisum0flblem2  27753  dchrisum0re  27757  dchrisum0lem1b  27759  dchrisum0lem1  27760  dirith2  27772  selbergb  27793  selberg2lem  27794  logdivbnd  27800  selberg3lem2  27802  selberg4lem1  27804  pntrsumo1  27809  pntrsumbnd2  27811  pntrlog2bndlem1  27821  pntrlog2bndlem2  27822  pntrlog2bndlem3  27823  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  pntpbnd1a  27829  pntpbnd1  27830  pntibndlem2a  27834  pntibndlem2  27835  pntlemg  27842  pntlemh  27843  pntlemj  27847  pntlemf  27849  ostth2lem1  27862  padicabvf  27875  padicabvcxp  27876  ostth2lem2  27878  ostth2lem3  27879  ostth2lem4  27880  ostth2  27881  ostth3  27882  numclwwlk5  30876  numclwwlk7  30879  nrt2irr  30961  ubthlem2  31360  minvecolem4  31369  iundisjf  33070  ssnnssfz  33266  iundisjfi  33275  nexple  33311  2exple2exp  33312  pfxlsw2ccat  33400  pmtrto1cl  33547  psgnfzto1stlem  33548  fzto1st1  33550  fzto1st  33551  psgnfzto1st  33553  cycpmco2lem6  33579  cycpmco2lem7  33580  fldextrspundgdvdslem  34198  fldextrspundgdvds  34199  fldext2rspun  34200  smatrcl  34314  smattr  34317  smatbl  34318  smatbr  34319  1smat1  34322  submateqlem1  34325  submateqlem2  34326  submateq  34327  esumcst  34581  fiunelros  34693  oddpwdc  34873  eulerpartlems  34879  eulerpartlemgc  34881  fiblem  34917  dstfrvunirn  34994  dstfrvclim1  34997  ballotlemimin  35025  fsum2dsub  35123  reprinfz1  35138  hgt750lemd  35164  hgt750lemb  35172  hgt750leme  35174  tgoldbachgtde  35176  tgoldbachgt  35179  subfaclim  35775  subfacval3  35776  erdszelem7  35784  erdszelem8  35785  erdsze2lem2  35791  cvmliftlem2  35873  cvmliftlem6  35877  cvmliftlem7  35878  cvmliftlem8  35879  cvmliftlem9  35880  cvmliftlem10  35881  cvmliftlem13  35883  bcprod  36325  bccolsum  36326  faclimlem2  36331  faclim2  36335  nn0prpwlem  36949  knoppcnlem10  37207  knoppndvlem15  37231  knoppndvlem17  37233  knoppndvlem18  37234  knoppndvlem19  37235  knoppndvlem20  37236  knoppndvlem21  37237  poimirlem3  38380  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem9  38386  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem13  38390  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem26  38403  poimirlem28  38405  opnmbllem0  38413  mblfinlem2  38415  incsequz  38506  nninfnub  38509  lcmineqlem4  42906  lcmineqlem10  42912  lcmineqlem11  42913  lcmineqlem15  42917  lcmineqlem18  42920  lcmineqlem19  42921  lcmineqlem20  42922  lcmineqlem21  42923  lcmineqlem22  42924  lcmineqlem23  42925  lcmineqlem  42926  3lexlogpow5ineq2  42929  3lexlogpow5ineq4  42930  3lexlogpow2ineq2  42933  3lexlogpow5ineq5  42934  aks4d1p1p3  42943  aks4d1p1p2  42944  aks4d1p1p4  42945  aks4d1p1p5  42949  aks4d1p1  42950  aks4d1p3  42952  aks4d1p4  42953  aks4d1p5  42954  aks4d1p6  42955  aks4d1p7  42957  aks4d1p8d2  42959  aks4d1p8  42961  aks4d1p9  42962  posbezout  42974  primrootlekpowne0  42979  primrootspoweq0  42980  aks6d1c1  42990  hashscontpow1  42995  aks6d1c3  42997  aks6d1c4  42998  aks6d1c2lem4  43001  aks6d1c2  43004  aks6d1c5lem1  43010  2ap1caineq  43019  sticksstones1  43020  sticksstones2  43021  sticksstones3  43022  sticksstones6  43025  sticksstones7  43026  sticksstones10  43029  sticksstones12a  43031  sticksstones12  43032  aks6d1c6lem4  43047  bcled  43052  bcle2d  43053  aks6d1c7lem1  43054  aks6d1c7lem2  43055  unitscyglem1  43069  unitscyglem2  43070  unitscyglem4  43072  unitscyglem5  43073  aks5lem8  43075  oexpreposd  43205  fimgmcyclem  43423  fimgmcyc  43424  flt4lem5e  43510  flt4lem6  43512  flt4lem7  43513  fltltc  43515  fltnltalem  43516  fltnlta  43517  3cubeslem3r  43540  irrapxlem3  43673  irrapxlem4  43674  irrapxlem5  43675  pellexlem2  43679  pellexlem6  43683  pell14qrgt0  43708  pell14qrgapw  43725  pellfundgt1  43732  rmspecsqrtnq  43755  ltrmxnn0  43798  jm3.1lem1  43866  jm3.1lem3  43868  dgraa0p  43998  hashnzfz2  45153  rfcnnnub  45878  nnxrd  46115  fzisoeu  46141  fsumnncl  46410  sumnnodd  46468  limsup10exlem  46608  stoweidlem1  46837  stoweidlem3  46839  stoweidlem11  46847  stoweidlem17  46853  stoweidlem20  46856  stoweidlem25  46861  stoweidlem26  46862  stoweidlem34  46870  stoweidlem38  46874  stoweidlem42  46878  stoweidlem44  46880  stoweidlem51  46887  stoweidlem59  46895  stoweidlem60  46896  wallispi  46906  wallispi2  46909  stirlinglem3  46912  stirlinglem4  46913  stirlinglem8  46917  stirlinglem10  46919  stirlinglem12  46921  stirlinglem15  46924  dirkertrigeqlem2  46935  dirkertrigeqlem3  46936  dirkercncflem2  46940  fourierdlem11  46954  fourierdlem14  46957  fourierdlem15  46958  fourierdlem20  46963  fourierdlem31  46974  fourierdlem64  47006  fourierdlem93  47035  fourierdlem95  47037  fourierdlem103  47045  fourierdlem104  47046  fourierdlem112  47054  sqwvfourb  47065  etransclem3  47073  etransclem19  47089  etransclem23  47093  etransclem24  47094  etransclem25  47095  etransclem32  47102  etransclem35  47105  etransclem41  47111  etransclem48  47118  qndenserrnbllem  47130  hoiqssbllem1  47458  hoiqssbllem2  47459  ovolval5lem1  47488  ovolval5lem2  47489  iccpartlt  48332  iccpartgt  48335  odz2prm2pw  48474  fmtnoprmfac1lem  48475  2pwp1prm  48500  sfprmdvdsmersenne  48514  lighneallem2  48517  proththdlem  48524  perfectALTVlem2  48646  gbowge7  48687  ztprmneprm  49285  pgrple2abl  49303  logbpw2m1  49505  nnpw2pmod  49521  nnolog2flm1  49528  blennngt2o2  49530  itcovalt2lem2lem1  49611