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

Theorem nnre 10321
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 10318 . 2  |-  NN  C_  RR
21sseli 3347 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   RRcr 9273   NNcn 10314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rrecex 9346  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-om 6472  df-recs 6824  df-rdg 6858  df-nn 10315
This theorem is referenced by:  nnrei  10323  nn2ge  10339  nnge1  10340  nngt1ne1  10341  nnle1eq1  10342  nngt0  10343  nnnlt1  10344  nndivre  10349  nnrecgt0  10351  nnsub  10352  nnunb  10567  arch  10568  nnrecl  10569  bndndx  10570  0mnnnnn0  10604  nnnegz  10641  elnnz  10648  elz2  10655  gtndiv  10711  prime  10714  btwnz  10736  indstr  10915  qre  10950  rpnnen1lem1  10971  rpnnen1lem2  10972  rpnnen1lem3  10973  rpnnen1lem5  10975  nnrp  10992  qbtwnre  11161  fzo1fzo0n0  11580  elfzo0le  11582  fzonmapblen  11584  ubmelfzo  11595  ubmelm1fzo  11615  flltdivnn0lt  11669  quoremz  11686  quoremnn0ALT  11688  intfracq  11690  fldiv  11691  modmulnn  11717  modidmul0  11726  addmodid  11740  modifeq2int  11753  modaddmodup  11754  modaddmodlo  11755  nnlesq  11961  digit2  11989  digit1  11990  facdiv  12055  facndiv  12056  faclbnd  12058  faclbnd3  12060  faclbnd4lem4  12064  faclbnd5  12066  bcval5  12086  seqcoll  12208  lswcl  12262  lswccatn0lsw  12279  swrdn0  12316  cshwidxmod  12432  cshwidxm1  12435  repswcshw  12438  isercolllem1  13134  harmonic  13313  efaddlem  13370  rpnnen2lem9  13497  rpnnen2  13500  sqr2irr  13523  nndivdvds  13533  dvdsle  13570  dvdseq  13572  fzm1ndvds  13577  divalg2  13601  divalgmod  13602  ndvdsadd  13604  modgcd  13712  gcdmultiple  13726  gcdmultiplez  13727  gcdeq  13728  sqgcd  13734  dvdssqlem  13735  isprm3  13764  qredeq  13784  qredeu  13785  isprm5  13790  divdenle  13819  phibndlem  13837  eulerthlem2  13849  oddprm  13874  pythagtriplem10  13879  pythagtriplem12  13885  pythagtriplem14  13887  pythagtriplem16  13889  pythagtriplem19  13892  pclem  13897  pc2dvds  13937  pcmpt  13946  fldivp1  13951  pcbc  13954  infpnlem1  13963  infpn2  13966  prmreclem1  13969  prmreclem3  13971  vdwlem3  14036  ram0  14075  cshwshashlem1  14114  cshwshashlem2  14115  mulgnegnn  15628  odmodnn0  16034  gexdvds  16074  sylow3lem6  16122  prmirredlem  17897  prmirredlemOLD  17900  znidomb  17974  ovolunlem1a  20959  ovoliunlem2  20966  ovolicc2lem3  20982  ovolicc2lem4  20983  iundisj2  21010  dyadss  21054  volsup2  21065  volivth  21067  vitali  21073  ismbf3d  21112  mbfi1fseqlem3  21175  mbfi1fseqlem4  21176  mbfi1fseqlem5  21177  itg2seq  21200  itg2gt0  21218  itg2cnlem1  21219  plyeq0lem  21658  dgreq0  21712  dgrcolem2  21721  elqaalem2  21766  elqaalem3  21767  logtayllem  22084  leibpi  22317  birthdaylem3  22327  basellem1  22398  basellem2  22399  basellem3  22400  basellem6  22403  basellem9  22406  prmorcht  22496  dvdsdivcl  22501  dvdsflsumcom  22508  muinv  22513  vmalelog  22524  chtublem  22530  logfac2  22536  logfaclbnd  22541  pcbcctr  22595  bcmono  22596  bposlem1  22603  bposlem5  22607  bposlem6  22608  bpos  22612  lgsval4a  22637  lgsquadlem1  22673  lgsquadlem2  22674  dchrisum0re  22742  dchrisum0lem1  22745  logdivbnd  22785  ostth2lem1  22847  ostth2lem3  22864  gxnn0neg  23718  gxmodid  23734  nmounbseqi  24145  nmounbseqiOLD  24146  nmobndseqi  24147  nmobndseqiOLD  24148  ubthlem1  24239  minvecolem3  24245  lnconi  25405  iundisj2f  25900  esumpmono  26497  eulerpartlemb  26720  fibp1  26753  zetacvg  26970  eldmgm  26977  subfaclim  27045  subfacval3  27046  snmlff  27187  fz0n  27358  nndivsub  28273  nndivlub  28274  mblfinlem2  28400  nn0prpwlem  28488  nn0prpw  28489  fzmul  28607  incsequz  28615  nnubfi  28617  nninfnub  28618  irrapxlem1  29134  irrapxlem2  29135  pellexlem1  29141  pellexlem5  29145  pellqrex  29191  monotoddzzfi  29254  jm2.24nn  29273  congabseq  29288  acongrep  29294  acongeq  29297  expdiophlem1  29341  idomrootle  29531  idomodle  29532  hashgcdlem  29536  fmuldfeq  29735  stoweidlem14  29780  stoweidlem17  29783  stoweidlem20  29786  stoweidlem49  29815  stoweidlem60  29826  wallispilem3  29833  wallispilem4  29834  wallispilem5  29835  wallispi  29836  wallispi2lem1  29837  wallispi2lem2  29838  stirlinglem1  29840  stirlinglem3  29842  stirlinglem4  29843  stirlinglem6  29845  stirlinglem7  29846  stirlinglem10  29849  stirlinglem11  29850  stirlinglem12  29851  stirlinglem13  29852  stirlingr  29856  subsubelfzo0  30181  elfzom1p1elfzo  30186  fzonn0p1p1  30187  clwwlkel  30426  clwwlkf  30427  clwwlkf1  30429  wwlkext2clwwlk  30436  wwlksubclwwlk  30437  clwwisshclwwlem  30441  numclwlk2lem2f  30667  altgsumbcALT  30719
  Copyright terms: Public domain W3C validator