Theorem nnre 9016

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℝcr 7897  ℕcn 9009

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7989  ax-resscn 7990  ax-1re 7992  ax-addrcl 7995

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-in 3163  df-ss 3170  df-int 3876  df-inn 9010

This theorem is referenced by:  nnrei  9018  peano2nn  9021  nn1suc  9028  nnge1  9032  nnle1eq1  9033  nngt0  9034  nnnlt1  9035  nnap0  9038  nn2ge  9042  nn1gt1  9043  nndivre  9045  nnrecgt0  9047  nnsub  9048  arch  9265  nnrecl  9266  bndndx  9267  nn0ge0  9293  0mnnnnn0  9300  nnnegz  9348  elnnz  9355  elz2  9416  gtndiv  9440  prime  9444  btwnz  9464  qre  9718  elpq  9742  elpqb  9743  nnrp  9757  nnledivrp  9860  fzo1fzo0n0  10278  elfzo0le  10280  fzonmapblen  10282  ubmelfzo  10295  fzonn0p1p1  10308  elfzom1p1elfzo  10309  ubmelm1fzo  10321  subfzo0  10337  adddivflid  10401  flltdivnn0lt  10413  intfracq  10431  flqdiv  10432  m1modnnsub1  10481  addmodid  10483  modfzo0difsn  10506  nnlesq  10754  facndiv  10850  faclbnd  10852  faclbnd3  10854  bcval5  10874  seq3coll  10953  caucvgre  11165  efaddlem  11858  nndivdvds  11980  nno  12090  nnoddm1d2  12094  divalglemnn  12102  divalg2  12110  ndvdsadd  12115  gcdmultiple  12214  gcdmultiplez  12215  gcdzeq  12216  sqgcd  12223  dvdssqlem  12224  lcmgcdlem  12272  coprmgcdb  12283  qredeq  12291  qredeu  12292  prmdvdsfz  12334  sqrt2irr  12357  divdenle  12392  phibndlem  12411  hashgcdlem  12433  oddprm  12455  pythagtriplem10  12465  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem16  12475  pythagtriplem19  12478  pclemub  12483  pc2dvds  12526  pcmpt  12539  fldivp1  12544  pcbc  12547  infpnlem1  12555  oddennn  12636  exmidunben  12670  mulgnegnn  13340  znidomb  14292  lgsval4a  15371  gausslemma2dlem0c  15400  gausslemma2dlem0d  15401  gausslemma2dlem1a  15407  gausslemma2dlem2  15411  gausslemma2dlem3  15412  lgsquadlem1  15426  lgsquadlem2  15427  2lgslem1a1  15435