Theorem nnred 12281

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11154  ℕcn 12266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267

This theorem is referenced by:  nnne0  12300  uzwo3  12985  modmulnn  13929  bernneq3  14270  expmulnbnd  14274  expnngt1b  14281  facwordi  14328  faclbnd  14329  faclbnd2  14330  faclbnd3  14331  faclbnd5  14337  faclbnd6  14338  facubnd  14339  facavg  14340  bcp1nk  14356  hashf1  14496  swrds2  14979  isercolllem1  15701  isercoll  15704  o1fsum  15849  climcndslem1  15885  climcndslem2  15886  climcnds  15887  eftabs  16111  efcllem  16113  ege2le3  16126  efcj  16128  eftlub  16145  eflegeo  16157  eirrlem  16240  fzm1ndvds  16359  nno  16419  nnoddm1d2  16423  bitsfzolem  16471  bitsfzo  16472  bitsinv1lem  16478  sadcaddlem  16494  smueqlem  16527  bezoutlem3  16578  bezoutlem4  16579  sqgcd  16599  nn0expgcd  16601  lcmgcdlem  16643  lcmf  16670  prmind2  16722  coprm  16748  prmfac1  16757  prmndvdsfaclt  16762  divdenle  16786  qnumgt0  16787  zsqrtelqelz  16795  hashdvds  16812  eulerthlem2  16819  odzdvds  16833  vfermltl  16839  modprm0  16843  pythagtriplem11  16863  pythagtriplem13  16865  pythagtriplem19  16871  pclem  16876  pcpre1  16880  pcidlem  16910  dvdsprmpweqle  16924  pcadd  16927  pcmpt  16930  pcmpt2  16931  pcfaclem  16936  pcfac  16937  qexpz  16939  pockthlem  16943  pockthg  16944  prmreclem1  16954  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  1arithlem4  16964  1arith  16965  4sqlem5  16980  4sqlem6  16981  4sqlem10  16985  mul4sqlem  16991  4sqlem11  16993  4sqlem12  16994  4sqlem13  16995  4sqlem14  16996  4sqlem15  16997  4sqlem16  16998  4sqlem17  16999  vdwlem1  17019  vdwlem3  17021  vdwlem6  17024  vdwlem9  17027  vdwlem10  17028  vdwlem12  17030  vdwnnlem3  17035  ramub1lem1  17064  prmolefac  17084  prmgaplem4  17092  prmgaplem5  17093  prmgaplem6  17094  prmgaplem8  17096  2expltfac  17130  cshwshashnsame  17141  setsstruct2  17211  psgnunilem4  19515  mndodconglem  19559  oddvds  19565  sylow1lem1  19616  sylow1lem5  19620  fislw  19643  efgredlem  19765  gexexlem  19870  zringlpirlem3  21475  prmirredlem  21483  fvmptnn04if  22855  fvmptnn04ifb  22857  fvmptnn04ifc  22858  fvmptnn04ifd  22859  chfacfisf  22860  chfacfisfcpmat  22861  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  lebnumii  24998  lmnn  25297  ovolunlem1a  25531  ovoliunlem1  25537  ovolicc2lem3  25554  ovolicc2lem4  25555  iundisj  25583  voliunlem1  25585  uniioombllem3  25620  dyadf  25626  dyadovol  25628  dyaddisjlem  25630  dyadmaxlem  25632  opnmbllem  25636  vitalilem4  25646  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  itg2gt0  25795  itg2cnlem2  25797  dgreq0  26305  dgrco  26315  elqaalem2  26362  aaliou3lem2  26385  aaliou3lem8  26387  aaliou3lem9  26392  rtprmirr  26803  leibpi  26985  log2tlbnd  26988  birthdaylem3  26996  amgm  27034  emcllem2  27040  harmonicbnd4  27054  lgamgulmlem1  27072  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamucov  27081  lgamcvg2  27098  wilthlem1  27111  ftalem5  27120  basellem1  27124  basellem2  27125  basellem3  27126  basellem4  27127  basellem5  27128  basellem6  27129  basellem8  27131  chtge0  27155  chtwordi  27199  vma1  27209  dvdsflf1o  27230  dvdsflsumcom  27231  fsumfldivdiaglem  27232  sgmmul  27245  chtublem  27255  fsumvma2  27258  logfac2  27261  chpchtsum  27263  chpub  27264  logfaclbnd  27266  logexprlim  27269  mersenne  27271  perfectlem2  27274  dchrelbas4  27287  bposlem1  27328  bposlem2  27329  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem7  27334  bposlem9  27336  lgslem1  27341  lgsval2lem  27351  lgsdirprm  27375  lgsdir  27376  lgsne0  27379  lgsqrlem2  27391  gausslemma2dlem0h  27407  gausslemma2dlem0i  27408  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem7  27417  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgseisen  27423  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  2sqlem3  27464  2sqlem8  27470  2sqblem  27475  2sqmod  27480  chebbnd1lem1  27513  chebbnd1lem3  27515  chtppilimlem1  27517  rplogsumlem1  27528  rplogsumlem2  27529  dchrisum0lem1a  27530  rpvmasumlem  27531  dchrisumlema  27532  dchrisumlem1  27533  dchrisumlem2  27534  dchrisumlem3  27535  dchrvmasumiflem1  27545  dchrisum0flblem2  27553  dchrisum0re  27557  dchrisum0lem1b  27559  dchrisum0lem1  27560  dirith2  27572  selbergb  27593  selberg2lem  27594  logdivbnd  27600  selberg3lem2  27602  selberg4lem1  27604  pntrsumo1  27609  pntrsumbnd2  27611  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntpbnd1a  27629  pntpbnd1  27630  pntibndlem2a  27634  pntibndlem2  27635  pntlemg  27642  pntlemh  27643  pntlemj  27647  pntlemf  27649  ostth2lem1  27662  padicabvf  27675  padicabvcxp  27676  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ostth2  27681  ostth3  27682  numclwwlk5  30407  numclwwlk7  30410  nrt2irr  30492  ubthlem2  30890  minvecolem4  30899  iundisjf  32602  ssnnssfz  32789  iundisjfi  32798  nexple  32833  2exple2exp  32834  pfxlsw2ccat  32935  chnub  33002  pmtrto1cl  33119  psgnfzto1stlem  33120  fzto1st1  33122  fzto1st  33123  psgnfzto1st  33125  cycpmco2lem6  33151  cycpmco2lem7  33152  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  fldext2rspun  33732  smatrcl  33795  smattr  33798  smatbl  33799  smatbr  33800  1smat1  33803  submateqlem1  33806  submateqlem2  33807  submateq  33808  esumcst  34064  fiunelros  34175  oddpwdc  34356  eulerpartlems  34362  eulerpartlemgc  34364  fiblem  34400  dstfrvunirn  34477  dstfrvclim1  34480  ballotlemimin  34508  fsum2dsub  34622  reprinfz1  34637  hgt750lemd  34663  hgt750lemb  34671  hgt750leme  34673  tgoldbachgtde  34675  tgoldbachgt  34678  subfaclim  35193  subfacval3  35194  erdszelem7  35202  erdszelem8  35203  erdsze2lem2  35209  cvmliftlem2  35291  cvmliftlem6  35295  cvmliftlem7  35296  cvmliftlem8  35297  cvmliftlem9  35298  cvmliftlem10  35299  cvmliftlem13  35301  bcprod  35738  bccolsum  35739  faclimlem2  35744  faclim2  35748  nn0prpwlem  36323  knoppcnlem10  36503  knoppndvlem15  36527  knoppndvlem17  36529  knoppndvlem18  36530  knoppndvlem19  36531  knoppndvlem20  36532  knoppndvlem21  36533  poimirlem3  37630  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem26  37653  poimirlem28  37655  opnmbllem0  37663  mblfinlem2  37665  incsequz  37755  nninfnub  37758  lcmineqlem4  42033  lcmineqlem10  42039  lcmineqlem11  42040  lcmineqlem15  42044  lcmineqlem18  42047  lcmineqlem19  42048  lcmineqlem20  42049  lcmineqlem21  42050  lcmineqlem22  42051  lcmineqlem23  42052  lcmineqlem  42053  3lexlogpow5ineq2  42056  3lexlogpow5ineq4  42057  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p3  42079  aks4d1p4  42080  aks4d1p5  42081  aks4d1p6  42082  aks4d1p7  42084  aks4d1p8d2  42086  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  primrootlekpowne0  42106  primrootspoweq0  42107  aks6d1c1  42117  hashscontpow1  42122  aks6d1c3  42124  aks6d1c4  42125  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c5lem1  42137  2ap1caineq  42146  sticksstones1  42147  sticksstones2  42148  sticksstones3  42149  sticksstones6  42152  sticksstones7  42153  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem4  42174  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  aks6d1c7lem2  42182  unitscyglem1  42196  unitscyglem2  42197  unitscyglem4  42199  unitscyglem5  42200  aks5lem8  42202  metakunt1  42206  metakunt2  42207  metakunt6  42211  metakunt7  42212  metakunt9  42214  metakunt10  42215  metakunt11  42216  metakunt12  42217  metakunt16  42221  metakunt18  42223  metakunt20  42225  metakunt22  42227  metakunt24  42229  metakunt27  42232  metakunt28  42233  metakunt29  42234  metakunt30  42235  nnadddir  42305  oexpreposd  42357  fimgmcyclem  42543  fimgmcyc  42544  flt4lem5e  42666  flt4lem6  42668  flt4lem7  42669  fltltc  42671  fltnltalem  42672  fltnlta  42673  3cubeslem3r  42698  irrapxlem3  42835  irrapxlem4  42836  irrapxlem5  42837  pellexlem2  42841  pellexlem6  42845  pell14qrgt0  42870  pell14qrgapw  42887  pellfundgt1  42894  rmspecsqrtnq  42917  ltrmxnn0  42961  jm3.1lem1  43029  jm3.1lem3  43031  dgraa0p  43161  hashnzfz2  44340  rfcnnnub  45041  nnxrd  45285  fzisoeu  45312  fsumnncl  45587  sumnnodd  45645  limsup10exlem  45787  stoweidlem1  46016  stoweidlem3  46018  stoweidlem11  46026  stoweidlem17  46032  stoweidlem20  46035  stoweidlem25  46040  stoweidlem26  46041  stoweidlem34  46049  stoweidlem38  46053  stoweidlem42  46057  stoweidlem44  46059  stoweidlem51  46066  stoweidlem59  46074  stoweidlem60  46075  wallispi  46085  wallispi2  46088  stirlinglem3  46091  stirlinglem4  46092  stirlinglem8  46096  stirlinglem10  46098  stirlinglem12  46100  stirlinglem15  46103  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkercncflem2  46119  fourierdlem11  46133  fourierdlem14  46136  fourierdlem15  46137  fourierdlem20  46142  fourierdlem31  46153  fourierdlem64  46185  fourierdlem93  46214  fourierdlem95  46216  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  sqwvfourb  46244  etransclem3  46252  etransclem19  46268  etransclem23  46272  etransclem24  46273  etransclem25  46274  etransclem32  46281  etransclem35  46284  etransclem41  46290  etransclem48  46297  qndenserrnbllem  46309  hoiqssbllem1  46637  hoiqssbllem2  46638  ovolval5lem1  46667  ovolval5lem2  46668  iccpartlt  47411  iccpartgt  47414  odz2prm2pw  47550  fmtnoprmfac1lem  47551  2pwp1prm  47576  sfprmdvdsmersenne  47590  lighneallem2  47593  proththdlem  47600  perfectALTVlem2  47709  gbowge7  47750  ztprmneprm  48263  pgrple2abl  48281  logbpw2m1  48488  nnpw2pmod  48504  nnolog2flm1  48511  blennngt2o2  48513  itcovalt2lem2lem1  48594