Theorem nnred 12331

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11180  ℕcn 12316

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-i2m1 11249  ax-1ne0 11250  ax-rrecex 11253  ax-cnre 11254

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-nn 12317

This theorem is used by:  nnne0  12353  nnadddir  12375  uzwo3  13051  modmulnn  14009  bernneq3  14355  expmulnbnd  14359  expnngt1b  14366  facwordi  14413  faclbnd  14414  faclbnd2  14415  faclbnd3  14416  faclbnd5  14422  faclbnd6  14423  facubnd  14424  facavg  14425  bcp1nk  14441  hashf1  14582  swrds2  15071  isercolllem1  15812  isercoll  15815  o1fsum  15960  climcndslem1  15998  climcndslem2  15999  climcnds  16000  eftabs  16221  efcllem  16223  ege2le3  16236  efcj  16238  eftlub  16257  eflegeo  16269  eirrlem  16352  fzm1ndvds  16472  nno  16532  nnoddm1d2  16536  bitsfzolem  16584  bitsfzo  16585  bitsinv1lem  16591  sadcaddlem  16607  smueqlem  16640  bezoutlem3  16694  bezoutlem4  16695  sqgcd  16716  nn0expgcd  16718  lcmgcdlem  16761  lcmf  16788  prmind2  16840  coprm  16867  prmfac1  16876  prmndvdsfaclt  16881  divdenle  16905  qnumgt0  16906  zsqrtelqelz  16914  hashdvds  16932  eulerthlem2  16939  odzdvds  16953  vfermltl  16959  modprm0  16963  pythagtriplem11  16983  pythagtriplem13  16985  pythagtriplem19  16991  pclem  16996  pcpre1  17000  pcidlem  17030  dvdsprmpweqle  17044  pcadd  17047  pcmpt  17050  pcmpt2  17051  pcfaclem  17056  pcfac  17057  qexpz  17059  pockthlem  17063  pockthg  17064  prmreclem1  17074  prmreclem3  17076  prmreclem4  17077  prmreclem5  17078  1arithlem4  17084  1arith  17085  4sqlem5  17100  4sqlem6  17101  4sqlem10  17105  mul4sqlem  17111  4sqlem11  17113  4sqlem12  17114  4sqlem13  17115  4sqlem14  17116  4sqlem15  17117  4sqlem16  17118  4sqlem17  17119  vdwlem1  17139  vdwlem3  17141  vdwlem6  17144  vdwlem9  17147  vdwlem10  17148  vdwlem12  17150  vdwnnlem3  17155  ramub1lem1  17184  prmolefac  17204  prmgaplem4  17212  prmgaplem5  17213  prmgaplem6  17214  prmgaplem8  17216  2expltfac  17250  cshwshashnsame  17261  setsstruct2  17332  chnub  18776  psgnunilem4  19691  mndodconglem  19735  oddvds  19741  sylow1lem1  19792  sylow1lem5  19796  fislw  19819  efgredlem  19941  gexexlem  20046  zringlpirlem3  21750  prmirredlem  21758  fvmptnn04if  23147  fvmptnn04ifb  23149  fvmptnn04ifc  23150  fvmptnn04ifd  23151  chfacfisf  23152  chfacfisfcpmat  23153  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  lebnumii  25267  lmnn  25564  ovolunlem1a  25797  ovoliunlem1  25803  ovolicc2lem3  25820  ovolicc2lem4  25821  iundisj  25849  voliunlem1  25851  uniioombllem3  25886  dyadf  25892  dyadovol  25894  dyaddisjlem  25896  dyadmaxlem  25898  opnmbllem  25902  vitalilem4  25912  mbfi1fseqlem1  26016  mbfi1fseqlem3  26018  mbfi1fseqlem4  26019  mbfi1fseqlem5  26020  mbfi1fseqlem6  26021  itg2gt0  26061  itg2cnlem2  26063  dgreq0  26564  dgrco  26574  elqaalem2  26625  aaliou3lem2  26652  aaliou3lem8  26654  aaliou3lem9  26659  rtprmirr  27070  leibpi  27252  log2tlbnd  27255  birthdaylem3  27263  amgm  27300  emcllem2  27306  harmonicbnd4  27320  lgamgulmlem1  27338  lgamgulmlem2  27339  lgamgulmlem3  27340  lgamgulmlem4  27341  lgamgulmlem5  27342  lgamgulmlem6  27343  lgamucov  27347  lgamcvg2  27364  wilthlem1  27377  ftalem5  27386  basellem1  27390  basellem2  27391  basellem3  27392  basellem4  27393  basellem5  27394  basellem6  27395  basellem8  27397  chtge0  27421  chtwordi  27465  vma1  27475  dvdsflf1o  27496  dvdsflsumcom  27497  fsumfldivdiaglem  27498  sgmmul  27510  chtublem  27520  fsumvma2  27523  logfac2  27526  chpchtsum  27528  chpub  27529  logfaclbnd  27531  logexprlim  27534  mersenne  27536  perfectlem2  27539  dchrelbas4  27552  bposlem1  27593  bposlem2  27594  bposlem3  27595  bposlem4  27596  bposlem5  27597  bposlem6  27598  bposlem7  27599  bposlem9  27601  lgslem1  27606  lgsval2lem  27616  lgsdirprm  27640  lgsdir  27641  lgsne0  27644  lgsqrlem2  27656  gausslemma2dlem0h  27672  gausslemma2dlem0i  27673  gausslemma2dlem1a  27674  gausslemma2dlem2  27676  gausslemma2dlem7  27682  gausslemma2d  27683  lgseisenlem1  27684  lgseisenlem2  27685  lgseisenlem3  27686  lgseisenlem4  27687  lgseisen  27688  lgsquadlem1  27689  lgsquadlem2  27690  lgsquadlem3  27691  2sqlem3  27729  2sqlem8  27735  2sqblem  27740  2sqmod  27745  chebbnd1lem1  27778  chebbnd1lem3  27780  chtppilimlem1  27782  rplogsumlem1  27793  rplogsumlem2  27794  dchrisum0lem1a  27795  rpvmasumlem  27796  dchrisumlema  27797  dchrisumlem1  27798  dchrisumlem2  27799  dchrisumlem3  27800  dchrvmasumiflem1  27810  dchrisum0flblem2  27818  dchrisum0re  27822  dchrisum0lem1b  27824  dchrisum0lem1  27825  dirith2  27837  selbergb  27858  selberg2lem  27859  logdivbnd  27865  selberg3lem2  27867  selberg4lem1  27869  pntrsumo1  27874  pntrsumbnd2  27876  pntrlog2bndlem1  27886  pntrlog2bndlem2  27887  pntrlog2bndlem3  27888  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  pntpbnd1a  27894  pntpbnd1  27895  pntibndlem2a  27899  pntibndlem2  27900  pntlemg  27907  pntlemh  27908  pntlemj  27912  pntlemf  27914  ostth2lem1  27927  padicabvf  27940  padicabvcxp  27941  ostth2lem2  27943  ostth2lem3  27944  ostth2lem4  27945  ostth2  27946  ostth3  27947  flt4lem5e  27968  flt4lem6  27970  flt4lem7  27971  numclwwlk5  30971  numclwwlk7  30974  nrt2irr  31056  ubthlem2  31455  minvecolem4  31464  iundisjf  33165  ssnnssfz  33361  iundisjfi  33370  nexple  33406  2exple2exp  33407  pfxlsw2ccat  33495  pmtrto1cl  33642  psgnfzto1stlem  33643  fzto1st1  33645  fzto1st  33646  psgnfzto1st  33648  cycpmco2lem6  33674  cycpmco2lem7  33675  fldextrspundgdvdslem  34294  fldextrspundgdvds  34295  fldext2rspun  34296  smatrcl  34410  smattr  34413  smatbl  34414  smatbr  34415  1smat1  34418  submateqlem1  34421  submateqlem2  34422  submateq  34423  esumcst  34677  fiunelros  34789  oddpwdc  34969  eulerpartlems  34975  eulerpartlemgc  34977  fiblem  35013  dstfrvunirn  35090  dstfrvclim1  35093  ballotlemimin  35121  fsum2dsub  35219  reprinfz1  35234  hgt750lemd  35260  hgt750lemb  35268  hgt750leme  35270  tgoldbachgtde  35272  tgoldbachgt  35275  subfaclim  35922  subfacval3  35923  erdszelem7  35931  erdszelem8  35932  erdsze2lem2  35938  cvmliftlem2  36020  cvmliftlem6  36024  cvmliftlem7  36025  cvmliftlem8  36026  cvmliftlem9  36027  cvmliftlem10  36028  cvmliftlem13  36030  bcprod  36472  bccolsum  36473  faclimlem2  36478  faclim2  36482  nn0prpwlem  37080  knoppcnlem10  37338  knoppndvlem15  37362  knoppndvlem17  37364  knoppndvlem18  37365  knoppndvlem19  37366  knoppndvlem20  37367  knoppndvlem21  37368  poimirlem3  38509  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem9  38515  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem13  38519  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem21  38527  poimirlem22  38528  poimirlem23  38529  poimirlem26  38532  poimirlem28  38534  opnmbllem0  38542  mblfinlem2  38544  incsequz  38650  nninfnub  38653  lcmineqlem4  43050  lcmineqlem10  43056  lcmineqlem11  43057  lcmineqlem15  43061  lcmineqlem18  43064  lcmineqlem19  43065  lcmineqlem20  43066  lcmineqlem21  43067  lcmineqlem22  43068  lcmineqlem23  43069  lcmineqlem  43070  3lexlogpow5ineq2  43073  3lexlogpow5ineq4  43074  3lexlogpow2ineq2  43077  3lexlogpow5ineq5  43078  aks4d1p1p3  43087  aks4d1p1p2  43088  aks4d1p1p4  43089  aks4d1p1p5  43093  aks4d1p1  43094  aks4d1p3  43096  aks4d1p4  43097  aks4d1p5  43098  aks4d1p6  43099  aks4d1p7  43101  aks4d1p8d2  43103  aks4d1p8  43105  aks4d1p9  43106  posbezout  43118  primrootlekpowne0  43123  primrootspoweq0  43124  aks6d1c1  43134  hashscontpow1  43139  aks6d1c3  43141  aks6d1c4  43142  aks6d1c2lem4  43145  aks6d1c2  43148  aks6d1c5lem1  43154  2ap1caineq  43163  sticksstones1  43164  sticksstones2  43165  sticksstones3  43166  sticksstones6  43169  sticksstones7  43170  sticksstones10  43173  sticksstones12a  43175  sticksstones12  43176  aks6d1c6lem4  43191  bcled  43196  bcle2d  43197  aks6d1c7lem1  43198  aks6d1c7lem2  43199  unitscyglem1  43213  unitscyglem2  43214  unitscyglem4  43216  unitscyglem5  43217  aks5lem8  43219  oexpreposd  43347  fimgmcyclem  43559  fimgmcyc  43560  fltltc  43626  fltnltalem  43627  fltnlta  43628  3cubeslem3r  43651  irrapxlem3  43784  irrapxlem4  43785  irrapxlem5  43786  pellexlem2  43790  pellexlem6  43794  pell14qrgt0  43819  pell14qrgapw  43836  pellfundgt1  43843  rmspecsqrtnq  43866  ltrmxnn0  43909  jm3.1lem1  43977  jm3.1lem3  43979  dgraa0p  44109  hashnzfz2  45264  rfcnnnub  45996  nnxrd  46233  fzisoeu  46259  fsumnncl  46528  sumnnodd  46586  limsup10exlem  46726  stoweidlem1  46955  stoweidlem3  46957  stoweidlem11  46965  stoweidlem17  46971  stoweidlem20  46974  stoweidlem25  46979  stoweidlem26  46980  stoweidlem34  46988  stoweidlem38  46992  stoweidlem42  46996  stoweidlem44  46998  stoweidlem51  47005  stoweidlem59  47013  stoweidlem60  47014  wallispi  47024  wallispi2  47027  stirlinglem3  47030  stirlinglem4  47031  stirlinglem8  47035  stirlinglem10  47037  stirlinglem12  47039  stirlinglem15  47042  dirkertrigeqlem2  47053  dirkertrigeqlem3  47054  dirkercncflem2  47058  fourierdlem11  47072  fourierdlem14  47075  fourierdlem15  47076  fourierdlem20  47081  fourierdlem31  47092  fourierdlem64  47124  fourierdlem93  47153  fourierdlem95  47155  fourierdlem103  47163  fourierdlem104  47164  fourierdlem112  47172  sqwvfourb  47183  etransclem3  47191  etransclem19  47207  etransclem23  47211  etransclem24  47212  etransclem25  47213  etransclem32  47220  etransclem35  47223  etransclem41  47229  etransclem48  47236  qndenserrnbllem  47248  hoiqssbllem1  47576  hoiqssbllem2  47577  ovolval5lem1  47606  ovolval5lem2  47607  iccpartlt  48450  iccpartgt  48453  odz2prm2pw  48592  fmtnoprmfac1lem  48593  2pwp1prm  48618  sfprmdvdsmersenne  48632  lighneallem2  48635  proththdlem  48642  perfectALTVlem2  48764  gbowge7  48805  ztprmneprm  49403  pgrple2abl  49421  logbpw2m1  49623  nnpw2pmod  49639  nnolog2flm1  49646  blennngt2o2  49648  itcovalt2lem2lem1  49729