Theorem nnred 11997

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 10879  ℕcn 11982

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 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-i2m1 10948  ax-1ne0 10949  ax-rrecex 10952  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-nn 11983

This theorem is referenced by:  nnne0  12016  uzwo3  12692  modmulnn  13618  bernneq3  13955  expmulnbnd  13959  expnngt1b  13966  facwordi  14012  faclbnd  14013  faclbnd2  14014  faclbnd3  14015  faclbnd5  14021  faclbnd6  14022  facubnd  14023  facavg  14024  bcp1nk  14040  hashf1  14180  swrds2  14662  isercolllem1  15385  isercoll  15388  o1fsum  15534  climcndslem1  15570  climcndslem2  15571  climcnds  15572  eftabs  15794  efcllem  15796  ege2le3  15808  efcj  15810  eftlub  15827  eflegeo  15839  eirrlem  15922  fzm1ndvds  16040  nno  16100  nnoddm1d2  16104  bitsfzolem  16150  bitsfzo  16151  bitsinv1lem  16157  sadcaddlem  16173  smueqlem  16206  bezoutlem3  16258  bezoutlem4  16259  sqgcd  16279  lcmgcdlem  16320  lcmf  16347  prmind2  16399  coprm  16425  prmfac1  16435  prmndvdsfaclt  16439  divdenle  16462  qnumgt0  16463  zsqrtelqelz  16471  hashdvds  16485  eulerthlem2  16492  odzdvds  16505  vfermltl  16511  modprm0  16515  pythagtriplem11  16535  pythagtriplem13  16537  pythagtriplem19  16543  pclem  16548  pcpre1  16552  pcidlem  16582  dvdsprmpweqle  16596  pcadd  16599  pcmpt  16602  pcmpt2  16603  pcfaclem  16608  pcfac  16609  qexpz  16611  pockthlem  16615  pockthg  16616  prmreclem1  16626  prmreclem3  16628  prmreclem4  16629  prmreclem5  16630  1arithlem4  16636  1arith  16637  4sqlem5  16652  4sqlem6  16653  4sqlem10  16657  mul4sqlem  16663  4sqlem11  16665  4sqlem12  16666  4sqlem13  16667  4sqlem14  16668  4sqlem15  16669  4sqlem16  16670  4sqlem17  16671  vdwlem1  16691  vdwlem3  16693  vdwlem6  16696  vdwlem9  16699  vdwlem10  16700  vdwlem12  16702  vdwnnlem3  16707  ramub1lem1  16736  prmolefac  16756  prmgaplem4  16764  prmgaplem5  16765  prmgaplem6  16766  prmgaplem8  16768  2expltfac  16803  cshwshashnsame  16814  setsstruct2  16884  psgnunilem4  19114  mndodconglem  19158  oddvds  19164  sylow1lem1  19212  sylow1lem5  19216  fislw  19239  efgredlem  19362  gexexlem  19462  zringlpirlem3  20695  prmirredlem  20703  fvmptnn04if  22007  fvmptnn04ifb  22009  fvmptnn04ifc  22010  fvmptnn04ifd  22011  chfacfisf  22012  chfacfisfcpmat  22013  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  lebnumii  24138  lmnn  24436  ovolunlem1a  24669  ovoliunlem1  24675  ovolicc2lem3  24692  ovolicc2lem4  24693  iundisj  24721  voliunlem1  24723  uniioombllem3  24758  dyadf  24764  dyadovol  24766  dyaddisjlem  24768  dyadmaxlem  24770  opnmbllem  24774  vitalilem4  24784  mbfi1fseqlem1  24889  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfi1fseqlem6  24894  itg2gt0  24934  itg2cnlem2  24936  dgreq0  25435  dgrco  25445  elqaalem2  25489  aaliou3lem2  25512  aaliou3lem8  25514  aaliou3lem9  25519  leibpi  26101  log2tlbnd  26104  birthdaylem3  26112  amgm  26149  emcllem2  26155  harmonicbnd4  26169  lgamgulmlem1  26187  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem4  26190  lgamgulmlem5  26191  lgamgulmlem6  26192  lgamucov  26196  lgamcvg2  26213  wilthlem1  26226  ftalem5  26235  basellem1  26239  basellem2  26240  basellem3  26241  basellem4  26242  basellem5  26243  basellem6  26244  basellem8  26246  chtge0  26270  chtwordi  26314  vma1  26324  dvdsflf1o  26345  dvdsflsumcom  26346  fsumfldivdiaglem  26347  sgmmul  26358  chtublem  26368  fsumvma2  26371  logfac2  26374  chpchtsum  26376  chpub  26377  logfaclbnd  26379  logexprlim  26382  mersenne  26384  perfectlem2  26387  dchrelbas4  26400  bposlem1  26441  bposlem2  26442  bposlem3  26443  bposlem4  26444  bposlem5  26445  bposlem6  26446  bposlem7  26447  bposlem9  26449  lgslem1  26454  lgsval2lem  26464  lgsdirprm  26488  lgsdir  26489  lgsne0  26492  lgsqrlem2  26504  gausslemma2dlem0h  26520  gausslemma2dlem0i  26521  gausslemma2dlem1a  26522  gausslemma2dlem2  26524  gausslemma2dlem7  26530  gausslemma2d  26531  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgseisen  26536  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  2sqlem3  26577  2sqlem8  26583  2sqblem  26588  2sqmod  26593  chebbnd1lem1  26626  chebbnd1lem3  26628  chtppilimlem1  26630  rplogsumlem1  26641  rplogsumlem2  26642  dchrisum0lem1a  26643  rpvmasumlem  26644  dchrisumlema  26645  dchrisumlem1  26646  dchrisumlem2  26647  dchrisumlem3  26648  dchrvmasumiflem1  26658  dchrisum0flblem2  26666  dchrisum0re  26670  dchrisum0lem1b  26672  dchrisum0lem1  26673  dirith2  26685  selbergb  26706  selberg2lem  26707  logdivbnd  26713  selberg3lem2  26715  selberg4lem1  26717  pntrsumo1  26722  pntrsumbnd2  26724  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntpbnd1a  26742  pntpbnd1  26743  pntibndlem2a  26747  pntibndlem2  26748  pntlemg  26755  pntlemh  26756  pntlemj  26760  pntlemf  26762  ostth2lem1  26775  padicabvf  26788  padicabvcxp  26789  ostth2lem2  26791  ostth2lem3  26792  ostth2lem4  26793  ostth2  26794  ostth3  26795  numclwwlk5  28761  numclwwlk7  28764  ubthlem2  29242  minvecolem4  29251  iundisjf  30937  ssnnssfz  31117  iundisjfi  31126  pfxlsw2ccat  31233  pmtrto1cl  31375  psgnfzto1stlem  31376  fzto1st1  31378  fzto1st  31379  psgnfzto1st  31381  cycpmco2lem6  31407  cycpmco2lem7  31408  smatrcl  31755  smattr  31758  smatbl  31759  smatbr  31760  1smat1  31763  submateqlem1  31766  submateqlem2  31767  submateq  31768  esumcst  32040  fiunelros  32151  oddpwdc  32330  eulerpartlems  32336  eulerpartlemgc  32338  fiblem  32374  dstfrvunirn  32450  dstfrvclim1  32453  ballotlemimin  32481  fsum2dsub  32596  reprinfz1  32611  hgt750lemd  32637  hgt750lemb  32645  hgt750leme  32647  tgoldbachgtde  32649  tgoldbachgt  32652  subfaclim  33159  subfacval3  33160  erdszelem7  33168  erdszelem8  33169  erdsze2lem2  33175  cvmliftlem2  33257  cvmliftlem6  33261  cvmliftlem7  33262  cvmliftlem8  33263  cvmliftlem9  33264  cvmliftlem10  33265  cvmliftlem13  33267  bcprod  33713  bccolsum  33714  faclimlem2  33719  faclim2  33723  nn0prpwlem  34520  knoppndvlem15  34715  knoppndvlem17  34717  knoppndvlem18  34718  knoppndvlem19  34719  knoppndvlem20  34720  knoppndvlem21  34721  poimirlem3  35789  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem9  35795  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem13  35799  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem26  35812  poimirlem28  35814  opnmbllem0  35822  mblfinlem2  35824  incsequz  35915  nninfnub  35918  lcmineqlem4  40047  lcmineqlem10  40053  lcmineqlem11  40054  lcmineqlem15  40058  lcmineqlem18  40061  lcmineqlem19  40062  lcmineqlem20  40063  lcmineqlem21  40064  lcmineqlem22  40065  lcmineqlem23  40066  lcmineqlem  40067  3lexlogpow5ineq2  40070  3lexlogpow5ineq4  40071  3lexlogpow2ineq2  40074  3lexlogpow5ineq5  40075  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p3  40093  aks4d1p4  40094  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7  40098  aks4d1p8d2  40100  aks4d1p8  40102  aks4d1p9  40103  2ap1caineq  40108  sticksstones1  40109  sticksstones2  40110  sticksstones3  40111  sticksstones6  40114  sticksstones7  40115  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  metakunt1  40132  metakunt2  40133  metakunt6  40137  metakunt7  40138  metakunt9  40140  metakunt10  40141  metakunt11  40142  metakunt12  40143  metakunt16  40147  metakunt18  40149  metakunt20  40151  metakunt22  40153  metakunt24  40155  metakunt27  40158  metakunt28  40159  metakunt29  40160  metakunt30  40161  nnadddir  40307  oexpreposd  40328  nn0expgcd  40342  rtprmirr  40354  flt4lem5e  40500  flt4lem6  40502  flt4lem7  40503  fltltc  40505  fltnltalem  40506  fltnlta  40507  3cubeslem3r  40516  irrapxlem3  40653  irrapxlem4  40654  irrapxlem5  40655  pellexlem2  40659  pellexlem6  40663  pell14qrgt0  40688  pell14qrgapw  40705  pellfundgt1  40712  rmspecsqrtnq  40735  ltrmxnn0  40778  jm3.1lem1  40846  jm3.1lem3  40848  dgraa0p  40981  hashnzfz2  41946  rfcnnnub  42586  nnxrd  42592  fzisoeu  42846  fsumnncl  43120  sumnnodd  43178  limsup10exlem  43320  stoweidlem1  43549  stoweidlem3  43551  stoweidlem11  43559  stoweidlem17  43565  stoweidlem20  43568  stoweidlem25  43573  stoweidlem26  43574  stoweidlem34  43582  stoweidlem38  43586  stoweidlem42  43590  stoweidlem44  43592  stoweidlem51  43599  stoweidlem59  43607  stoweidlem60  43608  wallispi  43618  wallispi2  43621  stirlinglem3  43624  stirlinglem4  43625  stirlinglem8  43629  stirlinglem10  43631  stirlinglem12  43633  stirlinglem15  43636  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkercncflem2  43652  fourierdlem11  43666  fourierdlem14  43669  fourierdlem15  43670  fourierdlem20  43675  fourierdlem31  43686  fourierdlem64  43718  fourierdlem93  43747  fourierdlem95  43749  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  sqwvfourb  43777  etransclem3  43785  etransclem19  43801  etransclem23  43805  etransclem24  43806  etransclem25  43807  etransclem32  43814  etransclem35  43817  etransclem41  43823  etransclem48  43830  qndenserrnbllem  43842  hoiqssbllem1  44167  hoiqssbllem2  44168  ovolval5lem1  44197  ovolval5lem2  44198  iccpartlt  44887  iccpartgt  44890  odz2prm2pw  45026  fmtnoprmfac1lem  45027  2pwp1prm  45052  sfprmdvdsmersenne  45066  lighneallem2  45069  proththdlem  45076  perfectALTVlem2  45185  gbowge7  45226  ztprmneprm  45694  pgrple2abl  45712  logbpw2m1  45924  nnpw2pmod  45940  nnolog2flm1  45947  blennngt2o2  45949  itcovalt2lem2lem1  46030