Theorem nnred 12224

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11106  ℕcn 12209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-i2m1 11175  ax-1ne0 11176  ax-rrecex 11179  ax-cnre 11180

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-nn 12210

This theorem is referenced by:  nnne0  12243  uzwo3  12924  modmulnn  13851  bernneq3  14191  expmulnbnd  14195  expnngt1b  14202  facwordi  14246  faclbnd  14247  faclbnd2  14248  faclbnd3  14249  faclbnd5  14255  faclbnd6  14256  facubnd  14257  facavg  14258  bcp1nk  14274  hashf1  14415  swrds2  14888  isercolllem1  15608  isercoll  15611  o1fsum  15756  climcndslem1  15792  climcndslem2  15793  climcnds  15794  eftabs  16016  efcllem  16018  ege2le3  16030  efcj  16032  eftlub  16049  eflegeo  16061  eirrlem  16144  fzm1ndvds  16262  nno  16322  nnoddm1d2  16326  bitsfzolem  16372  bitsfzo  16373  bitsinv1lem  16379  sadcaddlem  16395  smueqlem  16428  bezoutlem3  16480  bezoutlem4  16481  sqgcd  16499  lcmgcdlem  16540  lcmf  16567  prmind2  16619  coprm  16645  prmfac1  16655  prmndvdsfaclt  16659  divdenle  16682  qnumgt0  16683  zsqrtelqelz  16691  hashdvds  16705  eulerthlem2  16712  odzdvds  16725  vfermltl  16731  modprm0  16735  pythagtriplem11  16755  pythagtriplem13  16757  pythagtriplem19  16763  pclem  16768  pcpre1  16772  pcidlem  16802  dvdsprmpweqle  16816  pcadd  16819  pcmpt  16822  pcmpt2  16823  pcfaclem  16828  pcfac  16829  qexpz  16831  pockthlem  16835  pockthg  16836  prmreclem1  16846  prmreclem3  16848  prmreclem4  16849  prmreclem5  16850  1arithlem4  16856  1arith  16857  4sqlem5  16872  4sqlem6  16873  4sqlem10  16877  mul4sqlem  16883  4sqlem11  16885  4sqlem12  16886  4sqlem13  16887  4sqlem14  16888  4sqlem15  16889  4sqlem16  16890  4sqlem17  16891  vdwlem1  16911  vdwlem3  16913  vdwlem6  16916  vdwlem9  16919  vdwlem10  16920  vdwlem12  16922  vdwnnlem3  16927  ramub1lem1  16956  prmolefac  16976  prmgaplem4  16984  prmgaplem5  16985  prmgaplem6  16986  prmgaplem8  16988  2expltfac  17023  cshwshashnsame  17034  setsstruct2  17104  psgnunilem4  19360  mndodconglem  19404  oddvds  19410  sylow1lem1  19461  sylow1lem5  19465  fislw  19488  efgredlem  19610  gexexlem  19715  zringlpirlem3  21026  prmirredlem  21034  fvmptnn04if  22343  fvmptnn04ifb  22345  fvmptnn04ifc  22346  fvmptnn04ifd  22347  chfacfisf  22348  chfacfisfcpmat  22349  chfacfscmulgsum  22354  chfacfpmmulgsum  22358  lebnumii  24474  lmnn  24772  ovolunlem1a  25005  ovoliunlem1  25011  ovolicc2lem3  25028  ovolicc2lem4  25029  iundisj  25057  voliunlem1  25059  uniioombllem3  25094  dyadf  25100  dyadovol  25102  dyaddisjlem  25104  dyadmaxlem  25106  opnmbllem  25110  vitalilem4  25120  mbfi1fseqlem1  25225  mbfi1fseqlem3  25227  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1fseqlem6  25230  itg2gt0  25270  itg2cnlem2  25272  dgreq0  25771  dgrco  25781  elqaalem2  25825  aaliou3lem2  25848  aaliou3lem8  25850  aaliou3lem9  25855  leibpi  26437  log2tlbnd  26440  birthdaylem3  26448  amgm  26485  emcllem2  26491  harmonicbnd4  26505  lgamgulmlem1  26523  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem4  26526  lgamgulmlem5  26527  lgamgulmlem6  26528  lgamucov  26532  lgamcvg2  26549  wilthlem1  26562  ftalem5  26571  basellem1  26575  basellem2  26576  basellem3  26577  basellem4  26578  basellem5  26579  basellem6  26580  basellem8  26582  chtge0  26606  chtwordi  26650  vma1  26660  dvdsflf1o  26681  dvdsflsumcom  26682  fsumfldivdiaglem  26683  sgmmul  26694  chtublem  26704  fsumvma2  26707  logfac2  26710  chpchtsum  26712  chpub  26713  logfaclbnd  26715  logexprlim  26718  mersenne  26720  perfectlem2  26723  dchrelbas4  26736  bposlem1  26777  bposlem2  26778  bposlem3  26779  bposlem4  26780  bposlem5  26781  bposlem6  26782  bposlem7  26783  bposlem9  26785  lgslem1  26790  lgsval2lem  26800  lgsdirprm  26824  lgsdir  26825  lgsne0  26828  lgsqrlem2  26840  gausslemma2dlem0h  26856  gausslemma2dlem0i  26857  gausslemma2dlem1a  26858  gausslemma2dlem2  26860  gausslemma2dlem7  26866  gausslemma2d  26867  lgseisenlem1  26868  lgseisenlem2  26869  lgseisenlem3  26870  lgseisenlem4  26871  lgseisen  26872  lgsquadlem1  26873  lgsquadlem2  26874  lgsquadlem3  26875  2sqlem3  26913  2sqlem8  26919  2sqblem  26924  2sqmod  26929  chebbnd1lem1  26962  chebbnd1lem3  26964  chtppilimlem1  26966  rplogsumlem1  26977  rplogsumlem2  26978  dchrisum0lem1a  26979  rpvmasumlem  26980  dchrisumlema  26981  dchrisumlem1  26982  dchrisumlem2  26983  dchrisumlem3  26984  dchrvmasumiflem1  26994  dchrisum0flblem2  27002  dchrisum0re  27006  dchrisum0lem1b  27008  dchrisum0lem1  27009  dirith2  27021  selbergb  27042  selberg2lem  27043  logdivbnd  27049  selberg3lem2  27051  selberg4lem1  27053  pntrsumo1  27058  pntrsumbnd2  27060  pntrlog2bndlem1  27070  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntpbnd1a  27078  pntpbnd1  27079  pntibndlem2a  27083  pntibndlem2  27084  pntlemg  27091  pntlemh  27092  pntlemj  27096  pntlemf  27098  ostth2lem1  27111  padicabvf  27124  padicabvcxp  27125  ostth2lem2  27127  ostth2lem3  27128  ostth2lem4  27129  ostth2  27130  ostth3  27131  numclwwlk5  29631  numclwwlk7  29634  ubthlem2  30112  minvecolem4  30121  iundisjf  31808  ssnnssfz  31986  iundisjfi  31995  pfxlsw2ccat  32104  pmtrto1cl  32246  psgnfzto1stlem  32247  fzto1st1  32249  fzto1st  32250  psgnfzto1st  32252  cycpmco2lem6  32278  cycpmco2lem7  32279  smatrcl  32765  smattr  32768  smatbl  32769  smatbr  32770  1smat1  32773  submateqlem1  32776  submateqlem2  32777  submateq  32778  esumcst  33050  fiunelros  33161  oddpwdc  33342  eulerpartlems  33348  eulerpartlemgc  33350  fiblem  33386  dstfrvunirn  33462  dstfrvclim1  33465  ballotlemimin  33493  fsum2dsub  33608  reprinfz1  33623  hgt750lemd  33649  hgt750lemb  33657  hgt750leme  33659  tgoldbachgtde  33661  tgoldbachgt  33664  subfaclim  34168  subfacval3  34169  erdszelem7  34177  erdszelem8  34178  erdsze2lem2  34184  cvmliftlem2  34266  cvmliftlem6  34270  cvmliftlem7  34271  cvmliftlem8  34272  cvmliftlem9  34273  cvmliftlem10  34274  cvmliftlem13  34276  bcprod  34697  bccolsum  34698  faclimlem2  34703  faclim2  34707  nn0prpwlem  35196  knoppndvlem15  35391  knoppndvlem17  35393  knoppndvlem18  35394  knoppndvlem19  35395  knoppndvlem20  35396  knoppndvlem21  35397  poimirlem3  36480  poimirlem6  36483  poimirlem7  36484  poimirlem8  36485  poimirlem9  36486  poimirlem10  36487  poimirlem11  36488  poimirlem12  36489  poimirlem13  36490  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem21  36498  poimirlem22  36499  poimirlem23  36500  poimirlem26  36503  poimirlem28  36505  opnmbllem0  36513  mblfinlem2  36515  incsequz  36605  nninfnub  36608  lcmineqlem4  40886  lcmineqlem10  40892  lcmineqlem11  40893  lcmineqlem15  40897  lcmineqlem18  40900  lcmineqlem19  40901  lcmineqlem20  40902  lcmineqlem21  40903  lcmineqlem22  40904  lcmineqlem23  40905  lcmineqlem  40906  3lexlogpow5ineq2  40909  3lexlogpow5ineq4  40910  3lexlogpow2ineq2  40913  3lexlogpow5ineq5  40914  aks4d1p1p3  40923  aks4d1p1p2  40924  aks4d1p1p4  40925  aks4d1p1p5  40929  aks4d1p1  40930  aks4d1p3  40932  aks4d1p4  40933  aks4d1p5  40934  aks4d1p6  40935  aks4d1p7  40937  aks4d1p8d2  40939  aks4d1p8  40941  aks4d1p9  40942  2ap1caineq  40950  sticksstones1  40951  sticksstones2  40952  sticksstones3  40953  sticksstones6  40956  sticksstones7  40957  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  metakunt1  40974  metakunt2  40975  metakunt6  40979  metakunt7  40980  metakunt9  40982  metakunt10  40983  metakunt11  40984  metakunt12  40985  metakunt16  40989  metakunt18  40991  metakunt20  40993  metakunt22  40995  metakunt24  40997  metakunt27  41000  metakunt28  41001  metakunt29  41002  metakunt30  41003  nnadddir  41182  oexpreposd  41208  nn0expgcd  41222  rtprmirr  41234  flt4lem5e  41395  flt4lem6  41397  flt4lem7  41398  fltltc  41400  fltnltalem  41401  fltnlta  41402  3cubeslem3r  41411  irrapxlem3  41548  irrapxlem4  41549  irrapxlem5  41550  pellexlem2  41554  pellexlem6  41558  pell14qrgt0  41583  pell14qrgapw  41600  pellfundgt1  41607  rmspecsqrtnq  41630  ltrmxnn0  41674  jm3.1lem1  41742  jm3.1lem3  41744  dgraa0p  41877  hashnzfz2  43066  rfcnnnub  43706  nnxrd  43970  fzisoeu  43997  fsumnncl  44275  sumnnodd  44333  limsup10exlem  44475  stoweidlem1  44704  stoweidlem3  44706  stoweidlem11  44714  stoweidlem17  44720  stoweidlem20  44723  stoweidlem25  44728  stoweidlem26  44729  stoweidlem34  44737  stoweidlem38  44741  stoweidlem42  44745  stoweidlem44  44747  stoweidlem51  44754  stoweidlem59  44762  stoweidlem60  44763  wallispi  44773  wallispi2  44776  stirlinglem3  44779  stirlinglem4  44780  stirlinglem8  44784  stirlinglem10  44786  stirlinglem12  44788  stirlinglem15  44791  dirkertrigeqlem2  44802  dirkertrigeqlem3  44803  dirkercncflem2  44807  fourierdlem11  44821  fourierdlem14  44824  fourierdlem15  44825  fourierdlem20  44830  fourierdlem31  44841  fourierdlem64  44873  fourierdlem93  44902  fourierdlem95  44904  fourierdlem103  44912  fourierdlem104  44913  fourierdlem112  44921  sqwvfourb  44932  etransclem3  44940  etransclem19  44956  etransclem23  44960  etransclem24  44961  etransclem25  44962  etransclem32  44969  etransclem35  44972  etransclem41  44978  etransclem48  44985  qndenserrnbllem  44997  hoiqssbllem1  45325  hoiqssbllem2  45326  ovolval5lem1  45355  ovolval5lem2  45356  iccpartlt  46079  iccpartgt  46082  odz2prm2pw  46218  fmtnoprmfac1lem  46219  2pwp1prm  46244  sfprmdvdsmersenne  46258  lighneallem2  46261  proththdlem  46268  perfectALTVlem2  46377  gbowge7  46418  ztprmneprm  46977  pgrple2abl  46995  logbpw2m1  47207  nnpw2pmod  47223  nnolog2flm1  47230  blennngt2o2  47232  itcovalt2lem2lem1  47313