MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnred Structured version   Visualization version   GIF version

Theorem nnred 11073
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
StepHypRef Expression
1 nnssre 11062 . 2 ℕ ⊆ ℝ
2 nnred.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3634 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cr 9973  cn 11058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-nn 11059
This theorem is referenced by:  uzwo3  11821  modmulnn  12728  bernneq3  13032  expmulnbnd  13036  facwordi  13116  faclbnd  13117  faclbnd2  13118  faclbnd3  13119  faclbnd5  13125  faclbnd6  13126  facubnd  13127  facavg  13128  bcp1nk  13144  hashf1  13279  swrds2  13731  isercolllem1  14439  isercoll  14442  o1fsum  14589  climcndslem1  14625  climcndslem2  14626  climcnds  14627  eftabs  14850  efcllem  14852  ege2le3  14864  efcj  14866  eftlub  14883  eflegeo  14895  eirrlem  14976  fzm1ndvds  15091  nno  15145  nnoddm1d2  15149  bitsfzolem  15203  bitsfzo  15204  bitsinv1lem  15210  sadcaddlem  15226  smueqlem  15259  bezoutlem3  15305  bezoutlem4  15306  sqgcd  15325  lcmgcdlem  15366  lcmf  15393  prmind2  15445  coprm  15470  prmfac1  15478  prmndvdsfaclt  15482  divdenle  15504  qnumgt0  15505  zsqrtelqelz  15513  hashdvds  15527  eulerthlem2  15534  odzdvds  15547  modprm1div  15549  vfermltl  15553  modprm0  15557  pythagtriplem11  15577  pythagtriplem13  15579  pythagtriplem19  15585  pclem  15590  pcpre1  15594  pcidlem  15623  dvdsprmpweqle  15637  pcadd  15640  pcmpt  15643  pcmpt2  15644  pcfaclem  15649  pcfac  15650  qexpz  15652  pockthlem  15656  pockthg  15657  prmreclem1  15667  prmreclem3  15669  prmreclem4  15670  prmreclem5  15671  1arithlem4  15677  1arith  15678  4sqlem5  15693  4sqlem6  15694  4sqlem10  15698  mul4sqlem  15704  4sqlem11  15706  4sqlem12  15707  4sqlem13  15708  4sqlem14  15709  4sqlem15  15710  4sqlem16  15711  4sqlem17  15712  vdwlem1  15732  vdwlem3  15734  vdwlem6  15737  vdwlem9  15740  vdwlem10  15741  vdwlem12  15743  vdwnnlem3  15748  ramub1lem1  15777  prmolefac  15797  prmgaplem4  15805  prmgaplem5  15806  prmgaplem6  15807  prmgaplem8  15809  2expltfac  15846  cshwshashnsame  15857  setsstruct2  15943  psgnunilem4  17963  mndodconglem  18006  oddvds  18012  sylow1lem1  18059  sylow1lem5  18063  fislw  18086  efgredlem  18206  gexexlem  18301  zringlpirlem3  19882  prmirredlem  19889  fvmptnn04if  20702  fvmptnn04ifb  20704  fvmptnn04ifc  20705  fvmptnn04ifd  20706  chfacfisf  20707  chfacfisfcpmat  20708  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  lebnumii  22812  lmnn  23107  ovolunlem1a  23310  ovoliunlem1  23316  ovolicc2lem3  23333  ovolicc2lem4  23334  iundisj  23362  voliunlem1  23364  uniioombllem3  23399  dyadf  23405  dyadovol  23407  dyaddisjlem  23409  dyadmaxlem  23411  opnmbllem  23415  vitalilem4  23425  mbfi1fseqlem1  23527  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  itg2gt0  23572  itg2cnlem2  23574  dgreq0  24066  dgrco  24076  elqaalem2  24120  aaliou3lem2  24143  aaliou3lem8  24145  aaliou3lem9  24150  leibpi  24714  log2tlbnd  24717  birthdaylem3  24725  amgm  24762  emcllem2  24768  harmonicbnd4  24782  lgamgulmlem1  24800  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem4  24803  lgamgulmlem5  24804  lgamgulmlem6  24805  lgamucov  24809  lgamcvg2  24826  wilthlem1  24839  ftalem5  24848  basellem1  24852  basellem2  24853  basellem3  24854  basellem4  24855  basellem5  24856  basellem6  24857  basellem8  24859  chtge0  24883  chtwordi  24927  vma1  24937  dvdsflf1o  24958  dvdsflsumcom  24959  fsumfldivdiaglem  24960  sgmmul  24971  chtublem  24981  fsumvma2  24984  logfac2  24987  chpchtsum  24989  chpub  24990  logfaclbnd  24992  logexprlim  24995  mersenne  24997  perfectlem2  25000  dchrelbas4  25013  bposlem1  25054  bposlem2  25055  bposlem3  25056  bposlem4  25057  bposlem5  25058  bposlem6  25059  bposlem7  25060  bposlem9  25062  lgslem1  25067  lgsval2lem  25077  lgsdirprm  25101  lgsdir  25102  lgsne0  25105  lgsqrlem2  25117  gausslemma2dlem0h  25133  gausslemma2dlem0i  25134  gausslemma2dlem1a  25135  gausslemma2dlem2  25137  gausslemma2dlem7  25143  gausslemma2d  25144  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgseisenlem4  25148  lgseisen  25149  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  m1lgs  25158  2sqlem3  25190  2sqlem8  25196  2sqblem  25201  chebbnd1lem1  25203  chebbnd1lem3  25205  chtppilimlem1  25207  rplogsumlem1  25218  rplogsumlem2  25219  dchrisum0lem1a  25220  rpvmasumlem  25221  dchrisumlema  25222  dchrisumlem1  25223  dchrisumlem2  25224  dchrisumlem3  25225  dchrvmasumiflem1  25235  dchrisum0flblem2  25243  dchrisum0re  25247  dchrisum0lem1b  25249  dchrisum0lem1  25250  dirith2  25262  selbergb  25283  selberg2lem  25284  logdivbnd  25290  selberg3lem2  25292  selberg4lem1  25294  pntrsumo1  25299  pntrsumbnd2  25301  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntpbnd1a  25319  pntpbnd1  25320  pntibndlem2a  25324  pntibndlem2  25325  pntlemg  25332  pntlemh  25333  pntlemj  25337  pntlemf  25339  ostth2lem1  25352  padicabvf  25365  padicabvcxp  25366  ostth2lem2  25368  ostth2lem3  25369  ostth2lem4  25370  ostth2  25371  ostth3  25372  clwlksfclwwlk  27049  numclwwlk5  27375  numclwwlk7  27378  ubthlem2  27855  minvecolem4  27864  iundisjf  29528  ssnnssfz  29677  iundisjfi  29683  2sqmod  29776  pmtrto1cl  29977  psgnfzto1stlem  29978  fzto1st1  29980  fzto1st  29981  psgnfzto1st  29983  smatrcl  29990  smattr  29993  smatbl  29994  smatbr  29995  1smat1  29998  submateqlem1  30001  submateqlem2  30002  submateq  30003  esumcst  30253  fiunelros  30365  oddpwdc  30544  eulerpartlems  30550  eulerpartlemgc  30552  fiblem  30588  dstfrvunirn  30664  dstfrvclim1  30667  ballotlemimin  30695  fsum2dsub  30813  reprinfz1  30828  hgt750lemd  30854  hgt750lemb  30862  hgt750leme  30864  tgoldbachgtde  30866  tgoldbachgt  30869  subfaclim  31296  subfacval3  31297  erdszelem7  31305  erdszelem8  31306  erdsze2lem2  31312  cvmliftlem2  31394  cvmliftlem6  31398  cvmliftlem7  31399  cvmliftlem8  31400  cvmliftlem9  31401  cvmliftlem10  31402  cvmliftlem13  31404  bcprod  31750  bccolsum  31751  faclimlem2  31756  faclim2  31760  nn0prpwlem  32442  knoppndvlem15  32642  knoppndvlem17  32644  knoppndvlem18  32645  knoppndvlem19  32646  knoppndvlem20  32647  knoppndvlem21  32648  poimirlem3  33542  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem26  33565  poimirlem28  33567  opnmbllem0  33575  mblfinlem2  33577  incsequz  33674  nninfnub  33677  irrapxlem3  37705  irrapxlem4  37706  irrapxlem5  37707  pellexlem2  37711  pellexlem6  37715  pell14qrgt0  37740  pell14qrgapw  37757  pellfundgt1  37764  rmspecsqrtnq  37787  rmspecsqrtnqOLD  37788  ltrmxnn0  37833  jm3.1lem1  37901  jm3.1lem3  37903  dgraa0p  38036  hashnzfz2  38837  rfcnnnub  39509  nnxrd  39515  fzisoeu  39828  fsumnncl  40121  sumnnodd  40180  limsup10exlem  40322  stoweidlem1  40536  stoweidlem3  40538  stoweidlem11  40546  stoweidlem17  40552  stoweidlem20  40555  stoweidlem25  40560  stoweidlem26  40561  stoweidlem34  40569  stoweidlem38  40573  stoweidlem42  40577  stoweidlem44  40579  stoweidlem51  40586  stoweidlem59  40594  stoweidlem60  40595  wallispi  40605  wallispi2  40608  stirlinglem3  40611  stirlinglem4  40612  stirlinglem8  40616  stirlinglem10  40618  stirlinglem12  40620  stirlinglem15  40623  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkercncflem2  40639  fourierdlem11  40653  fourierdlem14  40656  fourierdlem15  40657  fourierdlem20  40662  fourierdlem31  40673  fourierdlem64  40705  fourierdlem93  40734  fourierdlem95  40736  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  sqwvfourb  40764  etransclem3  40772  etransclem19  40788  etransclem23  40792  etransclem24  40793  etransclem25  40794  etransclem32  40801  etransclem35  40804  etransclem41  40810  etransclem48  40817  qndenserrnbllem  40832  hoiqssbllem1  41157  hoiqssbllem2  41158  ovolval5lem1  41187  ovolval5lem2  41188  iccpartlt  41685  iccpartgt  41688  odz2prm2pw  41800  fmtnoprmfac1lem  41801  2pwp1prm  41828  sfprmdvdsmersenne  41845  lighneallem2  41848  proththdlem  41855  perfectALTVlem2  41956  gbowge7  41976  ztprmneprm  42450  pgrple2abl  42471  logbpw2m1  42686  nnpw2pmod  42702  nnolog2flm1  42709  blennngt2o2  42711
  Copyright terms: Public domain W3C validator