Theorem nnred 12239

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  ℕcn 12224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-i2m1 11156  ax-1ne0 11157  ax-rrecex 11160  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-nn 12225

This theorem is referenced by:  nnne0  12261  nnadddir  12283  uzwo3  12958  modmulnn  13913  bernneq3  14258  expmulnbnd  14262  expnngt1b  14269  facwordi  14316  faclbnd  14317  faclbnd2  14318  faclbnd3  14319  faclbnd5  14325  faclbnd6  14326  facubnd  14327  facavg  14328  bcp1nk  14344  hashf1  14484  swrds2  14967  isercolllem1  15706  isercoll  15709  o1fsum  15855  climcndslem1  15893  climcndslem2  15894  climcnds  15895  eftabs  16119  efcllem  16121  ege2le3  16134  efcj  16136  eftlub  16155  eflegeo  16167  eirrlem  16250  fzm1ndvds  16370  nno  16430  nnoddm1d2  16434  bitsfzolem  16482  bitsfzo  16483  bitsinv1lem  16489  sadcaddlem  16505  smueqlem  16538  bezoutlem3  16589  bezoutlem4  16590  sqgcd  16610  nn0expgcd  16612  lcmgcdlem  16654  lcmf  16681  prmind2  16733  coprm  16760  prmfac1  16769  prmndvdsfaclt  16774  divdenle  16798  qnumgt0  16799  zsqrtelqelz  16807  hashdvds  16824  eulerthlem2  16831  odzdvds  16845  vfermltl  16851  modprm0  16855  pythagtriplem11  16875  pythagtriplem13  16877  pythagtriplem19  16883  pclem  16888  pcpre1  16892  pcidlem  16922  dvdsprmpweqle  16936  pcadd  16939  pcmpt  16942  pcmpt2  16943  pcfaclem  16948  pcfac  16949  qexpz  16951  pockthlem  16955  pockthg  16956  prmreclem1  16966  prmreclem3  16968  prmreclem4  16969  prmreclem5  16970  1arithlem4  16976  1arith  16977  4sqlem5  16992  4sqlem6  16993  4sqlem10  16997  mul4sqlem  17003  4sqlem11  17005  4sqlem12  17006  4sqlem13  17007  4sqlem14  17008  4sqlem15  17009  4sqlem16  17010  4sqlem17  17011  vdwlem1  17031  vdwlem3  17033  vdwlem6  17036  vdwlem9  17039  vdwlem10  17040  vdwlem12  17042  vdwnnlem3  17047  ramub1lem1  17076  prmolefac  17096  prmgaplem4  17104  prmgaplem5  17105  prmgaplem6  17106  prmgaplem8  17108  2expltfac  17142  cshwshashnsame  17153  setsstruct2  17224  chnub  18668  psgnunilem4  19558  mndodconglem  19602  oddvds  19608  sylow1lem1  19659  sylow1lem5  19663  fislw  19686  efgredlem  19808  gexexlem  19913  zringlpirlem3  21574  prmirredlem  21582  fvmptnn04if  22967  fvmptnn04ifb  22969  fvmptnn04ifc  22970  fvmptnn04ifd  22971  chfacfisf  22972  chfacfisfcpmat  22973  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  lebnumii  25086  lmnn  25383  ovolunlem1a  25616  ovoliunlem1  25622  ovolicc2lem3  25639  ovolicc2lem4  25640  iundisj  25668  voliunlem1  25670  uniioombllem3  25705  dyadf  25711  dyadovol  25713  dyaddisjlem  25715  dyadmaxlem  25717  opnmbllem  25721  vitalilem4  25731  mbfi1fseqlem1  25835  mbfi1fseqlem3  25837  mbfi1fseqlem4  25838  mbfi1fseqlem5  25839  mbfi1fseqlem6  25840  itg2gt0  25880  itg2cnlem2  25882  dgreq0  26383  dgrco  26393  elqaalem2  26442  aaliou3lem2  26465  aaliou3lem8  26467  aaliou3lem9  26472  rtprmirr  26883  leibpi  27065  log2tlbnd  27068  birthdaylem3  27076  amgm  27113  emcllem2  27119  harmonicbnd4  27133  lgamgulmlem1  27151  lgamgulmlem2  27152  lgamgulmlem3  27153  lgamgulmlem4  27154  lgamgulmlem5  27155  lgamgulmlem6  27156  lgamucov  27160  lgamcvg2  27177  wilthlem1  27190  ftalem5  27199  basellem1  27203  basellem2  27204  basellem3  27205  basellem4  27206  basellem5  27207  basellem6  27208  basellem8  27210  chtge0  27234  chtwordi  27278  vma1  27288  dvdsflf1o  27309  dvdsflsumcom  27310  fsumfldivdiaglem  27311  sgmmul  27323  chtublem  27333  fsumvma2  27336  logfac2  27339  chpchtsum  27341  chpub  27342  logfaclbnd  27344  logexprlim  27347  mersenne  27349  perfectlem2  27352  dchrelbas4  27365  bposlem1  27406  bposlem2  27407  bposlem3  27408  bposlem4  27409  bposlem5  27410  bposlem6  27411  bposlem7  27412  bposlem9  27414  lgslem1  27419  lgsval2lem  27429  lgsdirprm  27453  lgsdir  27454  lgsne0  27457  lgsqrlem2  27469  gausslemma2dlem0h  27485  gausslemma2dlem0i  27486  gausslemma2dlem1a  27487  gausslemma2dlem2  27489  gausslemma2dlem7  27495  gausslemma2d  27496  lgseisenlem1  27497  lgseisenlem2  27498  lgseisenlem3  27499  lgseisenlem4  27500  lgseisen  27501  lgsquadlem1  27502  lgsquadlem2  27503  lgsquadlem3  27504  2sqlem3  27542  2sqlem8  27548  2sqblem  27553  2sqmod  27558  chebbnd1lem1  27591  chebbnd1lem3  27593  chtppilimlem1  27595  rplogsumlem1  27606  rplogsumlem2  27607  dchrisum0lem1a  27608  rpvmasumlem  27609  dchrisumlema  27610  dchrisumlem1  27611  dchrisumlem2  27612  dchrisumlem3  27613  dchrvmasumiflem1  27623  dchrisum0flblem2  27631  dchrisum0re  27635  dchrisum0lem1b  27637  dchrisum0lem1  27638  dirith2  27650  selbergb  27671  selberg2lem  27672  logdivbnd  27678  selberg3lem2  27680  selberg4lem1  27682  pntrsumo1  27687  pntrsumbnd2  27689  pntrlog2bndlem1  27699  pntrlog2bndlem2  27700  pntrlog2bndlem3  27701  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  pntpbnd1a  27707  pntpbnd1  27708  pntibndlem2a  27712  pntibndlem2  27713  pntlemg  27720  pntlemh  27721  pntlemj  27725  pntlemf  27727  ostth2lem1  27740  padicabvf  27753  padicabvcxp  27754  ostth2lem2  27756  ostth2lem3  27757  ostth2lem4  27758  ostth2  27759  ostth3  27760  numclwwlk5  30648  numclwwlk7  30651  nrt2irr  30733  ubthlem2  31132  minvecolem4  31141  iundisjf  32844  ssnnssfz  33044  iundisjfi  33053  nexple  33090  2exple2exp  33091  pfxlsw2ccat  33183  pmtrto1cl  33332  psgnfzto1stlem  33333  fzto1st1  33335  fzto1st  33336  psgnfzto1st  33338  cycpmco2lem6  33364  cycpmco2lem7  33365  fldextrspundgdvdslem  33987  fldextrspundgdvds  33988  fldext2rspun  33989  smatrcl  34103  smattr  34106  smatbl  34107  smatbr  34108  1smat1  34111  submateqlem1  34114  submateqlem2  34115  submateq  34116  esumcst  34370  fiunelros  34481  oddpwdc  34661  eulerpartlems  34667  eulerpartlemgc  34669  fiblem  34705  dstfrvunirn  34782  dstfrvclim1  34785  ballotlemimin  34813  fsum2dsub  34911  reprinfz1  34926  hgt750lemd  34952  hgt750lemb  34960  hgt750leme  34962  tgoldbachgtde  34964  tgoldbachgt  34967  subfaclim  35551  subfacval3  35552  erdszelem7  35560  erdszelem8  35561  erdsze2lem2  35567  cvmliftlem2  35649  cvmliftlem6  35653  cvmliftlem7  35654  cvmliftlem8  35655  cvmliftlem9  35656  cvmliftlem10  35657  cvmliftlem13  35659  bcprod  36101  bccolsum  36102  faclimlem2  36107  faclim2  36111  nn0prpwlem  36695  knoppcnlem10  36953  knoppndvlem15  36977  knoppndvlem17  36979  knoppndvlem18  36980  knoppndvlem19  36981  knoppndvlem20  36982  knoppndvlem21  36983  poimirlem3  38134  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem9  38140  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem13  38144  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem23  38154  poimirlem26  38157  poimirlem28  38159  opnmbllem0  38167  mblfinlem2  38169  incsequz  38259  nninfnub  38262  lcmineqlem4  42661  lcmineqlem10  42667  lcmineqlem11  42668  lcmineqlem15  42672  lcmineqlem18  42675  lcmineqlem19  42676  lcmineqlem20  42677  lcmineqlem21  42678  lcmineqlem22  42679  lcmineqlem23  42680  lcmineqlem  42681  3lexlogpow5ineq2  42684  3lexlogpow5ineq4  42685  3lexlogpow2ineq2  42688  3lexlogpow5ineq5  42689  aks4d1p1p3  42698  aks4d1p1p2  42699  aks4d1p1p4  42700  aks4d1p1p5  42704  aks4d1p1  42705  aks4d1p3  42707  aks4d1p4  42708  aks4d1p5  42709  aks4d1p6  42710  aks4d1p7  42712  aks4d1p8d2  42714  aks4d1p8  42716  aks4d1p9  42717  posbezout  42729  primrootlekpowne0  42734  primrootspoweq0  42735  aks6d1c1  42745  hashscontpow1  42750  aks6d1c3  42752  aks6d1c4  42753  aks6d1c2lem4  42756  aks6d1c2  42759  aks6d1c5lem1  42765  2ap1caineq  42774  sticksstones1  42775  sticksstones2  42776  sticksstones3  42777  sticksstones6  42780  sticksstones7  42781  sticksstones10  42784  sticksstones12a  42786  sticksstones12  42787  aks6d1c6lem4  42802  bcled  42807  bcle2d  42808  aks6d1c7lem1  42809  aks6d1c7lem2  42810  unitscyglem1  42824  unitscyglem2  42825  unitscyglem4  42827  unitscyglem5  42828  aks5lem8  42830  oexpreposd  42943  fimgmcyclem  43163  fimgmcyc  43164  flt4lem5e  43250  flt4lem6  43252  flt4lem7  43253  fltltc  43255  fltnltalem  43256  fltnlta  43257  3cubeslem3r  43280  irrapxlem3  43413  irrapxlem4  43414  irrapxlem5  43415  pellexlem2  43419  pellexlem6  43423  pell14qrgt0  43448  pell14qrgapw  43465  pellfundgt1  43472  rmspecsqrtnq  43495  ltrmxnn0  43538  jm3.1lem1  43606  jm3.1lem3  43608  dgraa0p  43738  hashnzfz2  44895  rfcnnnub  45614  nnxrd  45851  fzisoeu  45877  fsumnncl  46146  sumnnodd  46204  limsup10exlem  46344  stoweidlem1  46573  stoweidlem3  46575  stoweidlem11  46583  stoweidlem17  46589  stoweidlem20  46592  stoweidlem25  46597  stoweidlem26  46598  stoweidlem34  46606  stoweidlem38  46610  stoweidlem42  46614  stoweidlem44  46616  stoweidlem51  46623  stoweidlem59  46631  stoweidlem60  46632  wallispi  46642  wallispi2  46645  stirlinglem3  46648  stirlinglem4  46649  stirlinglem8  46653  stirlinglem10  46655  stirlinglem12  46657  stirlinglem15  46660  dirkertrigeqlem2  46671  dirkertrigeqlem3  46672  dirkercncflem2  46676  fourierdlem11  46690  fourierdlem14  46693  fourierdlem15  46694  fourierdlem20  46699  fourierdlem31  46710  fourierdlem64  46742  fourierdlem93  46771  fourierdlem95  46773  fourierdlem103  46781  fourierdlem104  46782  fourierdlem112  46790  sqwvfourb  46801  etransclem3  46809  etransclem19  46825  etransclem23  46829  etransclem24  46830  etransclem25  46831  etransclem32  46838  etransclem35  46841  etransclem41  46847  etransclem48  46854  qndenserrnbllem  46866  hoiqssbllem1  47194  hoiqssbllem2  47195  ovolval5lem1  47224  ovolval5lem2  47225  iccpartlt  48028  iccpartgt  48031  odz2prm2pw  48170  fmtnoprmfac1lem  48171  2pwp1prm  48196  sfprmdvdsmersenne  48210  lighneallem2  48213  proththdlem  48220  perfectALTVlem2  48342  gbowge7  48383  ztprmneprm  48978  pgrple2abl  48996  logbpw2m1  49198  nnpw2pmod  49214  nnolog2flm1  49221  blennngt2o2  49223  itcovalt2lem2lem1  49304