Theorem nnre 8920

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7805  ℕcn 8913

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4119  ax-cnex 7897  ax-resscn 7898  ax-1re 7900  ax-addrcl 7903

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2739  df-in 3135  df-ss 3142  df-int 3844  df-inn 8914

This theorem is referenced by:  nnrei  8922  peano2nn  8925  nn1suc  8932  nnge1  8936  nnle1eq1  8937  nngt0  8938  nnnlt1  8939  nnap0  8942  nn2ge  8946  nn1gt1  8947  nndivre  8949  nnrecgt0  8951  nnsub  8952  arch  9167  nnrecl  9168  bndndx  9169  nn0ge0  9195  0mnnnnn0  9202  nnnegz  9250  elnnz  9257  elz2  9318  gtndiv  9342  prime  9346  btwnz  9366  qre  9619  elpq  9642  elpqb  9643  nnrp  9657  nnledivrp  9760  fzo1fzo0n0  10176  elfzo0le  10178  fzonmapblen  10180  ubmelfzo  10193  fzonn0p1p1  10206  elfzom1p1elfzo  10207  ubmelm1fzo  10219  subfzo0  10235  adddivflid  10285  flltdivnn0lt  10297  intfracq  10313  flqdiv  10314  m1modnnsub1  10363  addmodid  10365  modfzo0difsn  10388  nnlesq  10616  facndiv  10710  faclbnd  10712  faclbnd3  10714  bcval5  10734  seq3coll  10813  caucvgre  10981  efaddlem  11673  nndivdvds  11794  nno  11901  nnoddm1d2  11905  divalglemnn  11913  divalg2  11921  ndvdsadd  11926  gcdmultiple  12011  gcdmultiplez  12012  gcdzeq  12013  sqgcd  12020  dvdssqlem  12021  lcmgcdlem  12067  coprmgcdb  12078  qredeq  12086  qredeu  12087  prmdvdsfz  12129  sqrt2irr  12152  divdenle  12187  phibndlem  12206  hashgcdlem  12228  oddprm  12249  pythagtriplem10  12259  pythagtriplem12  12265  pythagtriplem14  12267  pythagtriplem16  12269  pythagtriplem19  12272  pclemub  12277  pc2dvds  12319  pcmpt  12331  fldivp1  12336  pcbc  12339  infpnlem1  12347  oddennn  12383  exmidunben  12417  mulgnegnn  12921  lgsval4a  14205