Theorem nnre 12245

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11126  ℕcn 12238

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-nn 12239

This theorem is referenced by:  nnrei  12247  nnmulcl  12262  nn2ge  12265  nnge1  12266  nngt1ne1  12267  nnle1eq1  12268  nngt0  12269  nnnlt1  12270  nnnle0  12271  nndivre  12279  nnrecgt0  12281  nnsub  12282  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  12930  qre  12967  elpq  12989  elpqb  12990  rpnnen1lem2  12991  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem5  12995  nnrp  13018  nnledivrp  13119  qbtwnre  13213  elfzo0le  13718  fzonmapblen  13723  fzo1fzo0n0  13729  ubmelfzo  13744  fzonn0p1p1  13758  ubmelm1fzo  13777  subfzo0  13803  adddivflid  13833  flltdivnn0lt  13848  quoremz  13870  quoremnn0ALT  13872  intfracq  13874  fldiv  13875  modmulnn  13904  m1modnnsub1  13933  addmodid  13935  modifeq2int  13949  modaddmodup  13950  modaddmodlo  13951  modfzo0difsn  13959  modsumfzodifsn  13960  addmodlteq  13962  nnlesq  14221  digit2  14252  digit1  14253  expnngt1  14257  facdiv  14303  facndiv  14304  faclbnd  14306  faclbnd3  14308  faclbnd4lem4  14312  faclbnd5  14314  bcval5  14334  seqcoll  14480  ccatval21sw  14601  cshwidxmod  14819  cshwidxm1  14823  repswcshw  14828  isercolllem1  15679  harmonic  15873  efaddlem  16107  rpnnen2lem9  16238  rpnnen2lem12  16241  sqrt2irr  16265  nndivdvds  16279  dvdsle  16327  fzm1ndvds  16339  nno  16399  nnoddm1d2  16403  divalg2  16422  divalgmod  16423  ndvdsadd  16427  modgcd  16549  gcdzeq  16569  nn0rppwr  16578  sqgcd  16579  nn0expgcd  16581  dvdssqlem  16583  lcmgcdlem  16623  lcmf  16650  coprmgcdb  16666  qredeq  16674  qredeu  16675  isprm3  16700  ge2nprmge4  16718  prmdvdsfz  16722  isprm5  16724  ncoprmlnprm  16745  divdenle  16766  phibndlem  16787  eulerthlem2  16799  hashgcdlem  16805  oddprm  16828  pythagtriplem10  16838  pythagtriplem12  16844  pythagtriplem14  16846  pythagtriplem16  16848  pythagtriplem19  16851  pclem  16856  pc2dvds  16897  pcmpt  16910  fldivp1  16915  pcbc  16918  infpnlem1  16928  infpn2  16931  prmreclem1  16934  prmreclem3  16936  vdwlem3  17001  ram0  17040  prmgaplem4  17072  prmgaplem7  17075  cshwshashlem1  17113  cshwshashlem2  17114  setsstruct2  17191  mulgnegnn  19065  mulgmodid  19094  odmodnn0  19519  gexdvds  19563  sylow3lem6  19611  prmirredlem  21431  znidomb  21520  chfacfisf  22790  chfacfisfcpmat  22791  chfacffsupp  22792  chfacfscmul0  22794  chfacfpmmul0  22798  ovolunlem1a  25447  ovoliunlem2  25454  ovolicc2lem3  25470  ovolicc2lem4  25471  iundisj2  25500  dyadss  25545  volsup2  25556  volivth  25558  vitali  25564  ismbf3d  25605  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  itg2seq  25693  itg2gt0  25711  itg2cnlem1  25712  idomrootle  26128  plyeq0lem  26165  dgreq0  26221  dgrcolem2  26230  elqaalem2  26278  elqaalem3  26279  logtayllem  26618  leibpi  26902  birthdaylem3  26913  zetacvg  26975  eldmgm  26982  basellem1  27041  basellem2  27042  basellem3  27043  basellem6  27046  basellem9  27049  prmorcht  27138  dvdsflsumcom  27148  muinv  27153  vmalelog  27166  chtublem  27172  logfac2  27178  logfaclbnd  27183  pcbcctr  27237  bcmono  27238  bposlem1  27245  bposlem5  27249  bposlem6  27250  bpos  27254  lgsval4a  27280  gausslemma2dlem0c  27319  gausslemma2dlem0d  27320  gausslemma2dlem1a  27326  gausslemma2dlem2  27328  gausslemma2dlem3  27329  gausslemma2dlem5  27332  lgsquadlem1  27341  lgsquadlem2  27342  2lgslem1a1  27350  2sqreunnlem1  27410  2sqreunnltlem  27411  dchrisum0re  27474  dchrisum0lem1  27477  logdivbnd  27517  ostth2lem1  27579  ostth2lem3  27596  pthdlem2lem  29695  crctcshwlkn0lem1  29738  crctcshwlkn0lem3  29740  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  crctcshwlkn0lem6  29743  crctcshwlkn0lem7  29744  crctcshwlkn0  29749  clwlkclwwlkf1lem2  29932  clwwisshclwwslem  29941  clwwlkel  29973  clwwlkf  29974  clwwlkf1  29976  wwlksext2clwwlk  29984  wwlksubclwwlk  29985  eucrctshift  30170  eucrct2eupth  30172  numclwlk2lem2f  30304  nmounbseqi  30704  nmounbseqiALT  30705  nmobndseqi  30706  nmobndseqiALT  30707  ubthlem1  30797  minvecolem3  30803  lnconi  31960  iundisj2f  32517  nnmulge  32662  xrsmulgzz  32947  esumpmono  34056  eulerpartlemb  34346  fibp1  34379  subfaclim  35156  subfacval3  35157  snmlff  35297  fz0n  35694  bcprod  35701  nn0prpwlem  36286  nn0prpw  36287  nndivsub  36421  nndivlub  36422  knoppcnlem2  36458  knoppcnlem4  36460  knoppndvlem11  36486  knoppndvlem12  36487  knoppndvlem14  36489  poimirlem13  37603  poimirlem14  37604  poimirlem31  37621  poimirlem32  37622  mblfinlem2  37628  fzmul  37711  incsequz  37718  nnubfi  37720  nninfnub  37721  2ap1caineq  42104  sticksstones1  42105  unitscyglem5  42158  metakunt26  42189  metakunt29  42192  metakunt30  42193  factwoffsmonot  42201  nnadddir  42267  nnmul1com  42268  sn-nnne0  42438  nn0addcom  42440  renegmulnnass  42443  nn0mulcom  42444  zmulcomlem  42445  fimgmcyc  42504  irrapxlem1  42792  irrapxlem2  42793  pellexlem1  42799  pellexlem5  42803  pellqrex  42849  monotoddzzfi  42913  jm2.24nn  42930  congabseq  42945  acongrep  42951  acongeq  42954  expdiophlem1  42992  idomodle  43162  relexpmulnn  43680  prmunb2  44283  hashnzfzclim  44294  fmuldfeq  45560  sumnnodd  45607  stoweidlem14  45991  stoweidlem17  45994  stoweidlem20  45997  stoweidlem49  46026  stoweidlem60  46037  wallispilem3  46044  wallispilem4  46045  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  stirlinglem1  46051  stirlinglem3  46053  stirlinglem4  46054  stirlinglem6  46056  stirlinglem7  46057  stirlinglem10  46060  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  stirlingr  46067  dirker2re  46069  dirkerval2  46071  dirkerre  46072  dirkertrigeqlem1  46075  fourierdlem66  46149  fourierdlem73  46156  fourierdlem83  46166  fourierdlem87  46170  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fouriersw  46208  etransclem24  46235  sge0rpcpnf  46398  hoicvr  46525  hoicvrrex  46533  vonioolem2  46658  vonicclem2  46661  fsupdm  46819  finfdm  46823  smfinfdmmbllem  46825  subsubelfzo0  47303  ceilhalfelfzo1  47307  2tceilhalfelfzo1  47309  ceilhalfnn  47313  addmodne  47321  submodlt  47327  fmtnodvds  47506  2pwp1prm  47551  lighneallem2  47568  nn0oALTV  47658  nneven  47660  nnsum4primes4  47751  nnsum4primesprm  47753  nnsum4primesgbe  47755  nnsum4primesle9  47757  bgoldbachlt  47775  tgoldbach  47779  gpgusgralem  48008  gpgedgvtx0  48013  gpg3kgrtriexlem1  48033  gpg3kgrtriexlem2  48034  gpg3kgrtriexlem3  48035  gpg3kgrtriexlem4  48036  gpg3kgrtriexlem6  48038  altgsumbcALT  48276  modn0mul  48448  m1modmmod  48449  difmodm1lt  48450  nnlog2ge0lt1  48494  logbpw2m1  48495  blennn  48503  blennnelnn  48504  nnpw2pmod  48511  nnolog2flm1  48518  digvalnn0  48527  dignn0fr  48529  dignn0ldlem  48530  dignnld  48531  dig2nn1st  48533