MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnre Structured version   Unicode version

Theorem nnre 10538
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
Assertion
Ref Expression
nnre  |-  ( A  e.  NN  ->  A  e.  RR )

Proof of Theorem nnre
StepHypRef Expression
1 nnssre 10535 . 2  |-  NN  C_  RR
21sseli 3485 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   RRcr 9480   NNcn 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-om 6674  df-recs 7034  df-rdg 7068  df-nn 10532
This theorem is referenced by:  nnrei  10540  nn2ge  10556  nnge1  10557  nngt1ne1  10558  nnle1eq1  10559  nngt0  10560  nnnlt1  10561  nnnle0  10562  nndivre  10567  nnrecgt0  10569  nnsub  10570  nnunb  10787  arch  10788  nnrecl  10789  bndndx  10790  0mnnnnn0  10824  nnnegz  10863  elnnz  10870  elz2  10877  gtndiv  10936  prime  10939  btwnz  10962  indstr  11151  qre  11188  rpnnen1lem1  11209  rpnnen1lem2  11210  rpnnen1lem3  11211  rpnnen1lem5  11213  nnrp  11230  qbtwnre  11401  fzo1fzo0n0  11841  elfzo0le  11843  fzonmapblen  11845  ubmelfzo  11862  fzonn0p1p1  11875  elfzom1p1elfzo  11876  ubmelm1fzo  11889  flltdivnn0lt  11947  quoremz  11964  quoremnn0ALT  11966  intfracq  11968  fldiv  11969  modmulnn  11996  modidmul0OLD  12005  addmodid  12021  modifeq2int  12034  modaddmodup  12035  modaddmodlo  12036  nnlesq  12256  digit2  12284  digit1  12285  facdiv  12350  facndiv  12351  faclbnd  12353  faclbnd3  12355  faclbnd4lem4  12359  faclbnd5  12361  bcval5  12381  seqcoll  12499  cshwidxmod  12768  cshwidxm1  12771  repswcshw  12774  isercolllem1  13572  harmonic  13755  efaddlem  13913  rpnnen2lem9  14043  rpnnen2  14046  sqrt2irr  14069  nndivdvds  14079  dvdsle  14118  dvdseq  14120  fzm1ndvds  14125  divalg2  14150  divalgmod  14151  ndvdsadd  14153  modgcd  14261  gcdmultiple  14275  gcdmultiplez  14276  gcdeq  14277  sqgcd  14283  dvdssqlem  14284  isprm3  14313  qredeq  14334  qredeu  14335  isprm5  14340  divdenle  14369  phibndlem  14387  eulerthlem2  14399  oddprm  14426  pythagtriplem10  14431  pythagtriplem12  14437  pythagtriplem14  14439  pythagtriplem16  14441  pythagtriplem19  14444  pclem  14449  pc2dvds  14489  pcmpt  14498  fldivp1  14503  pcbc  14506  infpnlem1  14515  infpn2  14518  prmreclem1  14521  prmreclem3  14523  vdwlem3  14588  ram0  14627  cshwshashlem1  14667  cshwshashlem2  14668  mulgnegnn  16354  odmodnn0  16766  gexdvds  16806  sylow3lem6  16854  prmirredlem  18708  znidomb  18776  chfacfisf  19525  chfacfisfcpmat  19526  chfacffsupp  19527  chfacfscmul0  19529  chfacfpmmul0  19533  ovolunlem1a  22076  ovoliunlem2  22083  ovolicc2lem3  22099  ovolicc2lem4  22100  iundisj2  22128  dyadss  22172  volsup2  22183  volivth  22185  vitali  22191  ismbf3d  22230  mbfi1fseqlem3  22293  mbfi1fseqlem4  22294  mbfi1fseqlem5  22295  itg2seq  22318  itg2gt0  22336  itg2cnlem1  22337  plyeq0lem  22776  dgreq0  22831  dgrcolem2  22840  elqaalem2  22885  elqaalem3  22886  logtayllem  23211  leibpi  23473  birthdaylem3  23484  basellem1  23555  basellem2  23556  basellem3  23557  basellem6  23560  basellem9  23563  prmorcht  23653  dvdsdivcl  23658  dvdsflsumcom  23665  muinv  23670  vmalelog  23681  chtublem  23687  logfac2  23693  logfaclbnd  23698  pcbcctr  23752  bcmono  23753  bposlem1  23760  bposlem5  23764  bposlem6  23765  bpos  23769  lgsval4a  23794  lgsquadlem1  23830  lgsquadlem2  23831  dchrisum0re  23899  dchrisum0lem1  23902  logdivbnd  23942  ostth2lem1  24004  ostth2lem3  24021  clwwlkel  24998  clwwlkf  24999  clwwlkf1  25001  wwlkext2clwwlk  25008  wwlksubclwwlk  25009  clwwisshclwwlem  25011  numclwlk2lem2f  25308  gxnn0neg  25466  gxmodid  25482  nmounbseqi  25893  nmounbseqiALT  25894  nmobndseqi  25895  nmobndseqiALT  25896  ubthlem1  25987  minvecolem3  25993  lnconi  27153  iundisj2f  27663  xrsmulgzz  27903  esumpmono  28311  eulerpartlemb  28574  fibp1  28607  zetacvg  28824  eldmgm  28831  subfaclim  28899  subfacval3  28900  snmlff  29041  fz0n  29354  nndivsub  30153  nndivlub  30154  mblfinlem2  30295  nn0prpwlem  30383  nn0prpw  30384  fzmul  30476  incsequz  30484  nnubfi  30486  nninfnub  30487  irrapxlem1  31000  irrapxlem2  31001  pellexlem1  31007  pellexlem5  31011  pellqrex  31057  monotoddzzfi  31120  jm2.24nn  31139  congabseq  31154  acongrep  31160  acongeq  31163  expdiophlem1  31205  idomrootle  31396  idomodle  31397  hashgcdlem  31401  prmunb2  31435  lcmgcdlem  31456  hashnzfzclim  31471  fmuldfeq  31819  sumnnodd  31878  stoweidlem14  32038  stoweidlem17  32041  stoweidlem20  32044  stoweidlem49  32073  stoweidlem60  32084  wallispilem3  32091  wallispilem4  32092  wallispilem5  32093  wallispi  32094  wallispi2lem1  32095  wallispi2lem2  32096  stirlinglem1  32098  stirlinglem3  32100  stirlinglem4  32101  stirlinglem6  32103  stirlinglem7  32104  stirlinglem10  32107  stirlinglem11  32108  stirlinglem12  32109  stirlinglem13  32110  stirlingr  32114  dirker2re  32116  dirkerval2  32118  dirkerre  32119  dirkertrigeqlem1  32122  fourierdlem66  32197  fourierdlem73  32204  fourierdlem83  32214  fourierdlem87  32218  fourierdlem103  32234  fourierdlem104  32235  fourierdlem111  32242  fouriersw  32256  etransclem24  32283  gcdzeq  32578  nn0oALTV  32610  subsubelfzo0  32731  altgsumbcALT  33215  modn0mul  33406  m1modmmod  33407  difmodm1lt  33408  nno  33411  nnlog2ge0lt1  33460  logbpw2m1  33461  blennn  33469  blennnelnn  33470  nnpw2pmod  33477  nnolog2flm1  33484  digvalnn0  33493  dignn0fr  33495  dignn0ldlem  33496  dignnld  33497  dig2nn1st  33499  relexpmulnn  38248
  Copyright terms: Public domain W3C validator