Theorem nnred 12147

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11012  ℕcn 12132

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-i2m1 11081  ax-1ne0 11082  ax-rrecex 11085  ax-cnre 11086

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-nn 12133

This theorem is referenced by:  nnne0  12166  uzwo3  12843  modmulnn  13795  bernneq3  14140  expmulnbnd  14144  expnngt1b  14151  facwordi  14198  faclbnd  14199  faclbnd2  14200  faclbnd3  14201  faclbnd5  14207  faclbnd6  14208  facubnd  14209  facavg  14210  bcp1nk  14226  hashf1  14366  swrds2  14849  isercolllem1  15574  isercoll  15577  o1fsum  15722  climcndslem1  15758  climcndslem2  15759  climcnds  15760  eftabs  15984  efcllem  15986  ege2le3  15999  efcj  16001  eftlub  16020  eflegeo  16032  eirrlem  16115  fzm1ndvds  16235  nno  16295  nnoddm1d2  16299  bitsfzolem  16347  bitsfzo  16348  bitsinv1lem  16354  sadcaddlem  16370  smueqlem  16403  bezoutlem3  16454  bezoutlem4  16455  sqgcd  16475  nn0expgcd  16477  lcmgcdlem  16519  lcmf  16546  prmind2  16598  coprm  16624  prmfac1  16633  prmndvdsfaclt  16638  divdenle  16662  qnumgt0  16663  zsqrtelqelz  16671  hashdvds  16688  eulerthlem2  16695  odzdvds  16709  vfermltl  16715  modprm0  16719  pythagtriplem11  16739  pythagtriplem13  16741  pythagtriplem19  16747  pclem  16752  pcpre1  16756  pcidlem  16786  dvdsprmpweqle  16800  pcadd  16803  pcmpt  16806  pcmpt2  16807  pcfaclem  16812  pcfac  16813  qexpz  16815  pockthlem  16819  pockthg  16820  prmreclem1  16830  prmreclem3  16832  prmreclem4  16833  prmreclem5  16834  1arithlem4  16840  1arith  16841  4sqlem5  16856  4sqlem6  16857  4sqlem10  16861  mul4sqlem  16867  4sqlem11  16869  4sqlem12  16870  4sqlem13  16871  4sqlem14  16872  4sqlem15  16873  4sqlem16  16874  4sqlem17  16875  vdwlem1  16895  vdwlem3  16897  vdwlem6  16900  vdwlem9  16903  vdwlem10  16904  vdwlem12  16906  vdwnnlem3  16911  ramub1lem1  16940  prmolefac  16960  prmgaplem4  16968  prmgaplem5  16969  prmgaplem6  16970  prmgaplem8  16972  2expltfac  17006  cshwshashnsame  17017  setsstruct2  17087  chnub  18530  psgnunilem4  19411  mndodconglem  19455  oddvds  19461  sylow1lem1  19512  sylow1lem5  19516  fislw  19539  efgredlem  19661  gexexlem  19766  zringlpirlem3  21403  prmirredlem  21411  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  30370  numclwwlk7  30373  nrt2irr  30455  ubthlem2  30853  minvecolem4  30862  iundisjf  32571  ssnnssfz  32774  iundisjfi  32783  nexple  32832  2exple2exp  32833  pfxlsw2ccat  32938  pmtrto1cl  33075  psgnfzto1stlem  33076  fzto1st1  33078  fzto1st  33079  psgnfzto1st  33081  cycpmco2lem6  33107  cycpmco2lem7  33108  fldextrspundgdvdslem  33714  fldextrspundgdvds  33715  fldext2rspun  33716  smatrcl  33830  smattr  33833  smatbl  33834  smatbr  33835  1smat1  33838  submateqlem1  33841  submateqlem2  33842  submateq  33843  esumcst  34097  fiunelros  34208  oddpwdc  34388  eulerpartlems  34394  eulerpartlemgc  34396  fiblem  34432  dstfrvunirn  34509  dstfrvclim1  34512  ballotlemimin  34540  fsum2dsub  34641  reprinfz1  34656  hgt750lemd  34682  hgt750lemb  34690  hgt750leme  34692  tgoldbachgtde  34694  tgoldbachgt  34697  subfaclim  35253  subfacval3  35254  erdszelem7  35262  erdszelem8  35263  erdsze2lem2  35269  cvmliftlem2  35351  cvmliftlem6  35355  cvmliftlem7  35356  cvmliftlem8  35357  cvmliftlem9  35358  cvmliftlem10  35359  cvmliftlem13  35361  bcprod  35803  bccolsum  35804  faclimlem2  35809  faclim2  35813  nn0prpwlem  36387  knoppcnlem10  36567  knoppndvlem15  36591  knoppndvlem17  36593  knoppndvlem18  36594  knoppndvlem19  36595  knoppndvlem20  36596  knoppndvlem21  36597  poimirlem3  37684  poimirlem6  37687  poimirlem7  37688  poimirlem8  37689  poimirlem9  37690  poimirlem10  37691  poimirlem11  37692  poimirlem12  37693  poimirlem13  37694  poimirlem15  37696  poimirlem16  37697  poimirlem17  37698  poimirlem19  37700  poimirlem20  37701  poimirlem21  37702  poimirlem22  37703  poimirlem23  37704  poimirlem26  37707  poimirlem28  37709  opnmbllem0  37717  mblfinlem2  37719  incsequz  37809  nninfnub  37812  lcmineqlem4  42146  lcmineqlem10  42152  lcmineqlem11  42153  lcmineqlem15  42157  lcmineqlem18  42160  lcmineqlem19  42161  lcmineqlem20  42162  lcmineqlem21  42163  lcmineqlem22  42164  lcmineqlem23  42165  lcmineqlem  42166  3lexlogpow5ineq2  42169  3lexlogpow5ineq4  42170  3lexlogpow2ineq2  42173  3lexlogpow5ineq5  42174  aks4d1p1p3  42183  aks4d1p1p2  42184  aks4d1p1p4  42185  aks4d1p1p5  42189  aks4d1p1  42190  aks4d1p3  42192  aks4d1p4  42193  aks4d1p5  42194  aks4d1p6  42195  aks4d1p7  42197  aks4d1p8d2  42199  aks4d1p8  42201  aks4d1p9  42202  posbezout  42214  primrootlekpowne0  42219  primrootspoweq0  42220  aks6d1c1  42230  hashscontpow1  42235  aks6d1c3  42237  aks6d1c4  42238  aks6d1c2lem4  42241  aks6d1c2  42244  aks6d1c5lem1  42250  2ap1caineq  42259  sticksstones1  42260  sticksstones2  42261  sticksstones3  42262  sticksstones6  42265  sticksstones7  42266  sticksstones10  42269  sticksstones12a  42271  sticksstones12  42272  aks6d1c6lem4  42287  bcled  42292  bcle2d  42293  aks6d1c7lem1  42294  aks6d1c7lem2  42295  unitscyglem1  42309  unitscyglem2  42310  unitscyglem4  42312  unitscyglem5  42313  aks5lem8  42315  nnadddir  42389  oexpreposd  42441  fimgmcyclem  42652  fimgmcyc  42653  flt4lem5e  42775  flt4lem6  42777  flt4lem7  42778  fltltc  42780  fltnltalem  42781  fltnlta  42782  3cubeslem3r  42805  irrapxlem3  42942  irrapxlem4  42943  irrapxlem5  42944  pellexlem2  42948  pellexlem6  42952  pell14qrgt0  42977  pell14qrgapw  42994  pellfundgt1  43001  rmspecsqrtnq  43024  ltrmxnn0  43067  jm3.1lem1  43135  jm3.1lem3  43137  dgraa0p  43267  hashnzfz2  44439  rfcnnnub  45158  nnxrd  45400  fzisoeu  45426  fsumnncl  45697  sumnnodd  45755  limsup10exlem  45895  stoweidlem1  46124  stoweidlem3  46126  stoweidlem11  46134  stoweidlem17  46140  stoweidlem20  46143  stoweidlem25  46148  stoweidlem26  46149  stoweidlem34  46157  stoweidlem38  46161  stoweidlem42  46165  stoweidlem44  46167  stoweidlem51  46174  stoweidlem59  46182  stoweidlem60  46183  wallispi  46193  wallispi2  46196  stirlinglem3  46199  stirlinglem4  46200  stirlinglem8  46204  stirlinglem10  46206  stirlinglem12  46208  stirlinglem15  46211  dirkertrigeqlem2  46222  dirkertrigeqlem3  46223  dirkercncflem2  46227  fourierdlem11  46241  fourierdlem14  46244  fourierdlem15  46245  fourierdlem20  46250  fourierdlem31  46261  fourierdlem64  46293  fourierdlem93  46322  fourierdlem95  46324  fourierdlem103  46332  fourierdlem104  46333  fourierdlem112  46341  sqwvfourb  46352  etransclem3  46360  etransclem19  46376  etransclem23  46380  etransclem24  46381  etransclem25  46382  etransclem32  46389  etransclem35  46392  etransclem41  46398  etransclem48  46405  qndenserrnbllem  46417  hoiqssbllem1  46745  hoiqssbllem2  46746  ovolval5lem1  46775  ovolval5lem2  46776  iccpartlt  47549  iccpartgt  47552  odz2prm2pw  47688  fmtnoprmfac1lem  47689  2pwp1prm  47714  sfprmdvdsmersenne  47728  lighneallem2  47731  proththdlem  47738  perfectALTVlem2  47847  gbowge7  47888  ztprmneprm  48472  pgrple2abl  48490  logbpw2m1  48693  nnpw2pmod  48709  nnolog2flm1  48716  blennngt2o2  48718  itcovalt2lem2lem1  48799