Theorem nnre 9149

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8030  ℕcn 9142

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 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128

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 9143

This theorem is referenced by:  nnrei  9151  peano2nn  9154  nn1suc  9161  nnge1  9165  nnle1eq1  9166  nngt0  9167  nnnlt1  9168  nnap0  9171  nn2ge  9175  nn1gt1  9176  nndivre  9178  nnrecgt0  9180  nnsub  9181  arch  9398  nnrecl  9399  bndndx  9400  nn0ge0  9426  0mnnnnn0  9433  nnnegz  9481  elnnz  9488  elz2  9550  gtndiv  9574  prime  9578  btwnz  9598  qre  9858  elpq  9882  elpqb  9883  nnrp  9897  nnledivrp  10000  fzo1fzo0n0  10421  elfzo0le  10423  fzonmapblen  10425  ubmelfzo  10444  fzonn0p1p1  10457  elfzom1p1elfzo  10458  ubmelm1fzo  10470  subfzo0  10487  adddivflid  10551  flltdivnn0lt  10563  intfracq  10581  flqdiv  10582  m1modnnsub1  10631  addmodid  10633  modfzo0difsn  10656  nnlesq  10904  facndiv  11000  faclbnd  11002  faclbnd3  11004  bcval5  11024  seq3coll  11105  ccatval21sw  11181  caucvgre  11541  efaddlem  12234  nndivdvds  12356  nno  12466  nnoddm1d2  12470  divalglemnn  12478  divalg2  12486  ndvdsadd  12491  gcdmultiple  12590  gcdmultiplez  12591  gcdzeq  12592  sqgcd  12599  dvdssqlem  12600  lcmgcdlem  12648  coprmgcdb  12659  qredeq  12667  qredeu  12668  prmdvdsfz  12710  sqrt2irr  12733  divdenle  12768  phibndlem  12787  hashgcdlem  12809  oddprm  12831  pythagtriplem10  12841  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem16  12851  pythagtriplem19  12854  pclemub  12859  pc2dvds  12902  pcmpt  12915  fldivp1  12920  pcbc  12923  infpnlem1  12931  oddennn  13012  exmidunben  13046  mulgnegnn  13718  znidomb  14671  lgsval4a  15750  gausslemma2dlem0c  15779  gausslemma2dlem0d  15780  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  gausslemma2dlem3  15791  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem1a1  15814