Theorem nnred 12187

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11035  ℕcn 12172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-i2m1 11104  ax-1ne0 11105  ax-rrecex 11108  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-nn 12173

This theorem is referenced by:  nnne0  12209  nnadddir  12231  uzwo3  12891  modmulnn  13846  bernneq3  14191  expmulnbnd  14195  expnngt1b  14202  facwordi  14249  faclbnd  14250  faclbnd2  14251  faclbnd3  14252  faclbnd5  14258  faclbnd6  14259  facubnd  14260  facavg  14261  bcp1nk  14277  hashf1  14417  swrds2  14900  isercolllem1  15625  isercoll  15628  o1fsum  15774  climcndslem1  15812  climcndslem2  15813  climcnds  15814  eftabs  16038  efcllem  16040  ege2le3  16053  efcj  16055  eftlub  16074  eflegeo  16086  eirrlem  16169  fzm1ndvds  16289  nno  16349  nnoddm1d2  16353  bitsfzolem  16401  bitsfzo  16402  bitsinv1lem  16408  sadcaddlem  16424  smueqlem  16457  bezoutlem3  16508  bezoutlem4  16509  sqgcd  16529  nn0expgcd  16531  lcmgcdlem  16573  lcmf  16600  prmind2  16652  coprm  16679  prmfac1  16688  prmndvdsfaclt  16693  divdenle  16717  qnumgt0  16718  zsqrtelqelz  16726  hashdvds  16743  eulerthlem2  16750  odzdvds  16764  vfermltl  16770  modprm0  16774  pythagtriplem11  16794  pythagtriplem13  16796  pythagtriplem19  16802  pclem  16807  pcpre1  16811  pcidlem  16841  dvdsprmpweqle  16855  pcadd  16858  pcmpt  16861  pcmpt2  16862  pcfaclem  16867  pcfac  16868  qexpz  16870  pockthlem  16874  pockthg  16875  prmreclem1  16885  prmreclem3  16887  prmreclem4  16888  prmreclem5  16889  1arithlem4  16895  1arith  16896  4sqlem5  16911  4sqlem6  16912  4sqlem10  16916  mul4sqlem  16922  4sqlem11  16924  4sqlem12  16925  4sqlem13  16926  4sqlem14  16927  4sqlem15  16928  4sqlem16  16929  4sqlem17  16930  vdwlem1  16950  vdwlem3  16952  vdwlem6  16955  vdwlem9  16958  vdwlem10  16959  vdwlem12  16961  vdwnnlem3  16966  ramub1lem1  16995  prmolefac  17015  prmgaplem4  17023  prmgaplem5  17024  prmgaplem6  17025  prmgaplem8  17027  2expltfac  17061  cshwshashnsame  17072  setsstruct2  17142  chnub  18586  psgnunilem4  19470  mndodconglem  19514  oddvds  19520  sylow1lem1  19571  sylow1lem5  19575  fislw  19598  efgredlem  19720  gexexlem  19825  zringlpirlem3  21446  prmirredlem  21454  fvmptnn04if  22839  fvmptnn04ifb  22841  fvmptnn04ifc  22842  fvmptnn04ifd  22843  chfacfisf  22844  chfacfisfcpmat  22845  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  lebnumii  24958  lmnn  25255  ovolunlem1a  25488  ovoliunlem1  25494  ovolicc2lem3  25511  ovolicc2lem4  25512  iundisj  25540  voliunlem1  25542  uniioombllem3  25577  dyadf  25583  dyadovol  25585  dyaddisjlem  25587  dyadmaxlem  25589  opnmbllem  25593  vitalilem4  25603  mbfi1fseqlem1  25707  mbfi1fseqlem3  25709  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1fseqlem6  25712  itg2gt0  25752  itg2cnlem2  25754  dgreq0  26255  dgrco  26265  elqaalem2  26311  aaliou3lem2  26334  aaliou3lem8  26336  aaliou3lem9  26341  rtprmirr  26749  leibpi  26931  log2tlbnd  26934  birthdaylem3  26942  amgm  26979  emcllem2  26985  harmonicbnd4  26999  lgamgulmlem1  27017  lgamgulmlem2  27018  lgamgulmlem3  27019  lgamgulmlem4  27020  lgamgulmlem5  27021  lgamgulmlem6  27022  lgamucov  27026  lgamcvg2  27043  wilthlem1  27056  ftalem5  27065  basellem1  27069  basellem2  27070  basellem3  27071  basellem4  27072  basellem5  27073  basellem6  27074  basellem8  27076  chtge0  27100  chtwordi  27144  vma1  27154  dvdsflf1o  27175  dvdsflsumcom  27176  fsumfldivdiaglem  27177  sgmmul  27189  chtublem  27199  fsumvma2  27202  logfac2  27205  chpchtsum  27207  chpub  27208  logfaclbnd  27210  logexprlim  27213  mersenne  27215  perfectlem2  27218  dchrelbas4  27231  bposlem1  27272  bposlem2  27273  bposlem3  27274  bposlem4  27275  bposlem5  27276  bposlem6  27277  bposlem7  27278  bposlem9  27280  lgslem1  27285  lgsval2lem  27295  lgsdirprm  27319  lgsdir  27320  lgsne0  27323  lgsqrlem2  27335  gausslemma2dlem0h  27351  gausslemma2dlem0i  27352  gausslemma2dlem1a  27353  gausslemma2dlem2  27355  gausslemma2dlem7  27361  gausslemma2d  27362  lgseisenlem1  27363  lgseisenlem2  27364  lgseisenlem3  27365  lgseisenlem4  27366  lgseisen  27367  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  2sqlem3  27408  2sqlem8  27414  2sqblem  27419  2sqmod  27424  chebbnd1lem1  27457  chebbnd1lem3  27459  chtppilimlem1  27461  rplogsumlem1  27472  rplogsumlem2  27473  dchrisum0lem1a  27474  rpvmasumlem  27475  dchrisumlema  27476  dchrisumlem1  27477  dchrisumlem2  27478  dchrisumlem3  27479  dchrvmasumiflem1  27489  dchrisum0flblem2  27497  dchrisum0re  27501  dchrisum0lem1b  27503  dchrisum0lem1  27504  dirith2  27516  selbergb  27537  selberg2lem  27538  logdivbnd  27544  selberg3lem2  27546  selberg4lem1  27548  pntrsumo1  27553  pntrsumbnd2  27555  pntrlog2bndlem1  27565  pntrlog2bndlem2  27566  pntrlog2bndlem3  27567  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntpbnd1a  27573  pntpbnd1  27574  pntibndlem2a  27578  pntibndlem2  27579  pntlemg  27586  pntlemh  27587  pntlemj  27591  pntlemf  27593  ostth2lem1  27606  padicabvf  27619  padicabvcxp  27620  ostth2lem2  27622  ostth2lem3  27623  ostth2lem4  27624  ostth2  27625  ostth3  27626  numclwwlk5  30483  numclwwlk7  30486  nrt2irr  30568  ubthlem2  30967  minvecolem4  30976  iundisjf  32685  ssnnssfz  32886  iundisjfi  32895  nexple  32943  2exple2exp  32944  pfxlsw2ccat  33036  pmtrto1cl  33187  psgnfzto1stlem  33188  fzto1st1  33190  fzto1st  33191  psgnfzto1st  33193  cycpmco2lem6  33219  cycpmco2lem7  33220  fldextrspundgdvdslem  33871  fldextrspundgdvds  33872  fldext2rspun  33873  smatrcl  33987  smattr  33990  smatbl  33991  smatbr  33992  1smat1  33995  submateqlem1  33998  submateqlem2  33999  submateq  34000  esumcst  34254  fiunelros  34365  oddpwdc  34545  eulerpartlems  34551  eulerpartlemgc  34553  fiblem  34589  dstfrvunirn  34666  dstfrvclim1  34669  ballotlemimin  34697  fsum2dsub  34798  reprinfz1  34813  hgt750lemd  34839  hgt750lemb  34847  hgt750leme  34849  tgoldbachgtde  34851  tgoldbachgt  34854  subfaclim  35423  subfacval3  35424  erdszelem7  35432  erdszelem8  35433  erdsze2lem2  35439  cvmliftlem2  35521  cvmliftlem6  35525  cvmliftlem7  35526  cvmliftlem8  35527  cvmliftlem9  35528  cvmliftlem10  35529  cvmliftlem13  35531  bcprod  35973  bccolsum  35974  faclimlem2  35979  faclim2  35983  nn0prpwlem  36557  knoppcnlem10  36815  knoppndvlem15  36839  knoppndvlem17  36841  knoppndvlem18  36842  knoppndvlem19  36843  knoppndvlem20  36844  knoppndvlem21  36845  poimirlem3  37997  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem9  38003  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem13  38007  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem23  38017  poimirlem26  38020  poimirlem28  38022  opnmbllem0  38030  mblfinlem2  38032  incsequz  38122  nninfnub  38125  lcmineqlem4  42524  lcmineqlem10  42530  lcmineqlem11  42531  lcmineqlem15  42535  lcmineqlem18  42538  lcmineqlem19  42539  lcmineqlem20  42540  lcmineqlem21  42541  lcmineqlem22  42542  lcmineqlem23  42543  lcmineqlem  42544  3lexlogpow5ineq2  42547  3lexlogpow5ineq4  42548  3lexlogpow2ineq2  42551  3lexlogpow5ineq5  42552  aks4d1p1p3  42561  aks4d1p1p2  42562  aks4d1p1p4  42563  aks4d1p1p5  42567  aks4d1p1  42568  aks4d1p3  42570  aks4d1p4  42571  aks4d1p5  42572  aks4d1p6  42573  aks4d1p7  42575  aks4d1p8d2  42577  aks4d1p8  42579  aks4d1p9  42580  posbezout  42592  primrootlekpowne0  42597  primrootspoweq0  42598  aks6d1c1  42608  hashscontpow1  42613  aks6d1c3  42615  aks6d1c4  42616  aks6d1c2lem4  42619  aks6d1c2  42622  aks6d1c5lem1  42628  2ap1caineq  42637  sticksstones1  42638  sticksstones2  42639  sticksstones3  42640  sticksstones6  42643  sticksstones7  42644  sticksstones10  42647  sticksstones12a  42649  sticksstones12  42650  aks6d1c6lem4  42665  bcled  42670  bcle2d  42671  aks6d1c7lem1  42672  aks6d1c7lem2  42673  unitscyglem1  42687  unitscyglem2  42688  unitscyglem4  42690  unitscyglem5  42691  aks5lem8  42693  oexpreposd  42806  fimgmcyclem  43026  fimgmcyc  43027  flt4lem5e  43113  flt4lem6  43115  flt4lem7  43116  fltltc  43118  fltnltalem  43119  fltnlta  43120  3cubeslem3r  43143  irrapxlem3  43276  irrapxlem4  43277  irrapxlem5  43278  pellexlem2  43282  pellexlem6  43286  pell14qrgt0  43311  pell14qrgapw  43328  pellfundgt1  43335  rmspecsqrtnq  43358  ltrmxnn0  43401  jm3.1lem1  43469  jm3.1lem3  43471  dgraa0p  43601  hashnzfz2  44772  rfcnnnub  45491  nnxrd  45729  fzisoeu  45755  fsumnncl  46024  sumnnodd  46082  limsup10exlem  46222  stoweidlem1  46451  stoweidlem3  46453  stoweidlem11  46461  stoweidlem17  46467  stoweidlem20  46470  stoweidlem25  46475  stoweidlem26  46476  stoweidlem34  46484  stoweidlem38  46488  stoweidlem42  46492  stoweidlem44  46494  stoweidlem51  46501  stoweidlem59  46509  stoweidlem60  46510  wallispi  46520  wallispi2  46523  stirlinglem3  46526  stirlinglem4  46527  stirlinglem8  46531  stirlinglem10  46533  stirlinglem12  46535  stirlinglem15  46538  dirkertrigeqlem2  46549  dirkertrigeqlem3  46550  dirkercncflem2  46554  fourierdlem11  46568  fourierdlem14  46571  fourierdlem15  46572  fourierdlem20  46577  fourierdlem31  46588  fourierdlem64  46620  fourierdlem93  46649  fourierdlem95  46651  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  sqwvfourb  46679  etransclem3  46687  etransclem19  46703  etransclem23  46707  etransclem24  46708  etransclem25  46709  etransclem32  46716  etransclem35  46719  etransclem41  46725  etransclem48  46732  qndenserrnbllem  46744  hoiqssbllem1  47072  hoiqssbllem2  47073  ovolval5lem1  47102  ovolval5lem2  47103  iccpartlt  47906  iccpartgt  47909  odz2prm2pw  48048  fmtnoprmfac1lem  48049  2pwp1prm  48074  sfprmdvdsmersenne  48088  lighneallem2  48091  proththdlem  48098  perfectALTVlem2  48220  gbowge7  48261  ztprmneprm  48845  pgrple2abl  48863  logbpw2m1  49065  nnpw2pmod  49081  nnolog2flm1  49088  blennngt2o2  49090  itcovalt2lem2lem1  49171