Theorem nnre 9150

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8031  ℕcn 9143

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-inn 9144

This theorem is referenced by:  nnrei  9152  peano2nn  9155  nn1suc  9162  nnge1  9166  nnle1eq1  9167  nngt0  9168  nnnlt1  9169  nnap0  9172  nn2ge  9176  nn1gt1  9177  nndivre  9179  nnrecgt0  9181  nnsub  9182  arch  9399  nnrecl  9400  bndndx  9401  nn0ge0  9427  0mnnnnn0  9434  nnnegz  9482  elnnz  9489  elz2  9551  gtndiv  9575  prime  9579  btwnz  9599  qre  9859  elpq  9883  elpqb  9884  nnrp  9898  nnledivrp  10001  fzo1fzo0n0  10423  elfzo0le  10425  fzonmapblen  10427  ubmelfzo  10446  fzonn0p1p1  10459  elfzom1p1elfzo  10460  ubmelm1fzo  10472  subfzo0  10489  adddivflid  10553  flltdivnn0lt  10565  intfracq  10583  flqdiv  10584  m1modnnsub1  10633  addmodid  10635  modfzo0difsn  10658  nnlesq  10906  facndiv  11002  faclbnd  11004  faclbnd3  11006  bcval5  11026  seq3coll  11107  ccatval21sw  11186  caucvgre  11546  efaddlem  12240  nndivdvds  12362  nno  12472  nnoddm1d2  12476  divalglemnn  12484  divalg2  12492  ndvdsadd  12497  gcdmultiple  12596  gcdmultiplez  12597  gcdzeq  12598  sqgcd  12605  dvdssqlem  12606  lcmgcdlem  12654  coprmgcdb  12665  qredeq  12673  qredeu  12674  prmdvdsfz  12716  sqrt2irr  12739  divdenle  12774  phibndlem  12793  hashgcdlem  12815  oddprm  12837  pythagtriplem10  12847  pythagtriplem12  12853  pythagtriplem14  12855  pythagtriplem16  12857  pythagtriplem19  12860  pclemub  12865  pc2dvds  12908  pcmpt  12921  fldivp1  12926  pcbc  12929  infpnlem1  12937  oddennn  13018  exmidunben  13052  mulgnegnn  13724  znidomb  14678  lgsval4a  15757  gausslemma2dlem0c  15786  gausslemma2dlem0d  15787  gausslemma2dlem1a  15793  gausslemma2dlem2  15797  gausslemma2dlem3  15798  lgsquadlem1  15812  lgsquadlem2  15813  2lgslem1a1  15821