Theorem nnre 7921

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

Syntax hints:   → wi 4   ∈ wcel 1393  ℝcr 6888  ℕcn 7914

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-cnex 6975  ax-resscn 6976  ax-1re 6978  ax-addrcl 6981

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-v 2559  df-in 2924  df-ss 2931  df-int 3616  df-inn 7915

This theorem is referenced by:  nnrei  7923  peano2nn  7926  nn1suc  7933  nnge1  7937  nnle1eq1  7938  nngt0  7939  nnnlt1  7940  nnap0  7943  nn2ge  7946  nn1gt1  7947  nndivre  7949  nnrecgt0  7951  nnsub  7952  arch  8178  nnrecl  8179  bndndx  8180  nn0ge0  8207  0mnnnnn0  8214  nnnegz  8248  elnnz  8255  elz2  8312  gtndiv  8335  prime  8337  btwnz  8357  qre  8560  nnrp  8592  fzo1fzo0n0  9039  elfzo0le  9041  fzonmapblen  9043  ubmelfzo  9056  fzonn0p1p1  9069  elfzom1p1elfzo  9070  ubmelm1fzo  9082  subfzo0  9097  adddivflid  9134  flltdivnn0lt  9146  intfracq  9162  flqdiv  9163  nnlesq  9356  caucvgre  9580  sqrt2irr  9878