Theorem nnred 12208

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11074  ℕcn 12193

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194

This theorem is referenced by:  nnne0  12227  uzwo3  12909  modmulnn  13858  bernneq3  14203  expmulnbnd  14207  expnngt1b  14214  facwordi  14261  faclbnd  14262  faclbnd2  14263  faclbnd3  14264  faclbnd5  14270  faclbnd6  14271  facubnd  14272  facavg  14273  bcp1nk  14289  hashf1  14429  swrds2  14913  isercolllem1  15638  isercoll  15641  o1fsum  15786  climcndslem1  15822  climcndslem2  15823  climcnds  15824  eftabs  16048  efcllem  16050  ege2le3  16063  efcj  16065  eftlub  16084  eflegeo  16096  eirrlem  16179  fzm1ndvds  16299  nno  16359  nnoddm1d2  16363  bitsfzolem  16411  bitsfzo  16412  bitsinv1lem  16418  sadcaddlem  16434  smueqlem  16467  bezoutlem3  16518  bezoutlem4  16519  sqgcd  16539  nn0expgcd  16541  lcmgcdlem  16583  lcmf  16610  prmind2  16662  coprm  16688  prmfac1  16697  prmndvdsfaclt  16702  divdenle  16726  qnumgt0  16727  zsqrtelqelz  16735  hashdvds  16752  eulerthlem2  16759  odzdvds  16773  vfermltl  16779  modprm0  16783  pythagtriplem11  16803  pythagtriplem13  16805  pythagtriplem19  16811  pclem  16816  pcpre1  16820  pcidlem  16850  dvdsprmpweqle  16864  pcadd  16867  pcmpt  16870  pcmpt2  16871  pcfaclem  16876  pcfac  16877  qexpz  16879  pockthlem  16883  pockthg  16884  prmreclem1  16894  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  1arithlem4  16904  1arith  16905  4sqlem5  16920  4sqlem6  16921  4sqlem10  16925  mul4sqlem  16931  4sqlem11  16933  4sqlem12  16934  4sqlem13  16935  4sqlem14  16936  4sqlem15  16937  4sqlem16  16938  4sqlem17  16939  vdwlem1  16959  vdwlem3  16961  vdwlem6  16964  vdwlem9  16967  vdwlem10  16968  vdwlem12  16970  vdwnnlem3  16975  ramub1lem1  17004  prmolefac  17024  prmgaplem4  17032  prmgaplem5  17033  prmgaplem6  17034  prmgaplem8  17036  2expltfac  17070  cshwshashnsame  17081  setsstruct2  17151  psgnunilem4  19434  mndodconglem  19478  oddvds  19484  sylow1lem1  19535  sylow1lem5  19539  fislw  19562  efgredlem  19684  gexexlem  19789  zringlpirlem3  21381  prmirredlem  21389  fvmptnn04if  22743  fvmptnn04ifb  22745  fvmptnn04ifc  22746  fvmptnn04ifd  22747  chfacfisf  22748  chfacfisfcpmat  22749  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  lebnumii  24872  lmnn  25170  ovolunlem1a  25404  ovoliunlem1  25410  ovolicc2lem3  25427  ovolicc2lem4  25428  iundisj  25456  voliunlem1  25458  uniioombllem3  25493  dyadf  25499  dyadovol  25501  dyaddisjlem  25503  dyadmaxlem  25505  opnmbllem  25509  vitalilem4  25519  mbfi1fseqlem1  25623  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  itg2gt0  25668  itg2cnlem2  25670  dgreq0  26178  dgrco  26188  elqaalem2  26235  aaliou3lem2  26258  aaliou3lem8  26260  aaliou3lem9  26265  rtprmirr  26677  leibpi  26859  log2tlbnd  26862  birthdaylem3  26870  amgm  26908  emcllem2  26914  harmonicbnd4  26928  lgamgulmlem1  26946  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem4  26949  lgamgulmlem5  26950  lgamgulmlem6  26951  lgamucov  26955  lgamcvg2  26972  wilthlem1  26985  ftalem5  26994  basellem1  26998  basellem2  26999  basellem3  27000  basellem4  27001  basellem5  27002  basellem6  27003  basellem8  27005  chtge0  27029  chtwordi  27073  vma1  27083  dvdsflf1o  27104  dvdsflsumcom  27105  fsumfldivdiaglem  27106  sgmmul  27119  chtublem  27129  fsumvma2  27132  logfac2  27135  chpchtsum  27137  chpub  27138  logfaclbnd  27140  logexprlim  27143  mersenne  27145  perfectlem2  27148  dchrelbas4  27161  bposlem1  27202  bposlem2  27203  bposlem3  27204  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem7  27208  bposlem9  27210  lgslem1  27215  lgsval2lem  27225  lgsdirprm  27249  lgsdir  27250  lgsne0  27253  lgsqrlem2  27265  gausslemma2dlem0h  27281  gausslemma2dlem0i  27282  gausslemma2dlem1a  27283  gausslemma2dlem2  27285  gausslemma2dlem7  27291  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgseisen  27297  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  2sqlem3  27338  2sqlem8  27344  2sqblem  27349  2sqmod  27354  chebbnd1lem1  27387  chebbnd1lem3  27389  chtppilimlem1  27391  rplogsumlem1  27402  rplogsumlem2  27403  dchrisum0lem1a  27404  rpvmasumlem  27405  dchrisumlema  27406  dchrisumlem1  27407  dchrisumlem2  27408  dchrisumlem3  27409  dchrvmasumiflem1  27419  dchrisum0flblem2  27427  dchrisum0re  27431  dchrisum0lem1b  27433  dchrisum0lem1  27434  dirith2  27446  selbergb  27467  selberg2lem  27468  logdivbnd  27474  selberg3lem2  27476  selberg4lem1  27478  pntrsumo1  27483  pntrsumbnd2  27485  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntpbnd1a  27503  pntpbnd1  27504  pntibndlem2a  27508  pntibndlem2  27509  pntlemg  27516  pntlemh  27517  pntlemj  27521  pntlemf  27523  ostth2lem1  27536  padicabvf  27549  padicabvcxp  27550  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  ostth2  27555  ostth3  27556  numclwwlk5  30324  numclwwlk7  30327  nrt2irr  30409  ubthlem2  30807  minvecolem4  30816  iundisjf  32525  ssnnssfz  32717  iundisjfi  32726  nexple  32776  2exple2exp  32777  pfxlsw2ccat  32879  chnub  32945  pmtrto1cl  33063  psgnfzto1stlem  33064  fzto1st1  33066  fzto1st  33067  psgnfzto1st  33069  cycpmco2lem6  33095  cycpmco2lem7  33096  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  fldext2rspun  33684  smatrcl  33793  smattr  33796  smatbl  33797  smatbr  33798  1smat1  33801  submateqlem1  33804  submateqlem2  33805  submateq  33806  esumcst  34060  fiunelros  34171  oddpwdc  34352  eulerpartlems  34358  eulerpartlemgc  34360  fiblem  34396  dstfrvunirn  34473  dstfrvclim1  34476  ballotlemimin  34504  fsum2dsub  34605  reprinfz1  34620  hgt750lemd  34646  hgt750lemb  34654  hgt750leme  34656  tgoldbachgtde  34658  tgoldbachgt  34661  subfaclim  35182  subfacval3  35183  erdszelem7  35191  erdszelem8  35192  erdsze2lem2  35198  cvmliftlem2  35280  cvmliftlem6  35284  cvmliftlem7  35285  cvmliftlem8  35286  cvmliftlem9  35287  cvmliftlem10  35288  cvmliftlem13  35290  bcprod  35732  bccolsum  35733  faclimlem2  35738  faclim2  35742  nn0prpwlem  36317  knoppcnlem10  36497  knoppndvlem15  36521  knoppndvlem17  36523  knoppndvlem18  36524  knoppndvlem19  36525  knoppndvlem20  36526  knoppndvlem21  36527  poimirlem3  37624  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem26  37647  poimirlem28  37649  opnmbllem0  37657  mblfinlem2  37659  incsequz  37749  nninfnub  37752  lcmineqlem4  42027  lcmineqlem10  42033  lcmineqlem11  42034  lcmineqlem15  42038  lcmineqlem18  42041  lcmineqlem19  42042  lcmineqlem20  42043  lcmineqlem21  42044  lcmineqlem22  42045  lcmineqlem23  42046  lcmineqlem  42047  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p3  42073  aks4d1p4  42074  aks4d1p5  42075  aks4d1p6  42076  aks4d1p7  42078  aks4d1p8d2  42080  aks4d1p8  42082  aks4d1p9  42083  posbezout  42095  primrootlekpowne0  42100  primrootspoweq0  42101  aks6d1c1  42111  hashscontpow1  42116  aks6d1c3  42118  aks6d1c4  42119  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c5lem1  42131  2ap1caineq  42140  sticksstones1  42141  sticksstones2  42142  sticksstones3  42143  sticksstones6  42146  sticksstones7  42147  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem4  42168  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  aks6d1c7lem2  42176  unitscyglem1  42190  unitscyglem2  42191  unitscyglem4  42193  unitscyglem5  42194  aks5lem8  42196  nnadddir  42265  oexpreposd  42317  fimgmcyclem  42528  fimgmcyc  42529  flt4lem5e  42651  flt4lem6  42653  flt4lem7  42654  fltltc  42656  fltnltalem  42657  fltnlta  42658  3cubeslem3r  42682  irrapxlem3  42819  irrapxlem4  42820  irrapxlem5  42821  pellexlem2  42825  pellexlem6  42829  pell14qrgt0  42854  pell14qrgapw  42871  pellfundgt1  42878  rmspecsqrtnq  42901  ltrmxnn0  42945  jm3.1lem1  43013  jm3.1lem3  43015  dgraa0p  43145  hashnzfz2  44317  rfcnnnub  45037  nnxrd  45279  fzisoeu  45305  fsumnncl  45577  sumnnodd  45635  limsup10exlem  45777  stoweidlem1  46006  stoweidlem3  46008  stoweidlem11  46016  stoweidlem17  46022  stoweidlem20  46025  stoweidlem25  46030  stoweidlem26  46031  stoweidlem34  46039  stoweidlem38  46043  stoweidlem42  46047  stoweidlem44  46049  stoweidlem51  46056  stoweidlem59  46064  stoweidlem60  46065  wallispi  46075  wallispi2  46078  stirlinglem3  46081  stirlinglem4  46082  stirlinglem8  46086  stirlinglem10  46088  stirlinglem12  46090  stirlinglem15  46093  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkercncflem2  46109  fourierdlem11  46123  fourierdlem14  46126  fourierdlem15  46127  fourierdlem20  46132  fourierdlem31  46143  fourierdlem64  46175  fourierdlem93  46204  fourierdlem95  46206  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  sqwvfourb  46234  etransclem3  46242  etransclem19  46258  etransclem23  46262  etransclem24  46263  etransclem25  46264  etransclem32  46271  etransclem35  46274  etransclem41  46280  etransclem48  46287  qndenserrnbllem  46299  hoiqssbllem1  46627  hoiqssbllem2  46628  ovolval5lem1  46657  ovolval5lem2  46658  iccpartlt  47429  iccpartgt  47432  odz2prm2pw  47568  fmtnoprmfac1lem  47569  2pwp1prm  47594  sfprmdvdsmersenne  47608  lighneallem2  47611  proththdlem  47618  perfectALTVlem2  47727  gbowge7  47768  ztprmneprm  48339  pgrple2abl  48357  logbpw2m1  48560  nnpw2pmod  48576  nnolog2flm1  48583  blennngt2o2  48585  itcovalt2lem2lem1  48666