Theorem nnre 12193

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  ℕcn 12186

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187

This theorem is referenced by:  nnrei  12195  nnmulcl  12210  nn2ge  12213  nnge1  12214  nngt1ne1  12215  nnle1eq1  12216  nngt0  12217  nnnlt1  12218  nnnle0  12219  nndivre  12227  nnrecgt0  12229  nnsub  12230  nnunb  12438  arch  12439  nnrecl  12440  bndndx  12441  0mnnnnn0  12474  nnnegz  12532  elnnz  12539  elz2  12547  nnz  12550  gtndiv  12611  prime  12615  btwnz  12637  indstr  12875  qre  12912  elpq  12934  elpqb  12935  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  nnrp  12963  nnledivrp  13065  qbtwnre  13159  elfzo0le  13664  fzonmapblen  13669  fzo1fzo0n0  13676  ubmelfzo  13691  fzonn0p1p1  13705  ubmelm1fzo  13724  subfzo0  13750  adddivflid  13780  flltdivnn0lt  13795  quoremz  13817  quoremnn0ALT  13819  intfracq  13821  fldiv  13822  modmulnn  13851  m1modnnsub1  13882  addmodid  13884  modifeq2int  13898  modaddmodup  13899  modaddmodlo  13900  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  nnlesq  14170  digit2  14201  digit1  14202  expnngt1  14206  facdiv  14252  facndiv  14253  faclbnd  14255  faclbnd3  14257  faclbnd4lem4  14261  faclbnd5  14263  bcval5  14283  seqcoll  14429  ccatval21sw  14550  cshwidxmod  14768  cshwidxm1  14772  repswcshw  14777  isercolllem1  15631  harmonic  15825  efaddlem  16059  rpnnen2lem9  16190  rpnnen2lem12  16193  sqrt2irr  16217  nndivdvds  16231  dvdsle  16280  fzm1ndvds  16292  nno  16352  nnoddm1d2  16356  divalg2  16375  divalgmod  16376  ndvdsadd  16380  modgcd  16502  gcdzeq  16522  nn0rppwr  16531  sqgcd  16532  nn0expgcd  16534  dvdssqlem  16536  lcmgcdlem  16576  lcmf  16603  coprmgcdb  16619  qredeq  16627  qredeu  16628  isprm3  16653  ge2nprmge4  16671  prmdvdsfz  16675  isprm5  16677  ncoprmlnprm  16698  divdenle  16719  phibndlem  16740  eulerthlem2  16752  hashgcdlem  16758  oddprm  16781  pythagtriplem10  16791  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  pythagtriplem19  16804  pclem  16809  pc2dvds  16850  pcmpt  16863  fldivp1  16868  pcbc  16871  infpnlem1  16881  infpn2  16884  prmreclem1  16887  prmreclem3  16889  vdwlem3  16954  ram0  16993  prmgaplem4  17025  prmgaplem7  17028  cshwshashlem1  17066  cshwshashlem2  17067  setsstruct2  17144  mulgnegnn  19016  mulgmodid  19045  odmodnn0  19470  gexdvds  19514  sylow3lem6  19562  prmirredlem  21382  znidomb  21471  chfacfisf  22741  chfacfisfcpmat  22742  chfacffsupp  22743  chfacfscmul0  22745  chfacfpmmul0  22749  ovolunlem1a  25397  ovoliunlem2  25404  ovolicc2lem3  25420  ovolicc2lem4  25421  iundisj2  25450  dyadss  25495  volsup2  25506  volivth  25508  vitali  25514  ismbf3d  25555  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  itg2seq  25643  itg2gt0  25661  itg2cnlem1  25662  idomrootle  26078  plyeq0lem  26115  dgreq0  26171  dgrcolem2  26180  elqaalem2  26228  elqaalem3  26229  logtayllem  26568  leibpi  26852  birthdaylem3  26863  zetacvg  26925  eldmgm  26932  basellem1  26991  basellem2  26992  basellem3  26993  basellem6  26996  basellem9  26999  prmorcht  27088  dvdsflsumcom  27098  muinv  27103  vmalelog  27116  chtublem  27122  logfac2  27128  logfaclbnd  27133  pcbcctr  27187  bcmono  27188  bposlem1  27195  bposlem5  27199  bposlem6  27200  bpos  27204  lgsval4a  27230  gausslemma2dlem0c  27269  gausslemma2dlem0d  27270  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem3  27279  gausslemma2dlem5  27282  lgsquadlem1  27291  lgsquadlem2  27292  2lgslem1a1  27300  2sqreunnlem1  27360  2sqreunnltlem  27361  dchrisum0re  27424  dchrisum0lem1  27427  logdivbnd  27467  ostth2lem1  27529  ostth2lem3  27546  pthdlem2lem  29697  crctcshwlkn0lem1  29740  crctcshwlkn0lem3  29742  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem6  29745  crctcshwlkn0lem7  29746  crctcshwlkn0  29751  clwlkclwwlkf1lem2  29934  clwwisshclwwslem  29943  clwwlkel  29975  clwwlkf  29976  clwwlkf1  29978  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  eucrctshift  30172  eucrct2eupth  30174  numclwlk2lem2f  30306  nmounbseqi  30706  nmounbseqiALT  30707  nmobndseqi  30708  nmobndseqiALT  30709  ubthlem1  30799  minvecolem3  30805  lnconi  31962  iundisj2f  32519  nnmulge  32662  xrsmulgzz  32947  esumpmono  34069  eulerpartlemb  34359  fibp1  34392  subfaclim  35175  subfacval3  35176  snmlff  35316  fz0n  35718  bcprod  35725  nn0prpwlem  36310  nn0prpw  36311  nndivsub  36445  nndivlub  36446  knoppcnlem2  36482  knoppcnlem4  36484  knoppndvlem11  36510  knoppndvlem12  36511  knoppndvlem14  36513  poimirlem13  37627  poimirlem14  37628  poimirlem31  37645  poimirlem32  37646  mblfinlem2  37652  fzmul  37735  incsequz  37742  nnubfi  37744  nninfnub  37745  2ap1caineq  42133  sticksstones1  42134  unitscyglem5  42187  nnadddir  42258  nnmul1com  42259  sn-nnne0  42448  nn0addcom  42450  renegmulnnass  42453  nn0mulcom  42454  zmulcomlem  42455  fimgmcyc  42522  irrapxlem1  42810  irrapxlem2  42811  pellexlem1  42817  pellexlem5  42821  pellqrex  42867  monotoddzzfi  42931  jm2.24nn  42948  congabseq  42963  acongrep  42969  acongeq  42972  expdiophlem1  43010  idomodle  43180  relexpmulnn  43698  prmunb2  44300  hashnzfzclim  44311  fmuldfeq  45581  sumnnodd  45628  stoweidlem14  46012  stoweidlem17  46015  stoweidlem20  46018  stoweidlem49  46047  stoweidlem60  46058  wallispilem3  46065  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem1  46072  stirlinglem3  46074  stirlinglem4  46075  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlingr  46088  dirker2re  46090  dirkerval2  46092  dirkerre  46093  dirkertrigeqlem1  46096  fourierdlem66  46170  fourierdlem73  46177  fourierdlem83  46187  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fouriersw  46229  etransclem24  46256  sge0rpcpnf  46419  hoicvr  46546  hoicvrrex  46554  vonioolem2  46679  vonicclem2  46682  fsupdm  46840  finfdm  46844  smfinfdmmbllem  46846  subsubelfzo0  47327  ceilhalfelfzo1  47331  2tceilhalfelfzo1  47333  ceilhalfnn  47337  addmodne  47345  submodlt  47351  modn0mul  47358  m1modmmod  47359  difmodm1lt  47360  modlt0b  47364  fmtnodvds  47545  2pwp1prm  47590  lighneallem2  47607  nn0oALTV  47697  nneven  47699  nnsum4primes4  47790  nnsum4primesprm  47792  nnsum4primesgbe  47794  nnsum4primesle9  47796  bgoldbachlt  47814  tgoldbach  47818  gpgusgralem  48047  gpgedgvtx0  48052  gpg3kgrtriexlem1  48074  gpg3kgrtriexlem2  48075  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  altgsumbcALT  48341  nnlog2ge0lt1  48555  logbpw2m1  48556  blennn  48564  blennnelnn  48565  nnpw2pmod  48572  nnolog2flm1  48579  digvalnn0  48588  dignn0fr  48590  dignn0ldlem  48591  dignnld  48592  dig2nn1st  48594