Theorem nnre 12200

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 12197	. 2 ⊢ ℕ ⊆ ℝ
2	1	sseli 3945	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11074  ℕcn 12193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194

This theorem is referenced by:  nnrei  12202  nnmulcl  12217  nn2ge  12220  nnge1  12221  nngt1ne1  12222  nnle1eq1  12223  nngt0  12224  nnnlt1  12225  nnnle0  12226  nndivre  12234  nnrecgt0  12236  nnsub  12237  nnunb  12445  arch  12446  nnrecl  12447  bndndx  12448  0mnnnnn0  12481  nnnegz  12539  elnnz  12546  elz2  12554  nnz  12557  gtndiv  12618  prime  12622  btwnz  12644  indstr  12882  qre  12919  elpq  12941  elpqb  12942  rpnnen1lem2  12943  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  nnrp  12970  nnledivrp  13072  qbtwnre  13166  elfzo0le  13671  fzonmapblen  13676  fzo1fzo0n0  13683  ubmelfzo  13698  fzonn0p1p1  13712  ubmelm1fzo  13731  subfzo0  13757  adddivflid  13787  flltdivnn0lt  13802  quoremz  13824  quoremnn0ALT  13826  intfracq  13828  fldiv  13829  modmulnn  13858  m1modnnsub1  13889  addmodid  13891  modifeq2int  13905  modaddmodup  13906  modaddmodlo  13907  modfzo0difsn  13915  modsumfzodifsn  13916  addmodlteq  13918  nnlesq  14177  digit2  14208  digit1  14209  expnngt1  14213  facdiv  14259  facndiv  14260  faclbnd  14262  faclbnd3  14264  faclbnd4lem4  14268  faclbnd5  14270  bcval5  14290  seqcoll  14436  ccatval21sw  14557  cshwidxmod  14775  cshwidxm1  14779  repswcshw  14784  isercolllem1  15638  harmonic  15832  efaddlem  16066  rpnnen2lem9  16197  rpnnen2lem12  16200  sqrt2irr  16224  nndivdvds  16238  dvdsle  16287  fzm1ndvds  16299  nno  16359  nnoddm1d2  16363  divalg2  16382  divalgmod  16383  ndvdsadd  16387  modgcd  16509  gcdzeq  16529  nn0rppwr  16538  sqgcd  16539  nn0expgcd  16541  dvdssqlem  16543  lcmgcdlem  16583  lcmf  16610  coprmgcdb  16626  qredeq  16634  qredeu  16635  isprm3  16660  ge2nprmge4  16678  prmdvdsfz  16682  isprm5  16684  ncoprmlnprm  16705  divdenle  16726  phibndlem  16747  eulerthlem2  16759  hashgcdlem  16765  oddprm  16788  pythagtriplem10  16798  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem16  16808  pythagtriplem19  16811  pclem  16816  pc2dvds  16857  pcmpt  16870  fldivp1  16875  pcbc  16878  infpnlem1  16888  infpn2  16891  prmreclem1  16894  prmreclem3  16896  vdwlem3  16961  ram0  17000  prmgaplem4  17032  prmgaplem7  17035  cshwshashlem1  17073  cshwshashlem2  17074  setsstruct2  17151  mulgnegnn  19023  mulgmodid  19052  odmodnn0  19477  gexdvds  19521  sylow3lem6  19569  prmirredlem  21389  znidomb  21478  chfacfisf  22748  chfacfisfcpmat  22749  chfacffsupp  22750  chfacfscmul0  22752  chfacfpmmul0  22756  ovolunlem1a  25404  ovoliunlem2  25411  ovolicc2lem3  25427  ovolicc2lem4  25428  iundisj2  25457  dyadss  25502  volsup2  25513  volivth  25515  vitali  25521  ismbf3d  25562  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  itg2seq  25650  itg2gt0  25668  itg2cnlem1  25669  idomrootle  26085  plyeq0lem  26122  dgreq0  26178  dgrcolem2  26187  elqaalem2  26235  elqaalem3  26236  logtayllem  26575  leibpi  26859  birthdaylem3  26870  zetacvg  26932  eldmgm  26939  basellem1  26998  basellem2  26999  basellem3  27000  basellem6  27003  basellem9  27006  prmorcht  27095  dvdsflsumcom  27105  muinv  27110  vmalelog  27123  chtublem  27129  logfac2  27135  logfaclbnd  27140  pcbcctr  27194  bcmono  27195  bposlem1  27202  bposlem5  27206  bposlem6  27207  bpos  27211  lgsval4a  27237  gausslemma2dlem0c  27276  gausslemma2dlem0d  27277  gausslemma2dlem1a  27283  gausslemma2dlem2  27285  gausslemma2dlem3  27286  gausslemma2dlem5  27289  lgsquadlem1  27298  lgsquadlem2  27299  2lgslem1a1  27307  2sqreunnlem1  27367  2sqreunnltlem  27368  dchrisum0re  27431  dchrisum0lem1  27434  logdivbnd  27474  ostth2lem1  27536  ostth2lem3  27553  pthdlem2lem  29704  crctcshwlkn0lem1  29747  crctcshwlkn0lem3  29749  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshwlkn0lem6  29752  crctcshwlkn0lem7  29753  crctcshwlkn0  29758  clwlkclwwlkf1lem2  29941  clwwisshclwwslem  29950  clwwlkel  29982  clwwlkf  29983  clwwlkf1  29985  wwlksext2clwwlk  29993  wwlksubclwwlk  29994  eucrctshift  30179  eucrct2eupth  30181  numclwlk2lem2f  30313  nmounbseqi  30713  nmounbseqiALT  30714  nmobndseqi  30715  nmobndseqiALT  30716  ubthlem1  30806  minvecolem3  30812  lnconi  31969  iundisj2f  32526  nnmulge  32669  xrsmulgzz  32954  esumpmono  34076  eulerpartlemb  34366  fibp1  34399  subfaclim  35182  subfacval3  35183  snmlff  35323  fz0n  35725  bcprod  35732  nn0prpwlem  36317  nn0prpw  36318  nndivsub  36452  nndivlub  36453  knoppcnlem2  36489  knoppcnlem4  36491  knoppndvlem11  36517  knoppndvlem12  36518  knoppndvlem14  36520  poimirlem13  37634  poimirlem14  37635  poimirlem31  37652  poimirlem32  37653  mblfinlem2  37659  fzmul  37742  incsequz  37749  nnubfi  37751  nninfnub  37752  2ap1caineq  42140  sticksstones1  42141  unitscyglem5  42194  nnadddir  42265  nnmul1com  42266  sn-nnne0  42455  nn0addcom  42457  renegmulnnass  42460  nn0mulcom  42461  zmulcomlem  42462  fimgmcyc  42529  irrapxlem1  42817  irrapxlem2  42818  pellexlem1  42824  pellexlem5  42828  pellqrex  42874  monotoddzzfi  42938  jm2.24nn  42955  congabseq  42970  acongrep  42976  acongeq  42979  expdiophlem1  43017  idomodle  43187  relexpmulnn  43705  prmunb2  44307  hashnzfzclim  44318  fmuldfeq  45588  sumnnodd  45635  stoweidlem14  46019  stoweidlem17  46022  stoweidlem20  46025  stoweidlem49  46054  stoweidlem60  46065  wallispilem3  46072  wallispilem4  46073  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem1  46079  stirlinglem3  46081  stirlinglem4  46082  stirlinglem6  46084  stirlinglem7  46085  stirlinglem10  46088  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  stirlingr  46095  dirker2re  46097  dirkerval2  46099  dirkerre  46100  dirkertrigeqlem1  46103  fourierdlem66  46177  fourierdlem73  46184  fourierdlem83  46194  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fouriersw  46236  etransclem24  46263  sge0rpcpnf  46426  hoicvr  46553  hoicvrrex  46561  vonioolem2  46686  vonicclem2  46689  fsupdm  46847  finfdm  46851  smfinfdmmbllem  46853  subsubelfzo0  47331  ceilhalfelfzo1  47335  2tceilhalfelfzo1  47337  ceilhalfnn  47341  addmodne  47349  submodlt  47355  modn0mul  47362  m1modmmod  47363  difmodm1lt  47364  modlt0b  47368  fmtnodvds  47549  2pwp1prm  47594  lighneallem2  47611  nn0oALTV  47701  nneven  47703  nnsum4primes4  47794  nnsum4primesprm  47796  nnsum4primesgbe  47798  nnsum4primesle9  47800  bgoldbachlt  47818  tgoldbach  47822  gpgusgralem  48051  gpgedgvtx0  48056  gpg3kgrtriexlem1  48078  gpg3kgrtriexlem2  48079  gpg3kgrtriexlem3  48080  gpg3kgrtriexlem4  48081  gpg3kgrtriexlem6  48083  altgsumbcALT  48345  nnlog2ge0lt1  48559  logbpw2m1  48560  blennn  48568  blennnelnn  48569  nnpw2pmod  48576  nnolog2flm1  48583  digvalnn0  48592  dignn0fr  48594  dignn0ldlem  48595  dignnld  48596  dig2nn1st  48598