Theorem nnre 9244

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8126  ℕcn 9237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4228  ax-cnex 8218  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815  df-in 3217  df-ss 3224  df-int 3950  df-inn 9238

This theorem is referenced by:  nnrei  9246  peano2nn  9249  nn1suc  9256  nnge1  9260  nnle1eq1  9261  nngt0  9262  nnnlt1  9263  nnap0  9266  nn2ge  9270  nn1gt1  9271  nndivre  9273  nnrecgt0  9275  nnsub  9276  arch  9493  nnrecl  9494  bndndx  9495  nn0ge0  9521  0mnnnnn0  9528  nnnegz  9580  elnnz  9587  elz2  9649  gtndiv  9673  prime  9677  btwnz  9697  qre  9957  elpq  9981  elpqb  9982  nnrp  9996  nnledivrp  10099  fzo1fzo0n0  10522  elfzo0le  10524  fzonmapblen  10526  ubmelfzo  10545  fzonn0p1p1  10558  elfzom1p1elfzo  10559  ubmelm1fzo  10571  subfzo0  10588  adddivflid  10652  flltdivnn0lt  10664  intfracq  10682  flqdiv  10683  m1modnnsub1  10732  addmodid  10734  modfzo0difsn  10757  nnlesq  11005  facndiv  11101  faclbnd  11103  faclbnd3  11105  bcval5  11125  seq3coll  11214  ccatval21sw  11293  caucvgre  11666  efaddlem  12360  nndivdvds  12482  nno  12592  nnoddm1d2  12596  divalglemnn  12604  divalg2  12612  ndvdsadd  12617  gcdmultiple  12716  gcdmultiplez  12717  gcdzeq  12718  sqgcd  12725  dvdssqlem  12726  lcmgcdlem  12774  coprmgcdb  12785  qredeq  12793  qredeu  12794  prmdvdsfz  12836  sqrt2irr  12859  divdenle  12894  phibndlem  12913  hashgcdlem  12935  oddprm  12957  pythagtriplem10  12967  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem16  12977  pythagtriplem19  12980  pclemub  12985  pc2dvds  13028  pcmpt  13041  fldivp1  13046  pcbc  13049  infpnlem1  13057  ballotfilemonn  13140  oddennn  13143  exmidunben  13177  mulgnegnn  13849  znidomb  14806  pellexlem1  15845  lgsval4a  15895  gausslemma2dlem0c  15924  gausslemma2dlem0d  15925  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  gausslemma2dlem3  15936  lgsquadlem1  15950  lgsquadlem2  15951  2lgslem1a1  15959