Theorem nnred 12227

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11109  ℕcn 12212

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 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rrecex 11182  ax-cnre 11183

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 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-nn 12213

This theorem is referenced by:  nnne0  12246  uzwo3  12927  modmulnn  13854  bernneq3  14194  expmulnbnd  14198  expnngt1b  14205  facwordi  14249  faclbnd  14250  faclbnd2  14251  faclbnd3  14252  faclbnd5  14258  faclbnd6  14259  facubnd  14260  facavg  14261  bcp1nk  14277  hashf1  14418  swrds2  14891  isercolllem1  15611  isercoll  15614  o1fsum  15759  climcndslem1  15795  climcndslem2  15796  climcnds  15797  eftabs  16019  efcllem  16021  ege2le3  16033  efcj  16035  eftlub  16052  eflegeo  16064  eirrlem  16147  fzm1ndvds  16265  nno  16325  nnoddm1d2  16329  bitsfzolem  16375  bitsfzo  16376  bitsinv1lem  16382  sadcaddlem  16398  smueqlem  16431  bezoutlem3  16483  bezoutlem4  16484  sqgcd  16502  lcmgcdlem  16543  lcmf  16570  prmind2  16622  coprm  16648  prmfac1  16658  prmndvdsfaclt  16662  divdenle  16685  qnumgt0  16686  zsqrtelqelz  16694  hashdvds  16708  eulerthlem2  16715  odzdvds  16728  vfermltl  16734  modprm0  16738  pythagtriplem11  16758  pythagtriplem13  16760  pythagtriplem19  16766  pclem  16771  pcpre1  16775  pcidlem  16805  dvdsprmpweqle  16819  pcadd  16822  pcmpt  16825  pcmpt2  16826  pcfaclem  16831  pcfac  16832  qexpz  16834  pockthlem  16838  pockthg  16839  prmreclem1  16849  prmreclem3  16851  prmreclem4  16852  prmreclem5  16853  1arithlem4  16859  1arith  16860  4sqlem5  16875  4sqlem6  16876  4sqlem10  16880  mul4sqlem  16886  4sqlem11  16888  4sqlem12  16889  4sqlem13  16890  4sqlem14  16891  4sqlem15  16892  4sqlem16  16893  4sqlem17  16894  vdwlem1  16914  vdwlem3  16916  vdwlem6  16919  vdwlem9  16922  vdwlem10  16923  vdwlem12  16925  vdwnnlem3  16930  ramub1lem1  16959  prmolefac  16979  prmgaplem4  16987  prmgaplem5  16988  prmgaplem6  16989  prmgaplem8  16991  2expltfac  17026  cshwshashnsame  17037  setsstruct2  17107  psgnunilem4  19365  mndodconglem  19409  oddvds  19415  sylow1lem1  19466  sylow1lem5  19470  fislw  19493  efgredlem  19615  gexexlem  19720  zringlpirlem3  21034  prmirredlem  21042  fvmptnn04if  22351  fvmptnn04ifb  22353  fvmptnn04ifc  22354  fvmptnn04ifd  22355  chfacfisf  22356  chfacfisfcpmat  22357  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  lebnumii  24482  lmnn  24780  ovolunlem1a  25013  ovoliunlem1  25019  ovolicc2lem3  25036  ovolicc2lem4  25037  iundisj  25065  voliunlem1  25067  uniioombllem3  25102  dyadf  25108  dyadovol  25110  dyaddisjlem  25112  dyadmaxlem  25114  opnmbllem  25118  vitalilem4  25128  mbfi1fseqlem1  25233  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1fseqlem6  25238  itg2gt0  25278  itg2cnlem2  25280  dgreq0  25779  dgrco  25789  elqaalem2  25833  aaliou3lem2  25856  aaliou3lem8  25858  aaliou3lem9  25863  leibpi  26447  log2tlbnd  26450  birthdaylem3  26458  amgm  26495  emcllem2  26501  harmonicbnd4  26515  lgamgulmlem1  26533  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem4  26536  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamucov  26542  lgamcvg2  26559  wilthlem1  26572  ftalem5  26581  basellem1  26585  basellem2  26586  basellem3  26587  basellem4  26588  basellem5  26589  basellem6  26590  basellem8  26592  chtge0  26616  chtwordi  26660  vma1  26670  dvdsflf1o  26691  dvdsflsumcom  26692  fsumfldivdiaglem  26693  sgmmul  26704  chtublem  26714  fsumvma2  26717  logfac2  26720  chpchtsum  26722  chpub  26723  logfaclbnd  26725  logexprlim  26728  mersenne  26730  perfectlem2  26733  dchrelbas4  26746  bposlem1  26787  bposlem2  26788  bposlem3  26789  bposlem4  26790  bposlem5  26791  bposlem6  26792  bposlem7  26793  bposlem9  26795  lgslem1  26800  lgsval2lem  26810  lgsdirprm  26834  lgsdir  26835  lgsne0  26838  lgsqrlem2  26850  gausslemma2dlem0h  26866  gausslemma2dlem0i  26867  gausslemma2dlem1a  26868  gausslemma2dlem2  26870  gausslemma2dlem7  26876  gausslemma2d  26877  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgseisen  26882  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  2sqlem3  26923  2sqlem8  26929  2sqblem  26934  2sqmod  26939  chebbnd1lem1  26972  chebbnd1lem3  26974  chtppilimlem1  26976  rplogsumlem1  26987  rplogsumlem2  26988  dchrisum0lem1a  26989  rpvmasumlem  26990  dchrisumlema  26991  dchrisumlem1  26992  dchrisumlem2  26993  dchrisumlem3  26994  dchrvmasumiflem1  27004  dchrisum0flblem2  27012  dchrisum0re  27016  dchrisum0lem1b  27018  dchrisum0lem1  27019  dirith2  27031  selbergb  27052  selberg2lem  27053  logdivbnd  27059  selberg3lem2  27061  selberg4lem1  27063  pntrsumo1  27068  pntrsumbnd2  27070  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntpbnd1a  27088  pntpbnd1  27089  pntibndlem2a  27093  pntibndlem2  27094  pntlemg  27101  pntlemh  27102  pntlemj  27106  pntlemf  27108  ostth2lem1  27121  padicabvf  27134  padicabvcxp  27135  ostth2lem2  27137  ostth2lem3  27138  ostth2lem4  27139  ostth2  27140  ostth3  27141  numclwwlk5  29641  numclwwlk7  29644  nrt2irr  29726  ubthlem2  30124  minvecolem4  30133  iundisjf  31820  ssnnssfz  31998  iundisjfi  32007  pfxlsw2ccat  32116  pmtrto1cl  32258  psgnfzto1stlem  32259  fzto1st1  32261  fzto1st  32262  psgnfzto1st  32264  cycpmco2lem6  32290  cycpmco2lem7  32291  smatrcl  32776  smattr  32779  smatbl  32780  smatbr  32781  1smat1  32784  submateqlem1  32787  submateqlem2  32788  submateq  32789  esumcst  33061  fiunelros  33172  oddpwdc  33353  eulerpartlems  33359  eulerpartlemgc  33361  fiblem  33397  dstfrvunirn  33473  dstfrvclim1  33476  ballotlemimin  33504  fsum2dsub  33619  reprinfz1  33634  hgt750lemd  33660  hgt750lemb  33668  hgt750leme  33670  tgoldbachgtde  33672  tgoldbachgt  33675  subfaclim  34179  subfacval3  34180  erdszelem7  34188  erdszelem8  34189  erdsze2lem2  34195  cvmliftlem2  34277  cvmliftlem6  34281  cvmliftlem7  34282  cvmliftlem8  34283  cvmliftlem9  34284  cvmliftlem10  34285  cvmliftlem13  34287  bcprod  34708  bccolsum  34709  faclimlem2  34714  faclim2  34718  nn0prpwlem  35207  knoppndvlem15  35402  knoppndvlem17  35404  knoppndvlem18  35405  knoppndvlem19  35406  knoppndvlem20  35407  knoppndvlem21  35408  poimirlem3  36491  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem26  36514  poimirlem28  36516  opnmbllem0  36524  mblfinlem2  36526  incsequz  36616  nninfnub  36619  lcmineqlem4  40897  lcmineqlem10  40903  lcmineqlem11  40904  lcmineqlem15  40908  lcmineqlem18  40911  lcmineqlem19  40912  lcmineqlem20  40913  lcmineqlem21  40914  lcmineqlem22  40915  lcmineqlem23  40916  lcmineqlem  40917  3lexlogpow5ineq2  40920  3lexlogpow5ineq4  40921  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1p1p3  40934  aks4d1p1p2  40935  aks4d1p1p4  40936  aks4d1p1p5  40940  aks4d1p1  40941  aks4d1p3  40943  aks4d1p4  40944  aks4d1p5  40945  aks4d1p6  40946  aks4d1p7  40948  aks4d1p8d2  40950  aks4d1p8  40952  aks4d1p9  40953  2ap1caineq  40961  sticksstones1  40962  sticksstones2  40963  sticksstones3  40964  sticksstones6  40967  sticksstones7  40968  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  metakunt1  40985  metakunt2  40986  metakunt6  40990  metakunt7  40991  metakunt9  40993  metakunt10  40994  metakunt11  40995  metakunt12  40996  metakunt16  41000  metakunt18  41002  metakunt20  41004  metakunt22  41006  metakunt24  41008  metakunt27  41011  metakunt28  41012  metakunt29  41013  metakunt30  41014  nnadddir  41184  oexpreposd  41212  nn0expgcd  41226  rtprmirr  41237  flt4lem5e  41398  flt4lem6  41400  flt4lem7  41401  fltltc  41403  fltnltalem  41404  fltnlta  41405  3cubeslem3r  41425  irrapxlem3  41562  irrapxlem4  41563  irrapxlem5  41564  pellexlem2  41568  pellexlem6  41572  pell14qrgt0  41597  pell14qrgapw  41614  pellfundgt1  41621  rmspecsqrtnq  41644  ltrmxnn0  41688  jm3.1lem1  41756  jm3.1lem3  41758  dgraa0p  41891  hashnzfz2  43080  rfcnnnub  43720  nnxrd  43983  fzisoeu  44010  fsumnncl  44288  sumnnodd  44346  limsup10exlem  44488  stoweidlem1  44717  stoweidlem3  44719  stoweidlem11  44727  stoweidlem17  44733  stoweidlem20  44736  stoweidlem25  44741  stoweidlem26  44742  stoweidlem34  44750  stoweidlem38  44754  stoweidlem42  44758  stoweidlem44  44760  stoweidlem51  44767  stoweidlem59  44775  stoweidlem60  44776  wallispi  44786  wallispi2  44789  stirlinglem3  44792  stirlinglem4  44793  stirlinglem8  44797  stirlinglem10  44799  stirlinglem12  44801  stirlinglem15  44804  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkercncflem2  44820  fourierdlem11  44834  fourierdlem14  44837  fourierdlem15  44838  fourierdlem20  44843  fourierdlem31  44854  fourierdlem64  44886  fourierdlem93  44915  fourierdlem95  44917  fourierdlem103  44925  fourierdlem104  44926  fourierdlem112  44934  sqwvfourb  44945  etransclem3  44953  etransclem19  44969  etransclem23  44973  etransclem24  44974  etransclem25  44975  etransclem32  44982  etransclem35  44985  etransclem41  44991  etransclem48  44998  qndenserrnbllem  45010  hoiqssbllem1  45338  hoiqssbllem2  45339  ovolval5lem1  45368  ovolval5lem2  45369  iccpartlt  46092  iccpartgt  46095  odz2prm2pw  46231  fmtnoprmfac1lem  46232  2pwp1prm  46257  sfprmdvdsmersenne  46271  lighneallem2  46274  proththdlem  46281  perfectALTVlem2  46390  gbowge7  46431  ztprmneprm  47023  pgrple2abl  47041  logbpw2m1  47253  nnpw2pmod  47269  nnolog2flm1  47276  blennngt2o2  47278  itcovalt2lem2lem1  47359