Theorem nnre 12169

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11043  ℕcn 12162

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 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

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 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163

This theorem is referenced by:  nnrei  12171  nnmulcl  12186  nn2ge  12189  nnge1  12190  nngt1ne1  12191  nnle1eq1  12192  nngt0  12193  nnnlt1  12194  nnnle0  12195  nndivre  12203  nnrecgt0  12205  nnsub  12206  nnunb  12414  arch  12415  nnrecl  12416  bndndx  12417  0mnnnnn0  12450  nnnegz  12508  elnnz  12515  elz2  12523  nnz  12526  gtndiv  12587  prime  12591  btwnz  12613  indstr  12851  qre  12888  elpq  12910  elpqb  12911  rpnnen1lem2  12912  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem5  12916  nnrp  12939  nnledivrp  13041  qbtwnre  13135  elfzo0le  13640  fzonmapblen  13645  fzo1fzo0n0  13652  ubmelfzo  13667  fzonn0p1p1  13681  ubmelm1fzo  13700  subfzo0  13726  adddivflid  13756  flltdivnn0lt  13771  quoremz  13793  quoremnn0ALT  13795  intfracq  13797  fldiv  13798  modmulnn  13827  m1modnnsub1  13858  addmodid  13860  modifeq2int  13874  modaddmodup  13875  modaddmodlo  13876  modfzo0difsn  13884  modsumfzodifsn  13885  addmodlteq  13887  nnlesq  14146  digit2  14177  digit1  14178  expnngt1  14182  facdiv  14228  facndiv  14229  faclbnd  14231  faclbnd3  14233  faclbnd4lem4  14237  faclbnd5  14239  bcval5  14259  seqcoll  14405  ccatval21sw  14526  cshwidxmod  14744  cshwidxm1  14748  repswcshw  14753  isercolllem1  15607  harmonic  15801  efaddlem  16035  rpnnen2lem9  16166  rpnnen2lem12  16169  sqrt2irr  16193  nndivdvds  16207  dvdsle  16256  fzm1ndvds  16268  nno  16328  nnoddm1d2  16332  divalg2  16351  divalgmod  16352  ndvdsadd  16356  modgcd  16478  gcdzeq  16498  nn0rppwr  16507  sqgcd  16508  nn0expgcd  16510  dvdssqlem  16512  lcmgcdlem  16552  lcmf  16579  coprmgcdb  16595  qredeq  16603  qredeu  16604  isprm3  16629  ge2nprmge4  16647  prmdvdsfz  16651  isprm5  16653  ncoprmlnprm  16674  divdenle  16695  phibndlem  16716  eulerthlem2  16728  hashgcdlem  16734  oddprm  16757  pythagtriplem10  16767  pythagtriplem12  16773  pythagtriplem14  16775  pythagtriplem16  16777  pythagtriplem19  16780  pclem  16785  pc2dvds  16826  pcmpt  16839  fldivp1  16844  pcbc  16847  infpnlem1  16857  infpn2  16860  prmreclem1  16863  prmreclem3  16865  vdwlem3  16930  ram0  16969  prmgaplem4  17001  prmgaplem7  17004  cshwshashlem1  17042  cshwshashlem2  17043  setsstruct2  17120  mulgnegnn  18992  mulgmodid  19021  odmodnn0  19446  gexdvds  19490  sylow3lem6  19538  prmirredlem  21358  znidomb  21447  chfacfisf  22717  chfacfisfcpmat  22718  chfacffsupp  22719  chfacfscmul0  22721  chfacfpmmul0  22725  ovolunlem1a  25373  ovoliunlem2  25380  ovolicc2lem3  25396  ovolicc2lem4  25397  iundisj2  25426  dyadss  25471  volsup2  25482  volivth  25484  vitali  25490  ismbf3d  25531  mbfi1fseqlem3  25594  mbfi1fseqlem4  25595  mbfi1fseqlem5  25596  itg2seq  25619  itg2gt0  25637  itg2cnlem1  25638  idomrootle  26054  plyeq0lem  26091  dgreq0  26147  dgrcolem2  26156  elqaalem2  26204  elqaalem3  26205  logtayllem  26544  leibpi  26828  birthdaylem3  26839  zetacvg  26901  eldmgm  26908  basellem1  26967  basellem2  26968  basellem3  26969  basellem6  26972  basellem9  26975  prmorcht  27064  dvdsflsumcom  27074  muinv  27079  vmalelog  27092  chtublem  27098  logfac2  27104  logfaclbnd  27109  pcbcctr  27163  bcmono  27164  bposlem1  27171  bposlem5  27175  bposlem6  27176  bpos  27180  lgsval4a  27206  gausslemma2dlem0c  27245  gausslemma2dlem0d  27246  gausslemma2dlem1a  27252  gausslemma2dlem2  27254  gausslemma2dlem3  27255  gausslemma2dlem5  27258  lgsquadlem1  27267  lgsquadlem2  27268  2lgslem1a1  27276  2sqreunnlem1  27336  2sqreunnltlem  27337  dchrisum0re  27400  dchrisum0lem1  27403  logdivbnd  27443  ostth2lem1  27505  ostth2lem3  27522  pthdlem2lem  29670  crctcshwlkn0lem1  29713  crctcshwlkn0lem3  29715  crctcshwlkn0lem4  29716  crctcshwlkn0lem5  29717  crctcshwlkn0lem6  29718  crctcshwlkn0lem7  29719  crctcshwlkn0  29724  clwlkclwwlkf1lem2  29907  clwwisshclwwslem  29916  clwwlkel  29948  clwwlkf  29949  clwwlkf1  29951  wwlksext2clwwlk  29959  wwlksubclwwlk  29960  eucrctshift  30145  eucrct2eupth  30147  numclwlk2lem2f  30279  nmounbseqi  30679  nmounbseqiALT  30680  nmobndseqi  30681  nmobndseqiALT  30682  ubthlem1  30772  minvecolem3  30778  lnconi  31935  iundisj2f  32492  nnmulge  32635  xrsmulgzz  32920  esumpmono  34042  eulerpartlemb  34332  fibp1  34365  subfaclim  35148  subfacval3  35149  snmlff  35289  fz0n  35691  bcprod  35698  nn0prpwlem  36283  nn0prpw  36284  nndivsub  36418  nndivlub  36419  knoppcnlem2  36455  knoppcnlem4  36457  knoppndvlem11  36483  knoppndvlem12  36484  knoppndvlem14  36486  poimirlem13  37600  poimirlem14  37601  poimirlem31  37618  poimirlem32  37619  mblfinlem2  37625  fzmul  37708  incsequz  37715  nnubfi  37717  nninfnub  37718  2ap1caineq  42106  sticksstones1  42107  unitscyglem5  42160  nnadddir  42231  nnmul1com  42232  sn-nnne0  42421  nn0addcom  42423  renegmulnnass  42426  nn0mulcom  42427  zmulcomlem  42428  fimgmcyc  42495  irrapxlem1  42783  irrapxlem2  42784  pellexlem1  42790  pellexlem5  42794  pellqrex  42840  monotoddzzfi  42904  jm2.24nn  42921  congabseq  42936  acongrep  42942  acongeq  42945  expdiophlem1  42983  idomodle  43153  relexpmulnn  43671  prmunb2  44273  hashnzfzclim  44284  fmuldfeq  45554  sumnnodd  45601  stoweidlem14  45985  stoweidlem17  45988  stoweidlem20  45991  stoweidlem49  46020  stoweidlem60  46031  wallispilem3  46038  wallispilem4  46039  wallispilem5  46040  wallispi  46041  wallispi2lem1  46042  wallispi2lem2  46043  stirlinglem1  46045  stirlinglem3  46047  stirlinglem4  46048  stirlinglem6  46050  stirlinglem7  46051  stirlinglem10  46054  stirlinglem11  46055  stirlinglem12  46056  stirlinglem13  46057  stirlingr  46061  dirker2re  46063  dirkerval2  46065  dirkerre  46066  dirkertrigeqlem1  46069  fourierdlem66  46143  fourierdlem73  46150  fourierdlem83  46160  fourierdlem87  46164  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fouriersw  46202  etransclem24  46229  sge0rpcpnf  46392  hoicvr  46519  hoicvrrex  46527  vonioolem2  46652  vonicclem2  46655  fsupdm  46813  finfdm  46817  smfinfdmmbllem  46819  subsubelfzo0  47300  ceilhalfelfzo1  47304  2tceilhalfelfzo1  47306  ceilhalfnn  47310  addmodne  47318  submodlt  47324  modn0mul  47331  m1modmmod  47332  difmodm1lt  47333  modlt0b  47337  fmtnodvds  47518  2pwp1prm  47563  lighneallem2  47580  nn0oALTV  47670  nneven  47672  nnsum4primes4  47763  nnsum4primesprm  47765  nnsum4primesgbe  47767  nnsum4primesle9  47769  bgoldbachlt  47787  tgoldbach  47791  gpgusgralem  48020  gpgedgvtx0  48025  gpg3kgrtriexlem1  48047  gpg3kgrtriexlem2  48048  gpg3kgrtriexlem3  48049  gpg3kgrtriexlem4  48050  gpg3kgrtriexlem6  48052  altgsumbcALT  48314  nnlog2ge0lt1  48528  logbpw2m1  48529  blennn  48537  blennnelnn  48538  nnpw2pmod  48545  nnolog2flm1  48552  digvalnn0  48561  dignn0fr  48563  dignn0ldlem  48564  dignnld  48565  dig2nn1st  48567