Theorem nnre 12235

Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)

Assertion

Ref	Expression
nnre	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Proof of Theorem nnre

Step	Hyp	Ref	Expression
1		nnssre 12232	. 2 ⊢ ℕ ⊆ ℝ
2	1	sseli 3933	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11094  ℕcn 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12229

This theorem is referenced by:  nnrei  12237  nnmulcl  12252  nn2ge  12258  nnge1  12259  nngt1ne1  12260  nnle1eq1  12261  nngt0  12262  nnnlt1  12263  nnnle0  12264  nndivre  12272  nnrecgt0  12274  nnsub  12275  nnadddir  12287  nnmul1com  12288  nnunb  12495  arch  12496  nnrecl  12497  bndndx  12498  0mnnnnn0  12531  nnnegz  12589  elnnz  12596  elz2  12604  nnz  12607  gtndiv  12668  prime  12672  btwnz  12694  indstr  12935  qre  12972  elpq  12994  elpqb  12995  rpnnen1lem2  12996  rpnnen1lem1  12997  rpnnen1lem3  12998  rpnnen1lem5  13000  nnrp  13023  nnledivrp  13125  qbtwnre  13220  elfzo0le  13728  fzonmapblen  13733  fzo1fzo0n0  13740  ubmelfzo  13755  fzonn0p1p1  13769  ubmelm1fzo  13788  subfzo0  13817  adddivflid  13847  flltdivnn0lt  13862  quoremz  13884  quoremnn0ALT  13886  intfracq  13888  fldiv  13889  modmulnn  13918  m1modnnsub1  13949  addmodid  13951  modifeq2int  13965  modaddmodup  13966  modaddmodlo  13967  modfzo0difsn  13975  modsumfzodifsn  13976  addmodlteq  13978  nnlesq  14237  digit2  14268  digit1  14269  expnngt1  14273  facdiv  14319  facndiv  14320  faclbnd  14322  faclbnd3  14324  faclbnd4lem4  14328  faclbnd5  14330  bcval5  14350  seqcoll  14497  ccatval21sw  14619  cshwidxmod  14836  cshwidxm1  14840  repswcshw  14845  isercolllem1  15712  harmonic  15909  efaddlem  16142  rpnnen2lem9  16273  rpnnen2lem12  16276  sqrt2irr  16300  nndivdvds  16314  dvdsle  16363  fzm1ndvds  16375  nno  16435  nnoddm1d2  16439  divalg2  16458  divalgmod  16459  ndvdsadd  16463  modgcd  16585  gcdzeq  16605  nn0rppwr  16614  sqgcd  16615  nn0expgcd  16617  dvdssqlem  16619  lcmgcdlem  16659  lcmf  16686  coprmgcdb  16702  qredeq  16710  qredeu  16711  isprm3  16736  ge2nprmge4  16755  prmdvdsfz  16759  isprm5  16761  ncoprmlnprm  16782  divdenle  16803  phibndlem  16824  eulerthlem2  16836  hashgcdlem  16842  oddprm  16865  pythagtriplem10  16875  pythagtriplem12  16881  pythagtriplem14  16883  pythagtriplem16  16885  pythagtriplem19  16888  pclem  16893  pc2dvds  16934  pcmpt  16947  fldivp1  16952  pcbc  16955  infpnlem1  16965  infpn2  16968  prmreclem1  16971  prmreclem3  16973  vdwlem3  17038  ram0  17077  prmgaplem4  17109  prmgaplem7  17112  cshwshashlem1  17150  cshwshashlem2  17151  setsstruct2  17229  mulgnegnn  19145  mulgmodid  19174  odmodnn0  19605  gexdvds  19649  sylow3lem6  19697  prmirredlem  21622  znidomb  21711  chfacfisf  23011  chfacfisfcpmat  23012  chfacffsupp  23013  chfacfscmul0  23015  chfacfpmmul0  23019  ovolunlem1a  25655  ovoliunlem2  25662  ovolicc2lem3  25678  ovolicc2lem4  25679  iundisj2  25708  dyadss  25753  volsup2  25764  volivth  25766  vitali  25772  ismbf3d  25813  mbfi1fseqlem3  25876  mbfi1fseqlem4  25877  mbfi1fseqlem5  25878  itg2seq  25901  itg2gt0  25919  itg2cnlem1  25920  idomrootle  26330  plyeq0lem  26367  dgreq0  26422  dgrcolem2  26431  elqaalem2  26481  elqaalem3  26482  logtayllem  26824  leibpi  27107  birthdaylem3  27118  zetacvg  27179  eldmgm  27186  basellem1  27245  basellem2  27246  basellem3  27247  basellem6  27250  basellem9  27253  prmorcht  27342  dvdsflsumcom  27352  muinv  27357  vmalelog  27369  chtublem  27375  logfac2  27381  logfaclbnd  27386  pcbcctr  27440  bcmono  27441  bposlem1  27448  bposlem5  27452  bposlem6  27453  bpos  27457  lgsval4a  27483  gausslemma2dlem0c  27522  gausslemma2dlem0d  27523  gausslemma2dlem1a  27529  gausslemma2dlem2  27531  gausslemma2dlem3  27532  gausslemma2dlem5  27535  lgsquadlem1  27544  lgsquadlem2  27545  2lgslem1a1  27553  2sqreunnlem1  27613  2sqreunnltlem  27614  dchrisum0re  27677  dchrisum0lem1  27680  logdivbnd  27720  ostth2lem1  27782  ostth2lem3  27799  pthdlem2lem  30116  crctcshwlkn0lem1  30159  crctcshwlkn0lem3  30161  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  crctcshwlkn0lem6  30164  crctcshwlkn0lem7  30165  crctcshwlkn0  30170  clwlkclwwlkf1lem2  30356  clwwisshclwwslem  30365  clwwlkel  30397  clwwlkf  30398  clwwlkf1  30400  wwlksext2clwwlk  30408  wwlksubclwwlk  30409  eucrctshift  30594  eucrct2eupth  30596  numclwlk2lem2f  30728  nmounbseqi  31129  nmounbseqiALT  31130  nmobndseqi  31131  nmobndseqiALT  31132  ubthlem1  31222  minvecolem3  31228  lnconi  32385  iundisj2f  32935  nnmulge  33084  xrsmulgzz  33329  esumpmono  34469  eulerpartlemb  34758  fibp1  34791  subfaclim  35680  subfacval3  35681  snmlff  35821  fz0n  36223  bcprod  36230  nn0prpwlem  36853  nn0prpw  36854  nndivsub  36988  nndivlub  36989  knoppcnlem2  37103  knoppcnlem4  37105  knoppndvlem11  37131  knoppndvlem12  37132  knoppndvlem14  37134  poimirlem13  38304  poimirlem14  38305  poimirlem31  38322  poimirlem32  38323  mblfinlem2  38329  fzmul  38412  incsequz  38419  nnubfi  38421  nninfnub  38422  2ap1caineq  42932  sticksstones1  42933  unitscyglem5  42986  sn-nnne0  43254  nn0addcom  43256  renegmulnnass  43259  nn0mulcom  43260  zmulcomlem  43261  fimgmcyc  43322  irrapxlem1  43569  irrapxlem2  43570  pellexlem1  43576  pellexlem5  43580  pellqrex  43626  monotoddzzfi  43689  jm2.24nn  43706  congabseq  43721  acongrep  43727  acongeq  43730  expdiophlem1  43768  idomodle  43938  relexpmulnn  44455  prmunb2  45041  hashnzfzclim  45052  fmuldfeq  46319  sumnnodd  46366  stoweidlem14  46748  stoweidlem17  46751  stoweidlem20  46754  stoweidlem49  46783  stoweidlem60  46794  wallispilem3  46801  wallispilem4  46802  wallispilem5  46803  wallispi  46804  wallispi2lem1  46805  wallispi2lem2  46806  stirlinglem1  46808  stirlinglem3  46810  stirlinglem4  46811  stirlinglem6  46813  stirlinglem7  46814  stirlinglem10  46817  stirlinglem11  46818  stirlinglem12  46819  stirlinglem13  46820  stirlingr  46824  dirker2re  46826  dirkerval2  46828  dirkerre  46829  dirkertrigeqlem1  46832  fourierdlem66  46906  fourierdlem73  46913  fourierdlem83  46923  fourierdlem87  46927  fourierdlem103  46943  fourierdlem104  46944  fourierdlem111  46951  fouriersw  46965  etransclem24  46992  sge0rpcpnf  47155  hoicvr  47282  hoicvrrex  47290  vonioolem2  47415  vonicclem2  47418  fsupdm  47576  finfdm  47580  smfinfdmmbllem  47582  subsubelfzo0  48084  ceilhalfelfzo1  48091  2tceilhalfelfzo1  48093  ceilhalfnn  48097  addmodne  48107  submodlt  48113  modn0mul  48120  m1modmmod  48121  difmodm1lt  48122  modlt0b  48126  fmtnodvds  48316  2pwp1prm  48361  lighneallem2  48378  nn0oALTV  48481  nneven  48483  nnsum4primes4  48574  nnsum4primesprm  48576  nnsum4primesgbe  48578  nnsum4primesle9  48580  bgoldbachlt  48598  tgoldbach  48602  gpgusgralem  48841  gpgedgvtx0  48846  gpg3kgrtriexlem1  48868  gpg3kgrtriexlem2  48869  gpg3kgrtriexlem3  48870  gpg3kgrtriexlem4  48871  gpg3kgrtriexlem6  48873  altgsumbcALT  49153  nnlog2ge0lt1  49366  logbpw2m1  49367  blennn  49375  blennnelnn  49376  nnpw2pmod  49383  nnolog2flm1  49390  digvalnn0  49399  dignn0fr  49401  dignn0ldlem  49402  dignnld  49403  dig2nn1st  49405