Theorem nnre 9128

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8009  ℕcn 9121

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 4202  ax-cnex 8101  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107

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 2801  df-in 3203  df-ss 3210  df-int 3924  df-inn 9122

This theorem is referenced by:  nnrei  9130  peano2nn  9133  nn1suc  9140  nnge1  9144  nnle1eq1  9145  nngt0  9146  nnnlt1  9147  nnap0  9150  nn2ge  9154  nn1gt1  9155  nndivre  9157  nnrecgt0  9159  nnsub  9160  arch  9377  nnrecl  9378  bndndx  9379  nn0ge0  9405  0mnnnnn0  9412  nnnegz  9460  elnnz  9467  elz2  9529  gtndiv  9553  prime  9557  btwnz  9577  qre  9832  elpq  9856  elpqb  9857  nnrp  9871  nnledivrp  9974  fzo1fzo0n0  10395  elfzo0le  10397  fzonmapblen  10399  ubmelfzo  10418  fzonn0p1p1  10431  elfzom1p1elfzo  10432  ubmelm1fzo  10444  subfzo0  10460  adddivflid  10524  flltdivnn0lt  10536  intfracq  10554  flqdiv  10555  m1modnnsub1  10604  addmodid  10606  modfzo0difsn  10629  nnlesq  10877  facndiv  10973  faclbnd  10975  faclbnd3  10977  bcval5  10997  seq3coll  11077  ccatval21sw  11153  caucvgre  11507  efaddlem  12200  nndivdvds  12322  nno  12432  nnoddm1d2  12436  divalglemnn  12444  divalg2  12452  ndvdsadd  12457  gcdmultiple  12556  gcdmultiplez  12557  gcdzeq  12558  sqgcd  12565  dvdssqlem  12566  lcmgcdlem  12614  coprmgcdb  12625  qredeq  12633  qredeu  12634  prmdvdsfz  12676  sqrt2irr  12699  divdenle  12734  phibndlem  12753  hashgcdlem  12775  oddprm  12797  pythagtriplem10  12807  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem16  12817  pythagtriplem19  12820  pclemub  12825  pc2dvds  12868  pcmpt  12881  fldivp1  12886  pcbc  12889  infpnlem1  12897  oddennn  12978  exmidunben  13012  mulgnegnn  13684  znidomb  14637  lgsval4a  15716  gausslemma2dlem0c  15745  gausslemma2dlem0d  15746  gausslemma2dlem1a  15752  gausslemma2dlem2  15756  gausslemma2dlem3  15757  lgsquadlem1  15771  lgsquadlem2  15772  2lgslem1a1  15780