Theorem nnre 12135

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11008  ℕcn 12128

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 5235  ax-nul 5245  ax-pr 5371  ax-un 7671  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

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 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-nn 12129

This theorem is referenced by:  nnrei  12137  nnmulcl  12152  nn2ge  12155  nnge1  12156  nngt1ne1  12157  nnle1eq1  12158  nngt0  12159  nnnlt1  12160  nnnle0  12161  nndivre  12169  nnrecgt0  12171  nnsub  12172  nnunb  12380  arch  12381  nnrecl  12382  bndndx  12383  0mnnnnn0  12416  nnnegz  12474  elnnz  12481  elz2  12489  nnz  12492  gtndiv  12553  prime  12557  btwnz  12579  indstr  12817  qre  12854  elpq  12876  elpqb  12877  rpnnen1lem2  12878  rpnnen1lem1  12879  rpnnen1lem3  12880  rpnnen1lem5  12882  nnrp  12905  nnledivrp  13007  qbtwnre  13101  elfzo0le  13606  fzonmapblen  13611  fzo1fzo0n0  13618  ubmelfzo  13633  fzonn0p1p1  13647  ubmelm1fzo  13666  subfzo0  13692  adddivflid  13722  flltdivnn0lt  13737  quoremz  13759  quoremnn0ALT  13761  intfracq  13763  fldiv  13764  modmulnn  13793  m1modnnsub1  13824  addmodid  13826  modifeq2int  13840  modaddmodup  13841  modaddmodlo  13842  modfzo0difsn  13850  modsumfzodifsn  13851  addmodlteq  13853  nnlesq  14112  digit2  14143  digit1  14144  expnngt1  14148  facdiv  14194  facndiv  14195  faclbnd  14197  faclbnd3  14199  faclbnd4lem4  14203  faclbnd5  14205  bcval5  14225  seqcoll  14371  ccatval21sw  14492  cshwidxmod  14709  cshwidxm1  14713  repswcshw  14718  isercolllem1  15572  harmonic  15766  efaddlem  16000  rpnnen2lem9  16131  rpnnen2lem12  16134  sqrt2irr  16158  nndivdvds  16172  dvdsle  16221  fzm1ndvds  16233  nno  16293  nnoddm1d2  16297  divalg2  16316  divalgmod  16317  ndvdsadd  16321  modgcd  16443  gcdzeq  16463  nn0rppwr  16472  sqgcd  16473  nn0expgcd  16475  dvdssqlem  16477  lcmgcdlem  16517  lcmf  16544  coprmgcdb  16560  qredeq  16568  qredeu  16569  isprm3  16594  ge2nprmge4  16612  prmdvdsfz  16616  isprm5  16618  ncoprmlnprm  16639  divdenle  16660  phibndlem  16681  eulerthlem2  16693  hashgcdlem  16699  oddprm  16722  pythagtriplem10  16732  pythagtriplem12  16738  pythagtriplem14  16740  pythagtriplem16  16742  pythagtriplem19  16745  pclem  16750  pc2dvds  16791  pcmpt  16804  fldivp1  16809  pcbc  16812  infpnlem1  16822  infpn2  16825  prmreclem1  16828  prmreclem3  16830  vdwlem3  16895  ram0  16934  prmgaplem4  16966  prmgaplem7  16969  cshwshashlem1  17007  cshwshashlem2  17008  setsstruct2  17085  mulgnegnn  18963  mulgmodid  18992  odmodnn0  19419  gexdvds  19463  sylow3lem6  19511  prmirredlem  21379  znidomb  21468  chfacfisf  22739  chfacfisfcpmat  22740  chfacffsupp  22741  chfacfscmul0  22743  chfacfpmmul0  22747  ovolunlem1a  25395  ovoliunlem2  25402  ovolicc2lem3  25418  ovolicc2lem4  25419  iundisj2  25448  dyadss  25493  volsup2  25504  volivth  25506  vitali  25512  ismbf3d  25553  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  itg2seq  25641  itg2gt0  25659  itg2cnlem1  25660  idomrootle  26076  plyeq0lem  26113  dgreq0  26169  dgrcolem2  26178  elqaalem2  26226  elqaalem3  26227  logtayllem  26566  leibpi  26850  birthdaylem3  26861  zetacvg  26923  eldmgm  26930  basellem1  26989  basellem2  26990  basellem3  26991  basellem6  26994  basellem9  26997  prmorcht  27086  dvdsflsumcom  27096  muinv  27101  vmalelog  27114  chtublem  27120  logfac2  27126  logfaclbnd  27131  pcbcctr  27185  bcmono  27186  bposlem1  27193  bposlem5  27197  bposlem6  27198  bpos  27202  lgsval4a  27228  gausslemma2dlem0c  27267  gausslemma2dlem0d  27268  gausslemma2dlem1a  27274  gausslemma2dlem2  27276  gausslemma2dlem3  27277  gausslemma2dlem5  27280  lgsquadlem1  27289  lgsquadlem2  27290  2lgslem1a1  27298  2sqreunnlem1  27358  2sqreunnltlem  27359  dchrisum0re  27422  dchrisum0lem1  27425  logdivbnd  27465  ostth2lem1  27527  ostth2lem3  27544  pthdlem2lem  29712  crctcshwlkn0lem1  29755  crctcshwlkn0lem3  29757  crctcshwlkn0lem4  29758  crctcshwlkn0lem5  29759  crctcshwlkn0lem6  29760  crctcshwlkn0lem7  29761  crctcshwlkn0  29766  clwlkclwwlkf1lem2  29949  clwwisshclwwslem  29958  clwwlkel  29990  clwwlkf  29991  clwwlkf1  29993  wwlksext2clwwlk  30001  wwlksubclwwlk  30002  eucrctshift  30187  eucrct2eupth  30189  numclwlk2lem2f  30321  nmounbseqi  30721  nmounbseqiALT  30722  nmobndseqi  30723  nmobndseqiALT  30724  ubthlem1  30814  minvecolem3  30820  lnconi  31977  iundisj2f  32534  nnmulge  32682  xrsmulgzz  32963  esumpmono  34046  eulerpartlemb  34336  fibp1  34369  subfaclim  35165  subfacval3  35166  snmlff  35306  fz0n  35708  bcprod  35715  nn0prpwlem  36300  nn0prpw  36301  nndivsub  36435  nndivlub  36436  knoppcnlem2  36472  knoppcnlem4  36474  knoppndvlem11  36500  knoppndvlem12  36501  knoppndvlem14  36503  poimirlem13  37617  poimirlem14  37618  poimirlem31  37635  poimirlem32  37636  mblfinlem2  37642  fzmul  37725  incsequz  37732  nnubfi  37734  nninfnub  37735  2ap1caineq  42122  sticksstones1  42123  unitscyglem5  42176  nnadddir  42247  nnmul1com  42248  sn-nnne0  42437  nn0addcom  42439  renegmulnnass  42442  nn0mulcom  42443  zmulcomlem  42444  fimgmcyc  42511  irrapxlem1  42799  irrapxlem2  42800  pellexlem1  42806  pellexlem5  42810  pellqrex  42856  monotoddzzfi  42919  jm2.24nn  42936  congabseq  42951  acongrep  42957  acongeq  42960  expdiophlem1  42998  idomodle  43168  relexpmulnn  43686  prmunb2  44288  hashnzfzclim  44299  fmuldfeq  45568  sumnnodd  45615  stoweidlem14  45999  stoweidlem17  46002  stoweidlem20  46005  stoweidlem49  46034  stoweidlem60  46045  wallispilem3  46052  wallispilem4  46053  wallispilem5  46054  wallispi  46055  wallispi2lem1  46056  wallispi2lem2  46057  stirlinglem1  46059  stirlinglem3  46061  stirlinglem4  46062  stirlinglem6  46064  stirlinglem7  46065  stirlinglem10  46068  stirlinglem11  46069  stirlinglem12  46070  stirlinglem13  46071  stirlingr  46075  dirker2re  46077  dirkerval2  46079  dirkerre  46080  dirkertrigeqlem1  46083  fourierdlem66  46157  fourierdlem73  46164  fourierdlem83  46174  fourierdlem87  46178  fourierdlem103  46194  fourierdlem104  46195  fourierdlem111  46202  fouriersw  46216  etransclem24  46243  sge0rpcpnf  46406  hoicvr  46533  hoicvrrex  46541  vonioolem2  46666  vonicclem2  46669  fsupdm  46827  finfdm  46831  smfinfdmmbllem  46833  subsubelfzo0  47314  ceilhalfelfzo1  47318  2tceilhalfelfzo1  47320  ceilhalfnn  47324  addmodne  47332  submodlt  47338  modn0mul  47345  m1modmmod  47346  difmodm1lt  47347  modlt0b  47351  fmtnodvds  47532  2pwp1prm  47577  lighneallem2  47594  nn0oALTV  47684  nneven  47686  nnsum4primes4  47777  nnsum4primesprm  47779  nnsum4primesgbe  47781  nnsum4primesle9  47783  bgoldbachlt  47801  tgoldbach  47805  gpgusgralem  48044  gpgedgvtx0  48049  gpg3kgrtriexlem1  48071  gpg3kgrtriexlem2  48072  gpg3kgrtriexlem3  48073  gpg3kgrtriexlem4  48074  gpg3kgrtriexlem6  48076  altgsumbcALT  48341  nnlog2ge0lt1  48555  logbpw2m1  48556  blennn  48564  blennnelnn  48565  nnpw2pmod  48572  nnolog2flm1  48579  digvalnn0  48588  dignn0fr  48590  dignn0ldlem  48591  dignnld  48592  dig2nn1st  48594