Theorem nnre 12273

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11154  ℕcn 12266

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267

This theorem is referenced by:  nnrei  12275  nnmulcl  12290  nn2ge  12293  nnge1  12294  nngt1ne1  12295  nnle1eq1  12296  nngt0  12297  nnnlt1  12298  nnnle0  12299  nndivre  12307  nnrecgt0  12309  nnsub  12310  nnunb  12522  arch  12523  nnrecl  12524  bndndx  12525  0mnnnnn0  12558  nnnegz  12616  elnnz  12623  elz2  12631  nnz  12634  gtndiv  12695  prime  12699  btwnz  12721  indstr  12958  qre  12995  elpq  13017  elpqb  13018  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  nnrp  13046  nnledivrp  13147  qbtwnre  13241  elfzo0le  13743  fzonmapblen  13748  fzo1fzo0n0  13754  ubmelfzo  13769  fzonn0p1p1  13783  ubmelm1fzo  13802  subfzo0  13828  adddivflid  13858  flltdivnn0lt  13873  quoremz  13895  quoremnn0ALT  13897  intfracq  13899  fldiv  13900  modmulnn  13929  m1modnnsub1  13958  addmodid  13960  modifeq2int  13974  modaddmodup  13975  modaddmodlo  13976  modfzo0difsn  13984  modsumfzodifsn  13985  addmodlteq  13987  nnlesq  14244  digit2  14275  digit1  14276  expnngt1  14280  facdiv  14326  facndiv  14327  faclbnd  14329  faclbnd3  14331  faclbnd4lem4  14335  faclbnd5  14337  bcval5  14357  seqcoll  14503  ccatval21sw  14623  cshwidxmod  14841  cshwidxm1  14845  repswcshw  14850  isercolllem1  15701  harmonic  15895  efaddlem  16129  rpnnen2lem9  16258  rpnnen2lem12  16261  sqrt2irr  16285  nndivdvds  16299  dvdsle  16347  fzm1ndvds  16359  nno  16419  nnoddm1d2  16423  divalg2  16442  divalgmod  16443  ndvdsadd  16447  modgcd  16569  gcdzeq  16589  nn0rppwr  16598  sqgcd  16599  nn0expgcd  16601  dvdssqlem  16603  lcmgcdlem  16643  lcmf  16670  coprmgcdb  16686  qredeq  16694  qredeu  16695  isprm3  16720  ge2nprmge4  16738  prmdvdsfz  16742  isprm5  16744  ncoprmlnprm  16765  divdenle  16786  phibndlem  16807  eulerthlem2  16819  hashgcdlem  16825  oddprm  16848  pythagtriplem10  16858  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem16  16868  pythagtriplem19  16871  pclem  16876  pc2dvds  16917  pcmpt  16930  fldivp1  16935  pcbc  16938  infpnlem1  16948  infpn2  16951  prmreclem1  16954  prmreclem3  16956  vdwlem3  17021  ram0  17060  prmgaplem4  17092  prmgaplem7  17095  cshwshashlem1  17133  cshwshashlem2  17134  setsstruct2  17211  mulgnegnn  19102  mulgmodid  19131  odmodnn0  19558  gexdvds  19602  sylow3lem6  19650  prmirredlem  21483  znidomb  21580  chfacfisf  22860  chfacfisfcpmat  22861  chfacffsupp  22862  chfacfscmul0  22864  chfacfpmmul0  22868  ovolunlem1a  25531  ovoliunlem2  25538  ovolicc2lem3  25554  ovolicc2lem4  25555  iundisj2  25584  dyadss  25629  volsup2  25640  volivth  25642  vitali  25648  ismbf3d  25689  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  itg2seq  25777  itg2gt0  25795  itg2cnlem1  25796  idomrootle  26212  plyeq0lem  26249  dgreq0  26305  dgrcolem2  26314  elqaalem2  26362  elqaalem3  26363  logtayllem  26701  leibpi  26985  birthdaylem3  26996  zetacvg  27058  eldmgm  27065  basellem1  27124  basellem2  27125  basellem3  27126  basellem6  27129  basellem9  27132  prmorcht  27221  dvdsflsumcom  27231  muinv  27236  vmalelog  27249  chtublem  27255  logfac2  27261  logfaclbnd  27266  pcbcctr  27320  bcmono  27321  bposlem1  27328  bposlem5  27332  bposlem6  27333  bpos  27337  lgsval4a  27363  gausslemma2dlem0c  27402  gausslemma2dlem0d  27403  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem3  27412  gausslemma2dlem5  27415  lgsquadlem1  27424  lgsquadlem2  27425  2lgslem1a1  27433  2sqreunnlem1  27493  2sqreunnltlem  27494  dchrisum0re  27557  dchrisum0lem1  27560  logdivbnd  27600  ostth2lem1  27662  ostth2lem3  27679  pthdlem2lem  29787  crctcshwlkn0lem1  29830  crctcshwlkn0lem3  29832  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem6  29835  crctcshwlkn0lem7  29836  crctcshwlkn0  29841  clwlkclwwlkf1lem2  30024  clwwisshclwwslem  30033  clwwlkel  30065  clwwlkf  30066  clwwlkf1  30068  wwlksext2clwwlk  30076  wwlksubclwwlk  30077  eucrctshift  30262  eucrct2eupth  30264  numclwlk2lem2f  30396  nmounbseqi  30796  nmounbseqiALT  30797  nmobndseqi  30798  nmobndseqiALT  30799  ubthlem1  30889  minvecolem3  30895  lnconi  32052  iundisj2f  32603  nnmulge  32749  xrsmulgzz  33011  esumpmono  34080  eulerpartlemb  34370  fibp1  34403  subfaclim  35193  subfacval3  35194  snmlff  35334  fz0n  35731  bcprod  35738  nn0prpwlem  36323  nn0prpw  36324  nndivsub  36458  nndivlub  36459  knoppcnlem2  36495  knoppcnlem4  36497  knoppndvlem11  36523  knoppndvlem12  36524  knoppndvlem14  36526  poimirlem13  37640  poimirlem14  37641  poimirlem31  37658  poimirlem32  37659  mblfinlem2  37665  fzmul  37748  incsequz  37755  nnubfi  37757  nninfnub  37758  2ap1caineq  42146  sticksstones1  42147  unitscyglem5  42200  metakunt26  42231  metakunt29  42234  metakunt30  42235  factwoffsmonot  42243  nnadddir  42305  nnmul1com  42306  sn-nnne0  42478  nn0addcom  42480  renegmulnnass  42483  nn0mulcom  42484  zmulcomlem  42485  fimgmcyc  42544  irrapxlem1  42833  irrapxlem2  42834  pellexlem1  42840  pellexlem5  42844  pellqrex  42890  monotoddzzfi  42954  jm2.24nn  42971  congabseq  42986  acongrep  42992  acongeq  42995  expdiophlem1  43033  idomodle  43203  relexpmulnn  43722  prmunb2  44330  hashnzfzclim  44341  fmuldfeq  45598  sumnnodd  45645  stoweidlem14  46029  stoweidlem17  46032  stoweidlem20  46035  stoweidlem49  46064  stoweidlem60  46075  wallispilem3  46082  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  stirlinglem1  46089  stirlinglem3  46091  stirlinglem4  46092  stirlinglem6  46094  stirlinglem7  46095  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlingr  46105  dirker2re  46107  dirkerval2  46109  dirkerre  46110  dirkertrigeqlem1  46113  fourierdlem66  46187  fourierdlem73  46194  fourierdlem83  46204  fourierdlem87  46208  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fouriersw  46246  etransclem24  46273  sge0rpcpnf  46436  hoicvr  46563  hoicvrrex  46571  vonioolem2  46696  vonicclem2  46699  fsupdm  46857  finfdm  46861  smfinfdmmbllem  46863  subsubelfzo0  47338  addmodne  47346  submodlt  47352  fmtnodvds  47531  2pwp1prm  47576  lighneallem2  47593  nn0oALTV  47683  nneven  47685  nnsum4primes4  47776  nnsum4primesprm  47778  nnsum4primesgbe  47780  nnsum4primesle9  47782  bgoldbachlt  47800  tgoldbach  47804  gpgusgralem  48011  ceilhalfelfzo1  48016  2tceilhalfelfzo1  48018  gpgedgvtx0  48019  gpg3kgrtriexlem1  48039  gpg3kgrtriexlem2  48040  gpg3kgrtriexlem3  48041  gpg3kgrtriexlem4  48042  gpg3kgrtriexlem6  48044  altgsumbcALT  48269  modn0mul  48441  m1modmmod  48442  difmodm1lt  48443  nnlog2ge0lt1  48487  logbpw2m1  48488  blennn  48496  blennnelnn  48497  nnpw2pmod  48504  nnolog2flm1  48511  digvalnn0  48520  dignn0fr  48522  dignn0ldlem  48523  dignnld  48524  dig2nn1st  48526