Theorem nnred 11456

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

Syntax hints:   → wi 4   ∈ wcel 2050  ℝcr 10334  ℕcn 11439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-i2m1 10403  ax-1ne0 10404  ax-rrecex 10407  ax-cnre 10408

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-ov 6979  df-om 7397  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-nn 11440

This theorem is referenced by:  nnne0  11474  uzwo3  12157  modmulnn  13072  bernneq3  13407  expmulnbnd  13411  expnngt1b  13418  facwordi  13464  faclbnd  13465  faclbnd2  13466  faclbnd3  13467  faclbnd5  13473  faclbnd6  13474  facubnd  13475  facavg  13476  bcp1nk  13492  hashf1  13628  swrds2  14164  isercolllem1  14882  isercoll  14885  o1fsum  15028  climcndslem1  15064  climcndslem2  15065  climcnds  15066  eftabs  15289  efcllem  15291  ege2le3  15303  efcj  15305  eftlub  15322  eflegeo  15334  eirrlem  15417  fzm1ndvds  15532  nno  15593  nnoddm1d2  15597  bitsfzolem  15643  bitsfzo  15644  bitsinv1lem  15650  sadcaddlem  15666  smueqlem  15699  bezoutlem3  15745  bezoutlem4  15746  sqgcd  15765  lcmgcdlem  15806  lcmf  15833  prmind2  15885  coprm  15911  prmfac1  15919  prmndvdsfaclt  15923  divdenle  15945  qnumgt0  15946  zsqrtelqelz  15954  hashdvds  15968  eulerthlem2  15975  odzdvds  15988  vfermltl  15994  modprm0  15998  pythagtriplem11  16018  pythagtriplem13  16020  pythagtriplem19  16026  pclem  16031  pcpre1  16035  pcidlem  16064  dvdsprmpweqle  16078  pcadd  16081  pcmpt  16084  pcmpt2  16085  pcfaclem  16090  pcfac  16091  qexpz  16093  pockthlem  16097  pockthg  16098  prmreclem1  16108  prmreclem3  16110  prmreclem4  16111  prmreclem5  16112  1arithlem4  16118  1arith  16119  4sqlem5  16134  4sqlem6  16135  4sqlem10  16139  mul4sqlem  16145  4sqlem11  16147  4sqlem12  16148  4sqlem13  16149  4sqlem14  16150  4sqlem15  16151  4sqlem16  16152  4sqlem17  16153  vdwlem1  16173  vdwlem3  16175  vdwlem6  16178  vdwlem9  16181  vdwlem10  16182  vdwlem12  16184  vdwnnlem3  16189  ramub1lem1  16218  prmolefac  16238  prmgaplem4  16246  prmgaplem5  16247  prmgaplem6  16248  prmgaplem8  16250  2expltfac  16282  cshwshashnsame  16293  setsstruct2  16377  psgnunilem4  18387  mndodconglem  18431  oddvds  18437  sylow1lem1  18484  sylow1lem5  18488  fislw  18511  efgredlem  18632  efgredlemOLD  18633  gexexlem  18728  zringlpirlem3  20335  prmirredlem  20342  fvmptnn04if  21161  fvmptnn04ifb  21163  fvmptnn04ifc  21164  fvmptnn04ifd  21165  chfacfisf  21166  chfacfisfcpmat  21167  chfacfscmulgsum  21172  chfacfpmmulgsum  21176  lebnumii  23273  lmnn  23569  ovolunlem1a  23800  ovoliunlem1  23806  ovolicc2lem3  23823  ovolicc2lem4  23824  iundisj  23852  voliunlem1  23854  uniioombllem3  23889  dyadf  23895  dyadovol  23897  dyaddisjlem  23899  dyadmaxlem  23901  opnmbllem  23905  vitalilem4  23915  mbfi1fseqlem1  24019  mbfi1fseqlem3  24021  mbfi1fseqlem4  24022  mbfi1fseqlem5  24023  mbfi1fseqlem6  24024  itg2gt0  24064  itg2cnlem2  24066  dgreq0  24558  dgrco  24568  elqaalem2  24612  aaliou3lem2  24635  aaliou3lem8  24637  aaliou3lem9  24642  leibpi  25222  log2tlbnd  25225  birthdaylem3  25233  amgm  25270  emcllem2  25276  harmonicbnd4  25290  lgamgulmlem1  25308  lgamgulmlem2  25309  lgamgulmlem3  25310  lgamgulmlem4  25311  lgamgulmlem5  25312  lgamgulmlem6  25313  lgamucov  25317  lgamcvg2  25334  wilthlem1  25347  ftalem5  25356  basellem1  25360  basellem2  25361  basellem3  25362  basellem4  25363  basellem5  25364  basellem6  25365  basellem8  25367  chtge0  25391  chtwordi  25435  vma1  25445  dvdsflf1o  25466  dvdsflsumcom  25467  fsumfldivdiaglem  25468  sgmmul  25479  chtublem  25489  fsumvma2  25492  logfac2  25495  chpchtsum  25497  chpub  25498  logfaclbnd  25500  logexprlim  25503  mersenne  25505  perfectlem2  25508  dchrelbas4  25521  bposlem1  25562  bposlem2  25563  bposlem3  25564  bposlem4  25565  bposlem5  25566  bposlem6  25567  bposlem7  25568  bposlem9  25570  lgslem1  25575  lgsval2lem  25585  lgsdirprm  25609  lgsdir  25610  lgsne0  25613  lgsqrlem2  25625  gausslemma2dlem0h  25641  gausslemma2dlem0i  25642  gausslemma2dlem1a  25643  gausslemma2dlem2  25645  gausslemma2dlem7  25651  gausslemma2d  25652  lgseisenlem1  25653  lgseisenlem2  25654  lgseisenlem3  25655  lgseisenlem4  25656  lgseisen  25657  lgsquadlem1  25658  lgsquadlem2  25659  lgsquadlem3  25660  2sqlem3  25698  2sqlem8  25704  2sqblem  25709  2sqmod  25714  chebbnd1lem1  25747  chebbnd1lem3  25749  chtppilimlem1  25751  rplogsumlem1  25762  rplogsumlem2  25763  dchrisum0lem1a  25764  rpvmasumlem  25765  dchrisumlema  25766  dchrisumlem1  25767  dchrisumlem2  25768  dchrisumlem3  25769  dchrvmasumiflem1  25779  dchrisum0flblem2  25787  dchrisum0re  25791  dchrisum0lem1b  25793  dchrisum0lem1  25794  dirith2  25806  selbergb  25827  selberg2lem  25828  logdivbnd  25834  selberg3lem2  25836  selberg4lem1  25838  pntrsumo1  25843  pntrsumbnd2  25845  pntrlog2bndlem1  25855  pntrlog2bndlem2  25856  pntrlog2bndlem3  25857  pntrlog2bndlem4  25858  pntrlog2bndlem5  25859  pntpbnd1a  25863  pntpbnd1  25864  pntibndlem2a  25868  pntibndlem2  25869  pntlemg  25876  pntlemh  25877  pntlemj  25881  pntlemf  25883  ostth2lem1  25896  padicabvf  25909  padicabvcxp  25910  ostth2lem2  25912  ostth2lem3  25913  ostth2lem4  25914  ostth2  25915  ostth3  25916  numclwwlk5  27945  numclwwlk7  27948  ubthlem2  28426  minvecolem4  28435  iundisjf  30105  ssnnssfz  30269  iundisjfi  30275  pmtrto1cl  30696  psgnfzto1stlem  30697  fzto1st1  30699  fzto1st  30700  psgnfzto1st  30702  smatrcl  30709  smattr  30712  smatbl  30713  smatbr  30714  1smat1  30717  submateqlem1  30720  submateqlem2  30721  submateq  30722  esumcst  30972  fiunelros  31084  oddpwdc  31263  eulerpartlems  31269  eulerpartlemgc  31271  fiblem  31308  dstfrvunirn  31384  dstfrvclim1  31387  ballotlemimin  31415  fsum2dsub  31532  reprinfz1  31547  hgt750lemd  31573  hgt750lemb  31581  hgt750leme  31583  tgoldbachgtde  31585  tgoldbachgt  31588  subfaclim  32026  subfacval3  32027  erdszelem7  32035  erdszelem8  32036  erdsze2lem2  32042  cvmliftlem2  32124  cvmliftlem6  32128  cvmliftlem7  32129  cvmliftlem8  32130  cvmliftlem9  32131  cvmliftlem10  32132  cvmliftlem13  32134  bcprod  32496  bccolsum  32497  faclimlem2  32502  faclim2  32506  nn0prpwlem  33197  knoppndvlem15  33391  knoppndvlem17  33393  knoppndvlem18  33394  knoppndvlem19  33395  knoppndvlem20  33396  knoppndvlem21  33397  poimirlem3  34342  poimirlem6  34345  poimirlem7  34346  poimirlem8  34347  poimirlem9  34348  poimirlem10  34349  poimirlem11  34350  poimirlem12  34351  poimirlem13  34352  poimirlem15  34354  poimirlem16  34355  poimirlem17  34356  poimirlem19  34358  poimirlem20  34359  poimirlem21  34360  poimirlem22  34361  poimirlem23  34362  poimirlem26  34365  poimirlem28  34367  opnmbllem0  34375  mblfinlem2  34377  incsequz  34471  nninfnub  34474  oexpreposd  38617  nn0expgcd  38622  rtprmirr  38632  fltltc  38686  fltnltalem  38687  fltnlta  38688  irrapxlem3  38823  irrapxlem4  38824  irrapxlem5  38825  pellexlem2  38829  pellexlem6  38833  pell14qrgt0  38858  pell14qrgapw  38875  pellfundgt1  38882  rmspecsqrtnq  38905  ltrmxnn0  38948  jm3.1lem1  39016  jm3.1lem3  39018  dgraa0p  39151  hashnzfz2  40075  rfcnnnub  40718  nnxrd  40724  fzisoeu  41002  fsumnncl  41289  sumnnodd  41348  limsup10exlem  41490  stoweidlem1  41723  stoweidlem3  41725  stoweidlem11  41733  stoweidlem17  41739  stoweidlem20  41742  stoweidlem25  41747  stoweidlem26  41748  stoweidlem34  41756  stoweidlem38  41760  stoweidlem42  41764  stoweidlem44  41766  stoweidlem51  41773  stoweidlem59  41781  stoweidlem60  41782  wallispi  41792  wallispi2  41795  stirlinglem3  41798  stirlinglem4  41799  stirlinglem8  41803  stirlinglem10  41805  stirlinglem12  41807  stirlinglem15  41810  dirkertrigeqlem2  41821  dirkertrigeqlem3  41822  dirkercncflem2  41826  fourierdlem11  41840  fourierdlem14  41843  fourierdlem15  41844  fourierdlem20  41849  fourierdlem31  41860  fourierdlem64  41892  fourierdlem93  41921  fourierdlem95  41923  fourierdlem103  41931  fourierdlem104  41932  fourierdlem112  41940  sqwvfourb  41951  etransclem3  41959  etransclem19  41975  etransclem23  41979  etransclem24  41980  etransclem25  41981  etransclem32  41988  etransclem35  41991  etransclem41  41997  etransclem48  42004  qndenserrnbllem  42016  hoiqssbllem1  42341  hoiqssbllem2  42342  ovolval5lem1  42371  ovolval5lem2  42372  iccpartlt  42962  iccpartgt  42965  odz2prm2pw  43099  fmtnoprmfac1lem  43100  2pwp1prm  43125  sfprmdvdsmersenne  43142  lighneallem2  43145  proththdlem  43152  perfectALTVlem2  43261  gbowge7  43302  ztprmneprm  43765  pgrple2abl  43785  logbpw2m1  44001  nnpw2pmod  44017  nnolog2flm1  44024  blennngt2o2  44026