Theorem nnre 8751

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

Syntax hints:   → wi 4   ∈ wcel 1481  ℝcr 7643  ℕcn 8744

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-cnex 7735  ax-resscn 7736  ax-1re 7738  ax-addrcl 7741

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691  df-in 3082  df-ss 3089  df-int 3780  df-inn 8745

This theorem is referenced by:  nnrei  8753  peano2nn  8756  nn1suc  8763  nnge1  8767  nnle1eq1  8768  nngt0  8769  nnnlt1  8770  nnap0  8773  nn2ge  8777  nn1gt1  8778  nndivre  8780  nnrecgt0  8782  nnsub  8783  arch  8998  nnrecl  8999  bndndx  9000  nn0ge0  9026  0mnnnnn0  9033  nnnegz  9081  elnnz  9088  elz2  9146  gtndiv  9170  prime  9174  btwnz  9194  qre  9444  elpq  9467  elpqb  9468  nnrp  9480  nnledivrp  9583  fzo1fzo0n0  9991  elfzo0le  9993  fzonmapblen  9995  ubmelfzo  10008  fzonn0p1p1  10021  elfzom1p1elfzo  10022  ubmelm1fzo  10034  subfzo0  10050  adddivflid  10096  flltdivnn0lt  10108  intfracq  10124  flqdiv  10125  m1modnnsub1  10174  addmodid  10176  modfzo0difsn  10199  nnlesq  10427  facndiv  10517  faclbnd  10519  faclbnd3  10521  bcval5  10541  seq3coll  10617  caucvgre  10785  efaddlem  11417  nndivdvds  11535  nno  11639  nnoddm1d2  11643  divalglemnn  11651  divalg2  11659  ndvdsadd  11664  gcdmultiple  11744  gcdmultiplez  11745  gcdzeq  11746  sqgcd  11753  dvdssqlem  11754  lcmgcdlem  11794  coprmgcdb  11805  qredeq  11813  qredeu  11814  prmdvdsfz  11855  sqrt2irr  11876  divdenle  11911  phibndlem  11928  hashgcdlem  11939  oddennn  11941  exmidunben  11975