Theorem nnred 12140

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11005  ℕcn 12125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-i2m1 11074  ax-1ne0 11075  ax-rrecex 11078  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126

This theorem is referenced by:  nnne0  12159  uzwo3  12841  modmulnn  13793  bernneq3  14138  expmulnbnd  14142  expnngt1b  14149  facwordi  14196  faclbnd  14197  faclbnd2  14198  faclbnd3  14199  faclbnd5  14205  faclbnd6  14206  facubnd  14207  facavg  14208  bcp1nk  14224  hashf1  14364  swrds2  14847  isercolllem1  15572  isercoll  15575  o1fsum  15720  climcndslem1  15756  climcndslem2  15757  climcnds  15758  eftabs  15982  efcllem  15984  ege2le3  15997  efcj  15999  eftlub  16018  eflegeo  16030  eirrlem  16113  fzm1ndvds  16233  nno  16293  nnoddm1d2  16297  bitsfzolem  16345  bitsfzo  16346  bitsinv1lem  16352  sadcaddlem  16368  smueqlem  16401  bezoutlem3  16452  bezoutlem4  16453  sqgcd  16473  nn0expgcd  16475  lcmgcdlem  16517  lcmf  16544  prmind2  16596  coprm  16622  prmfac1  16631  prmndvdsfaclt  16636  divdenle  16660  qnumgt0  16661  zsqrtelqelz  16669  hashdvds  16686  eulerthlem2  16693  odzdvds  16707  vfermltl  16713  modprm0  16717  pythagtriplem11  16737  pythagtriplem13  16739  pythagtriplem19  16745  pclem  16750  pcpre1  16754  pcidlem  16784  dvdsprmpweqle  16798  pcadd  16801  pcmpt  16804  pcmpt2  16805  pcfaclem  16810  pcfac  16811  qexpz  16813  pockthlem  16817  pockthg  16818  prmreclem1  16828  prmreclem3  16830  prmreclem4  16831  prmreclem5  16832  1arithlem4  16838  1arith  16839  4sqlem5  16854  4sqlem6  16855  4sqlem10  16859  mul4sqlem  16865  4sqlem11  16867  4sqlem12  16868  4sqlem13  16869  4sqlem14  16870  4sqlem15  16871  4sqlem16  16872  4sqlem17  16873  vdwlem1  16893  vdwlem3  16895  vdwlem6  16898  vdwlem9  16901  vdwlem10  16902  vdwlem12  16904  vdwnnlem3  16909  ramub1lem1  16938  prmolefac  16958  prmgaplem4  16966  prmgaplem5  16967  prmgaplem6  16968  prmgaplem8  16970  2expltfac  17004  cshwshashnsame  17015  setsstruct2  17085  chnub  18528  psgnunilem4  19410  mndodconglem  19454  oddvds  19460  sylow1lem1  19511  sylow1lem5  19515  fislw  19538  efgredlem  19660  gexexlem  19765  zringlpirlem3  21402  prmirredlem  21410  fvmptnn04if  22765  fvmptnn04ifb  22767  fvmptnn04ifc  22768  fvmptnn04ifd  22769  chfacfisf  22770  chfacfisfcpmat  22771  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  lebnumii  24893  lmnn  25191  ovolunlem1a  25425  ovoliunlem1  25431  ovolicc2lem3  25448  ovolicc2lem4  25449  iundisj  25477  voliunlem1  25479  uniioombllem3  25514  dyadf  25520  dyadovol  25522  dyaddisjlem  25524  dyadmaxlem  25526  opnmbllem  25530  vitalilem4  25540  mbfi1fseqlem1  25644  mbfi1fseqlem3  25646  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1fseqlem6  25649  itg2gt0  25689  itg2cnlem2  25691  dgreq0  26199  dgrco  26209  elqaalem2  26256  aaliou3lem2  26279  aaliou3lem8  26281  aaliou3lem9  26286  rtprmirr  26698  leibpi  26880  log2tlbnd  26883  birthdaylem3  26891  amgm  26929  emcllem2  26935  harmonicbnd4  26949  lgamgulmlem1  26967  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem4  26970  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamucov  26976  lgamcvg2  26993  wilthlem1  27006  ftalem5  27015  basellem1  27019  basellem2  27020  basellem3  27021  basellem4  27022  basellem5  27023  basellem6  27024  basellem8  27026  chtge0  27050  chtwordi  27094  vma1  27104  dvdsflf1o  27125  dvdsflsumcom  27126  fsumfldivdiaglem  27127  sgmmul  27140  chtublem  27150  fsumvma2  27153  logfac2  27156  chpchtsum  27158  chpub  27159  logfaclbnd  27161  logexprlim  27164  mersenne  27166  perfectlem2  27169  dchrelbas4  27182  bposlem1  27223  bposlem2  27224  bposlem3  27225  bposlem4  27226  bposlem5  27227  bposlem6  27228  bposlem7  27229  bposlem9  27231  lgslem1  27236  lgsval2lem  27246  lgsdirprm  27270  lgsdir  27271  lgsne0  27274  lgsqrlem2  27286  gausslemma2dlem0h  27302  gausslemma2dlem0i  27303  gausslemma2dlem1a  27304  gausslemma2dlem2  27306  gausslemma2dlem7  27312  gausslemma2d  27313  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem3  27316  lgseisenlem4  27317  lgseisen  27318  lgsquadlem1  27319  lgsquadlem2  27320  lgsquadlem3  27321  2sqlem3  27359  2sqlem8  27365  2sqblem  27370  2sqmod  27375  chebbnd1lem1  27408  chebbnd1lem3  27410  chtppilimlem1  27412  rplogsumlem1  27423  rplogsumlem2  27424  dchrisum0lem1a  27425  rpvmasumlem  27426  dchrisumlema  27427  dchrisumlem1  27428  dchrisumlem2  27429  dchrisumlem3  27430  dchrvmasumiflem1  27440  dchrisum0flblem2  27448  dchrisum0re  27452  dchrisum0lem1b  27454  dchrisum0lem1  27455  dirith2  27467  selbergb  27488  selberg2lem  27489  logdivbnd  27495  selberg3lem2  27497  selberg4lem1  27499  pntrsumo1  27504  pntrsumbnd2  27506  pntrlog2bndlem1  27516  pntrlog2bndlem2  27517  pntrlog2bndlem3  27518  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntpbnd1a  27524  pntpbnd1  27525  pntibndlem2a  27529  pntibndlem2  27530  pntlemg  27537  pntlemh  27538  pntlemj  27542  pntlemf  27544  ostth2lem1  27557  padicabvf  27570  padicabvcxp  27571  ostth2lem2  27573  ostth2lem3  27574  ostth2lem4  27575  ostth2  27576  ostth3  27577  numclwwlk5  30366  numclwwlk7  30369  nrt2irr  30451  ubthlem2  30849  minvecolem4  30858  iundisjf  32567  ssnnssfz  32768  iundisjfi  32776  nexple  32825  2exple2exp  32826  pfxlsw2ccat  32929  pmtrto1cl  33066  psgnfzto1stlem  33067  fzto1st1  33069  fzto1st  33070  psgnfzto1st  33072  cycpmco2lem6  33098  cycpmco2lem7  33099  fldextrspundgdvdslem  33691  fldextrspundgdvds  33692  fldext2rspun  33693  smatrcl  33807  smattr  33810  smatbl  33811  smatbr  33812  1smat1  33815  submateqlem1  33818  submateqlem2  33819  submateq  33820  esumcst  34074  fiunelros  34185  oddpwdc  34365  eulerpartlems  34371  eulerpartlemgc  34373  fiblem  34409  dstfrvunirn  34486  dstfrvclim1  34489  ballotlemimin  34517  fsum2dsub  34618  reprinfz1  34633  hgt750lemd  34659  hgt750lemb  34667  hgt750leme  34669  tgoldbachgtde  34671  tgoldbachgt  34674  subfaclim  35230  subfacval3  35231  erdszelem7  35239  erdszelem8  35240  erdsze2lem2  35246  cvmliftlem2  35328  cvmliftlem6  35332  cvmliftlem7  35333  cvmliftlem8  35334  cvmliftlem9  35335  cvmliftlem10  35336  cvmliftlem13  35338  bcprod  35780  bccolsum  35781  faclimlem2  35786  faclim2  35790  nn0prpwlem  36362  knoppcnlem10  36542  knoppndvlem15  36566  knoppndvlem17  36568  knoppndvlem18  36569  knoppndvlem19  36570  knoppndvlem20  36571  knoppndvlem21  36572  poimirlem3  37669  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem9  37675  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem13  37679  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem23  37689  poimirlem26  37692  poimirlem28  37694  opnmbllem0  37702  mblfinlem2  37704  incsequz  37794  nninfnub  37797  lcmineqlem4  42071  lcmineqlem10  42077  lcmineqlem11  42078  lcmineqlem15  42082  lcmineqlem18  42085  lcmineqlem19  42086  lcmineqlem20  42087  lcmineqlem21  42088  lcmineqlem22  42089  lcmineqlem23  42090  lcmineqlem  42091  3lexlogpow5ineq2  42094  3lexlogpow5ineq4  42095  3lexlogpow2ineq2  42098  3lexlogpow5ineq5  42099  aks4d1p1p3  42108  aks4d1p1p2  42109  aks4d1p1p4  42110  aks4d1p1p5  42114  aks4d1p1  42115  aks4d1p3  42117  aks4d1p4  42118  aks4d1p5  42119  aks4d1p6  42120  aks4d1p7  42122  aks4d1p8d2  42124  aks4d1p8  42126  aks4d1p9  42127  posbezout  42139  primrootlekpowne0  42144  primrootspoweq0  42145  aks6d1c1  42155  hashscontpow1  42160  aks6d1c3  42162  aks6d1c4  42163  aks6d1c2lem4  42166  aks6d1c2  42169  aks6d1c5lem1  42175  2ap1caineq  42184  sticksstones1  42185  sticksstones2  42186  sticksstones3  42187  sticksstones6  42190  sticksstones7  42191  sticksstones10  42194  sticksstones12a  42196  sticksstones12  42197  aks6d1c6lem4  42212  bcled  42217  bcle2d  42218  aks6d1c7lem1  42219  aks6d1c7lem2  42220  unitscyglem1  42234  unitscyglem2  42235  unitscyglem4  42237  unitscyglem5  42238  aks5lem8  42240  nnadddir  42309  oexpreposd  42361  fimgmcyclem  42572  fimgmcyc  42573  flt4lem5e  42695  flt4lem6  42697  flt4lem7  42698  fltltc  42700  fltnltalem  42701  fltnlta  42702  3cubeslem3r  42726  irrapxlem3  42863  irrapxlem4  42864  irrapxlem5  42865  pellexlem2  42869  pellexlem6  42873  pell14qrgt0  42898  pell14qrgapw  42915  pellfundgt1  42922  rmspecsqrtnq  42945  ltrmxnn0  42988  jm3.1lem1  43056  jm3.1lem3  43058  dgraa0p  43188  hashnzfz2  44360  rfcnnnub  45079  nnxrd  45321  fzisoeu  45347  fsumnncl  45618  sumnnodd  45676  limsup10exlem  45816  stoweidlem1  46045  stoweidlem3  46047  stoweidlem11  46055  stoweidlem17  46061  stoweidlem20  46064  stoweidlem25  46069  stoweidlem26  46070  stoweidlem34  46078  stoweidlem38  46082  stoweidlem42  46086  stoweidlem44  46088  stoweidlem51  46095  stoweidlem59  46103  stoweidlem60  46104  wallispi  46114  wallispi2  46117  stirlinglem3  46120  stirlinglem4  46121  stirlinglem8  46125  stirlinglem10  46127  stirlinglem12  46129  stirlinglem15  46132  dirkertrigeqlem2  46143  dirkertrigeqlem3  46144  dirkercncflem2  46148  fourierdlem11  46162  fourierdlem14  46165  fourierdlem15  46166  fourierdlem20  46171  fourierdlem31  46182  fourierdlem64  46214  fourierdlem93  46243  fourierdlem95  46245  fourierdlem103  46253  fourierdlem104  46254  fourierdlem112  46262  sqwvfourb  46273  etransclem3  46281  etransclem19  46297  etransclem23  46301  etransclem24  46302  etransclem25  46303  etransclem32  46310  etransclem35  46313  etransclem41  46319  etransclem48  46326  qndenserrnbllem  46338  hoiqssbllem1  46666  hoiqssbllem2  46667  ovolval5lem1  46696  ovolval5lem2  46697  iccpartlt  47461  iccpartgt  47464  odz2prm2pw  47600  fmtnoprmfac1lem  47601  2pwp1prm  47626  sfprmdvdsmersenne  47640  lighneallem2  47643  proththdlem  47650  perfectALTVlem2  47759  gbowge7  47800  ztprmneprm  48384  pgrple2abl  48402  logbpw2m1  48605  nnpw2pmod  48621  nnolog2flm1  48628  blennngt2o2  48630  itcovalt2lem2lem1  48711