Theorem nnre 9140

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8021  ℕcn 9133

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 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119

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 3927  df-inn 9134

This theorem is referenced by:  nnrei  9142  peano2nn  9145  nn1suc  9152  nnge1  9156  nnle1eq1  9157  nngt0  9158  nnnlt1  9159  nnap0  9162  nn2ge  9166  nn1gt1  9167  nndivre  9169  nnrecgt0  9171  nnsub  9172  arch  9389  nnrecl  9390  bndndx  9391  nn0ge0  9417  0mnnnnn0  9424  nnnegz  9472  elnnz  9479  elz2  9541  gtndiv  9565  prime  9569  btwnz  9589  qre  9849  elpq  9873  elpqb  9874  nnrp  9888  nnledivrp  9991  fzo1fzo0n0  10412  elfzo0le  10414  fzonmapblen  10416  ubmelfzo  10435  fzonn0p1p1  10448  elfzom1p1elfzo  10449  ubmelm1fzo  10461  subfzo0  10478  adddivflid  10542  flltdivnn0lt  10554  intfracq  10572  flqdiv  10573  m1modnnsub1  10622  addmodid  10624  modfzo0difsn  10647  nnlesq  10895  facndiv  10991  faclbnd  10993  faclbnd3  10995  bcval5  11015  seq3coll  11096  ccatval21sw  11172  caucvgre  11532  efaddlem  12225  nndivdvds  12347  nno  12457  nnoddm1d2  12461  divalglemnn  12469  divalg2  12477  ndvdsadd  12482  gcdmultiple  12581  gcdmultiplez  12582  gcdzeq  12583  sqgcd  12590  dvdssqlem  12591  lcmgcdlem  12639  coprmgcdb  12650  qredeq  12658  qredeu  12659  prmdvdsfz  12701  sqrt2irr  12724  divdenle  12759  phibndlem  12778  hashgcdlem  12800  oddprm  12822  pythagtriplem10  12832  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem16  12842  pythagtriplem19  12845  pclemub  12850  pc2dvds  12893  pcmpt  12906  fldivp1  12911  pcbc  12914  infpnlem1  12922  oddennn  13003  exmidunben  13037  mulgnegnn  13709  znidomb  14662  lgsval4a  15741  gausslemma2dlem0c  15770  gausslemma2dlem0d  15771  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  gausslemma2dlem3  15782  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem1a1  15805