Theorem nnre 8527

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

Syntax hints:   → wi 4   ∈ wcel 1445  ℝcr 7446  ℕcn 8520

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-cnex 7533  ax-resscn 7534  ax-1re 7536  ax-addrcl 7539

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-v 2635  df-in 3019  df-ss 3026  df-int 3711  df-inn 8521

This theorem is referenced by:  nnrei  8529  peano2nn  8532  nn1suc  8539  nnge1  8543  nnle1eq1  8544  nngt0  8545  nnnlt1  8546  nnap0  8549  nn2ge  8553  nn1gt1  8554  nndivre  8556  nnrecgt0  8558  nnsub  8559  arch  8768  nnrecl  8769  bndndx  8770  nn0ge0  8796  0mnnnnn0  8803  nnnegz  8851  elnnz  8858  elz2  8916  gtndiv  8940  prime  8944  btwnz  8964  qre  9209  nnrp  9242  nnledivrp  9336  fzo1fzo0n0  9743  elfzo0le  9745  fzonmapblen  9747  ubmelfzo  9760  fzonn0p1p1  9773  elfzom1p1elfzo  9774  ubmelm1fzo  9786  subfzo0  9802  adddivflid  9848  flltdivnn0lt  9860  intfracq  9876  flqdiv  9877  m1modnnsub1  9926  addmodid  9928  modfzo0difsn  9951  nnlesq  10173  facndiv  10262  faclbnd  10264  faclbnd3  10266  bcval5  10286  seq3coll  10362  caucvgre  10529  efaddlem  11113  nndivdvds  11229  nno  11333  nnoddm1d2  11337  divalglemnn  11345  divalg2  11353  ndvdsadd  11358  gcdmultiple  11436  gcdmultiplez  11437  gcdzeq  11438  sqgcd  11445  dvdssqlem  11446  lcmgcdlem  11486  coprmgcdb  11497  qredeq  11505  qredeu  11506  prmdvdsfz  11547  sqrt2irr  11568  divdenle  11602  phibndlem  11619  hashgcdlem  11630  oddennn  11632