Theorem nnre 8840

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

Syntax hints:   → wi 4   ∈ wcel 2128  ℝcr 7731  ℕcn 8833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-sep 4082  ax-cnex 7823  ax-resscn 7824  ax-1re 7826  ax-addrcl 7829

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-v 2714  df-in 3108  df-ss 3115  df-int 3808  df-inn 8834

This theorem is referenced by:  nnrei  8842  peano2nn  8845  nn1suc  8852  nnge1  8856  nnle1eq1  8857  nngt0  8858  nnnlt1  8859  nnap0  8862  nn2ge  8866  nn1gt1  8867  nndivre  8869  nnrecgt0  8871  nnsub  8872  arch  9087  nnrecl  9088  bndndx  9089  nn0ge0  9115  0mnnnnn0  9122  nnnegz  9170  elnnz  9177  elz2  9235  gtndiv  9259  prime  9263  btwnz  9283  qre  9534  elpq  9557  elpqb  9558  nnrp  9570  nnledivrp  9673  fzo1fzo0n0  10082  elfzo0le  10084  fzonmapblen  10086  ubmelfzo  10099  fzonn0p1p1  10112  elfzom1p1elfzo  10113  ubmelm1fzo  10125  subfzo0  10141  adddivflid  10191  flltdivnn0lt  10203  intfracq  10219  flqdiv  10220  m1modnnsub1  10269  addmodid  10271  modfzo0difsn  10294  nnlesq  10522  facndiv  10613  faclbnd  10615  faclbnd3  10617  bcval5  10637  seq3coll  10713  caucvgre  10881  efaddlem  11571  nndivdvds  11692  nno  11797  nnoddm1d2  11801  divalglemnn  11809  divalg2  11817  ndvdsadd  11822  gcdmultiple  11904  gcdmultiplez  11905  gcdzeq  11906  sqgcd  11913  dvdssqlem  11914  lcmgcdlem  11954  coprmgcdb  11965  qredeq  11973  qredeu  11974  prmdvdsfz  12016  sqrt2irr  12037  divdenle  12072  phibndlem  12091  hashgcdlem  12113  oddennn  12132  exmidunben  12166