Theorem nnre 9138

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8019  ℕcn 9131

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4203  ax-cnex 8111  ax-resscn 8112  ax-1re 8114  ax-addrcl 8117

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-in 3204  df-ss 3211  df-int 3925  df-inn 9132

This theorem is referenced by:  nnrei  9140  peano2nn  9143  nn1suc  9150  nnge1  9154  nnle1eq1  9155  nngt0  9156  nnnlt1  9157  nnap0  9160  nn2ge  9164  nn1gt1  9165  nndivre  9167  nnrecgt0  9169  nnsub  9170  arch  9387  nnrecl  9388  bndndx  9389  nn0ge0  9415  0mnnnnn0  9422  nnnegz  9470  elnnz  9477  elz2  9539  gtndiv  9563  prime  9567  btwnz  9587  qre  9847  elpq  9871  elpqb  9872  nnrp  9886  nnledivrp  9989  fzo1fzo0n0  10410  elfzo0le  10412  fzonmapblen  10414  ubmelfzo  10433  fzonn0p1p1  10446  elfzom1p1elfzo  10447  ubmelm1fzo  10459  subfzo0  10476  adddivflid  10540  flltdivnn0lt  10552  intfracq  10570  flqdiv  10571  m1modnnsub1  10620  addmodid  10622  modfzo0difsn  10645  nnlesq  10893  facndiv  10989  faclbnd  10991  faclbnd3  10993  bcval5  11013  seq3coll  11093  ccatval21sw  11169  caucvgre  11529  efaddlem  12222  nndivdvds  12344  nno  12454  nnoddm1d2  12458  divalglemnn  12466  divalg2  12474  ndvdsadd  12479  gcdmultiple  12578  gcdmultiplez  12579  gcdzeq  12580  sqgcd  12587  dvdssqlem  12588  lcmgcdlem  12636  coprmgcdb  12647  qredeq  12655  qredeu  12656  prmdvdsfz  12698  sqrt2irr  12721  divdenle  12756  phibndlem  12775  hashgcdlem  12797  oddprm  12819  pythagtriplem10  12829  pythagtriplem12  12835  pythagtriplem14  12837  pythagtriplem16  12839  pythagtriplem19  12842  pclemub  12847  pc2dvds  12890  pcmpt  12903  fldivp1  12908  pcbc  12911  infpnlem1  12919  oddennn  13000  exmidunben  13034  mulgnegnn  13706  znidomb  14659  lgsval4a  15738  gausslemma2dlem0c  15767  gausslemma2dlem0d  15768  gausslemma2dlem1a  15774  gausslemma2dlem2  15778  gausslemma2dlem3  15779  lgsquadlem1  15793  lgsquadlem2  15794  2lgslem1a1  15802