Theorem nnred 12249

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11100  ℕcn 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-i2m1 11169  ax-1ne0 11170  ax-rrecex 11173  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-nn 12235

This theorem is referenced by:  nnne0  12271  nnadddir  12293  uzwo3  12968  modmulnn  13924  bernneq3  14269  expmulnbnd  14273  expnngt1b  14280  facwordi  14327  faclbnd  14328  faclbnd2  14329  faclbnd3  14330  faclbnd5  14336  faclbnd6  14337  facubnd  14338  facavg  14339  bcp1nk  14355  hashf1  14496  swrds2  14979  isercolllem1  15718  isercoll  15721  o1fsum  15867  climcndslem1  15905  climcndslem2  15906  climcnds  15907  eftabs  16130  efcllem  16132  ege2le3  16145  efcj  16147  eftlub  16166  eflegeo  16178  eirrlem  16261  fzm1ndvds  16381  nno  16441  nnoddm1d2  16445  bitsfzolem  16493  bitsfzo  16494  bitsinv1lem  16500  sadcaddlem  16516  smueqlem  16549  bezoutlem3  16600  bezoutlem4  16601  sqgcd  16621  nn0expgcd  16623  lcmgcdlem  16665  lcmf  16692  prmind2  16744  coprm  16771  prmfac1  16780  prmndvdsfaclt  16785  divdenle  16809  qnumgt0  16810  zsqrtelqelz  16818  hashdvds  16835  eulerthlem2  16842  odzdvds  16856  vfermltl  16862  modprm0  16866  pythagtriplem11  16886  pythagtriplem13  16888  pythagtriplem19  16894  pclem  16899  pcpre1  16903  pcidlem  16933  dvdsprmpweqle  16947  pcadd  16950  pcmpt  16953  pcmpt2  16954  pcfaclem  16959  pcfac  16960  qexpz  16962  pockthlem  16966  pockthg  16967  prmreclem1  16977  prmreclem3  16979  prmreclem4  16980  prmreclem5  16981  1arithlem4  16987  1arith  16988  4sqlem5  17003  4sqlem6  17004  4sqlem10  17008  mul4sqlem  17014  4sqlem11  17016  4sqlem12  17017  4sqlem13  17018  4sqlem14  17019  4sqlem15  17020  4sqlem16  17021  4sqlem17  17022  vdwlem1  17042  vdwlem3  17044  vdwlem6  17047  vdwlem9  17050  vdwlem10  17051  vdwlem12  17053  vdwnnlem3  17058  ramub1lem1  17087  prmolefac  17107  prmgaplem4  17115  prmgaplem5  17116  prmgaplem6  17117  prmgaplem8  17119  2expltfac  17153  cshwshashnsame  17164  setsstruct2  17235  chnub  18679  psgnunilem4  19568  mndodconglem  19612  oddvds  19618  sylow1lem1  19669  sylow1lem5  19673  fislw  19696  efgredlem  19818  gexexlem  19923  zringlpirlem3  21595  prmirredlem  21603  fvmptnn04if  22987  fvmptnn04ifb  22989  fvmptnn04ifc  22990  fvmptnn04ifd  22991  chfacfisf  22992  chfacfisfcpmat  22993  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  lebnumii  25106  lmnn  25403  ovolunlem1a  25636  ovoliunlem1  25642  ovolicc2lem3  25659  ovolicc2lem4  25660  iundisj  25688  voliunlem1  25690  uniioombllem3  25725  dyadf  25731  dyadovol  25733  dyaddisjlem  25735  dyadmaxlem  25737  opnmbllem  25741  vitalilem4  25751  mbfi1fseqlem1  25855  mbfi1fseqlem3  25857  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  mbfi1fseqlem6  25860  itg2gt0  25900  itg2cnlem2  25902  dgreq0  26403  dgrco  26413  elqaalem2  26462  aaliou3lem2  26485  aaliou3lem8  26487  aaliou3lem9  26492  rtprmirr  26903  leibpi  27085  log2tlbnd  27088  birthdaylem3  27096  amgm  27133  emcllem2  27139  harmonicbnd4  27153  lgamgulmlem1  27171  lgamgulmlem2  27172  lgamgulmlem3  27173  lgamgulmlem4  27174  lgamgulmlem5  27175  lgamgulmlem6  27176  lgamucov  27180  lgamcvg2  27197  wilthlem1  27210  ftalem5  27219  basellem1  27223  basellem2  27224  basellem3  27225  basellem4  27226  basellem5  27227  basellem6  27228  basellem8  27230  chtge0  27254  chtwordi  27298  vma1  27308  dvdsflf1o  27329  dvdsflsumcom  27330  fsumfldivdiaglem  27331  sgmmul  27343  chtublem  27353  fsumvma2  27356  logfac2  27359  chpchtsum  27361  chpub  27362  logfaclbnd  27364  logexprlim  27367  mersenne  27369  perfectlem2  27372  dchrelbas4  27385  bposlem1  27426  bposlem2  27427  bposlem3  27428  bposlem4  27429  bposlem5  27430  bposlem6  27431  bposlem7  27432  bposlem9  27434  lgslem1  27439  lgsval2lem  27449  lgsdirprm  27473  lgsdir  27474  lgsne0  27477  lgsqrlem2  27489  gausslemma2dlem0h  27505  gausslemma2dlem0i  27506  gausslemma2dlem1a  27507  gausslemma2dlem2  27509  gausslemma2dlem7  27515  gausslemma2d  27516  lgseisenlem1  27517  lgseisenlem2  27518  lgseisenlem3  27519  lgseisenlem4  27520  lgseisen  27521  lgsquadlem1  27522  lgsquadlem2  27523  lgsquadlem3  27524  2sqlem3  27562  2sqlem8  27568  2sqblem  27573  2sqmod  27578  chebbnd1lem1  27611  chebbnd1lem3  27613  chtppilimlem1  27615  rplogsumlem1  27626  rplogsumlem2  27627  dchrisum0lem1a  27628  rpvmasumlem  27629  dchrisumlema  27630  dchrisumlem1  27631  dchrisumlem2  27632  dchrisumlem3  27633  dchrvmasumiflem1  27643  dchrisum0flblem2  27651  dchrisum0re  27655  dchrisum0lem1b  27657  dchrisum0lem1  27658  dirith2  27670  selbergb  27691  selberg2lem  27692  logdivbnd  27698  selberg3lem2  27700  selberg4lem1  27702  pntrsumo1  27707  pntrsumbnd2  27709  pntrlog2bndlem1  27719  pntrlog2bndlem2  27720  pntrlog2bndlem3  27721  pntrlog2bndlem4  27722  pntrlog2bndlem5  27723  pntpbnd1a  27727  pntpbnd1  27728  pntibndlem2a  27732  pntibndlem2  27733  pntlemg  27740  pntlemh  27741  pntlemj  27745  pntlemf  27747  ostth2lem1  27760  padicabvf  27773  padicabvcxp  27774  ostth2lem2  27776  ostth2lem3  27777  ostth2lem4  27778  ostth2  27779  ostth3  27780  numclwwlk5  30717  numclwwlk7  30720  nrt2irr  30802  ubthlem2  31201  minvecolem4  31210  iundisjf  32912  ssnnssfz  33110  iundisjfi  33119  nexple  33155  2exple2exp  33156  pfxlsw2ccat  33248  pmtrto1cl  33397  psgnfzto1stlem  33398  fzto1st1  33400  fzto1st  33401  psgnfzto1st  33403  cycpmco2lem6  33429  cycpmco2lem7  33430  fldextrspundgdvdslem  34048  fldextrspundgdvds  34049  fldext2rspun  34050  smatrcl  34164  smattr  34167  smatbl  34168  smatbr  34169  1smat1  34172  submateqlem1  34175  submateqlem2  34176  submateq  34177  esumcst  34431  fiunelros  34542  oddpwdc  34722  eulerpartlems  34728  eulerpartlemgc  34730  fiblem  34766  dstfrvunirn  34843  dstfrvclim1  34846  ballotlemimin  34874  fsum2dsub  34972  reprinfz1  34987  hgt750lemd  35013  hgt750lemb  35021  hgt750leme  35023  tgoldbachgtde  35025  tgoldbachgt  35028  subfaclim  35658  subfacval3  35659  erdszelem7  35667  erdszelem8  35668  erdsze2lem2  35674  cvmliftlem2  35756  cvmliftlem6  35760  cvmliftlem7  35761  cvmliftlem8  35762  cvmliftlem9  35763  cvmliftlem10  35764  cvmliftlem13  35766  bcprod  36208  bccolsum  36209  faclimlem2  36214  faclim2  36218  nn0prpwlem  36811  knoppcnlem10  37069  knoppndvlem15  37093  knoppndvlem17  37095  knoppndvlem18  37096  knoppndvlem19  37097  knoppndvlem20  37098  knoppndvlem21  37099  poimirlem3  38252  poimirlem6  38255  poimirlem7  38256  poimirlem8  38257  poimirlem9  38258  poimirlem10  38259  poimirlem11  38260  poimirlem12  38261  poimirlem13  38262  poimirlem15  38264  poimirlem16  38265  poimirlem17  38266  poimirlem19  38268  poimirlem20  38269  poimirlem21  38270  poimirlem22  38271  poimirlem23  38272  poimirlem26  38275  poimirlem28  38277  opnmbllem0  38285  mblfinlem2  38287  incsequz  38377  nninfnub  38380  lcmineqlem4  42777  lcmineqlem10  42783  lcmineqlem11  42784  lcmineqlem15  42788  lcmineqlem18  42791  lcmineqlem19  42792  lcmineqlem20  42793  lcmineqlem21  42794  lcmineqlem22  42795  lcmineqlem23  42796  lcmineqlem  42797  3lexlogpow5ineq2  42800  3lexlogpow5ineq4  42801  3lexlogpow2ineq2  42804  3lexlogpow5ineq5  42805  aks4d1p1p3  42814  aks4d1p1p2  42815  aks4d1p1p4  42816  aks4d1p1p5  42820  aks4d1p1  42821  aks4d1p3  42823  aks4d1p4  42824  aks4d1p5  42825  aks4d1p6  42826  aks4d1p7  42828  aks4d1p8d2  42830  aks4d1p8  42832  aks4d1p9  42833  posbezout  42845  primrootlekpowne0  42850  primrootspoweq0  42851  aks6d1c1  42861  hashscontpow1  42866  aks6d1c3  42868  aks6d1c4  42869  aks6d1c2lem4  42872  aks6d1c2  42875  aks6d1c5lem1  42881  2ap1caineq  42890  sticksstones1  42891  sticksstones2  42892  sticksstones3  42893  sticksstones6  42896  sticksstones7  42897  sticksstones10  42900  sticksstones12a  42902  sticksstones12  42903  aks6d1c6lem4  42918  bcled  42923  bcle2d  42924  aks6d1c7lem1  42925  aks6d1c7lem2  42926  unitscyglem1  42940  unitscyglem2  42941  unitscyglem4  42943  unitscyglem5  42944  aks5lem8  42946  oexpreposd  43061  fimgmcyclem  43281  fimgmcyc  43282  flt4lem5e  43368  flt4lem6  43370  flt4lem7  43371  fltltc  43373  fltnltalem  43374  fltnlta  43375  3cubeslem3r  43398  irrapxlem3  43531  irrapxlem4  43532  irrapxlem5  43533  pellexlem2  43537  pellexlem6  43541  pell14qrgt0  43566  pell14qrgapw  43583  pellfundgt1  43590  rmspecsqrtnq  43613  ltrmxnn0  43656  jm3.1lem1  43724  jm3.1lem3  43726  dgraa0p  43856  hashnzfz2  45011  rfcnnnub  45736  nnxrd  45973  fzisoeu  45999  fsumnncl  46268  sumnnodd  46326  limsup10exlem  46466  stoweidlem1  46695  stoweidlem3  46697  stoweidlem11  46705  stoweidlem17  46711  stoweidlem20  46714  stoweidlem25  46719  stoweidlem26  46720  stoweidlem34  46728  stoweidlem38  46732  stoweidlem42  46736  stoweidlem44  46738  stoweidlem51  46745  stoweidlem59  46753  stoweidlem60  46754  wallispi  46764  wallispi2  46767  stirlinglem3  46770  stirlinglem4  46771  stirlinglem8  46775  stirlinglem10  46777  stirlinglem12  46779  stirlinglem15  46782  dirkertrigeqlem2  46793  dirkertrigeqlem3  46794  dirkercncflem2  46798  fourierdlem11  46812  fourierdlem14  46815  fourierdlem15  46816  fourierdlem20  46821  fourierdlem31  46832  fourierdlem64  46864  fourierdlem93  46893  fourierdlem95  46895  fourierdlem103  46903  fourierdlem104  46904  fourierdlem112  46912  sqwvfourb  46923  etransclem3  46931  etransclem19  46947  etransclem23  46951  etransclem24  46952  etransclem25  46953  etransclem32  46960  etransclem35  46963  etransclem41  46969  etransclem48  46976  qndenserrnbllem  46988  hoiqssbllem1  47316  hoiqssbllem2  47317  ovolval5lem1  47346  ovolval5lem2  47347  iccpartlt  48150  iccpartgt  48153  odz2prm2pw  48292  fmtnoprmfac1lem  48293  2pwp1prm  48318  sfprmdvdsmersenne  48332  lighneallem2  48335  proththdlem  48342  perfectALTVlem2  48464  gbowge7  48505  ztprmneprm  49104  pgrple2abl  49122  logbpw2m1  49324  nnpw2pmod  49340  nnolog2flm1  49347  blennngt2o2  49349  itcovalt2lem2lem1  49430