Theorem nnre 9261

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8142  ℕcn 9254

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3220  df-ss 3227  df-int 3955  df-inn 9255

This theorem is referenced by:  nnrei  9263  peano2nn  9266  nn1suc  9273  nnge1  9277  nnle1eq1  9278  nngt0  9279  nnnlt1  9280  nnap0  9283  nn2ge  9287  nn1gt1  9288  nndivre  9290  nnrecgt0  9292  nnsub  9293  arch  9510  nnrecl  9511  bndndx  9512  nn0ge0  9538  0mnnnnn0  9545  nnnegz  9597  elnnz  9604  elz2  9666  gtndiv  9691  prime  9695  btwnz  9715  qre  9975  elpq  9999  elpqb  10000  nnrp  10014  nnledivrp  10117  fzo1fzo0n0  10544  elfzo0le  10546  fzonmapblen  10548  ubmelfzo  10567  fzonn0p1p1  10580  elfzom1p1elfzo  10581  ubmelm1fzo  10593  subfzo0  10610  adddivflid  10676  flltdivnn0lt  10688  intfracq  10706  flqdiv  10707  m1modnnsub1  10756  addmodid  10758  modfzo0difsn  10781  nnlesq  11029  facndiv  11126  faclbnd  11128  faclbnd3  11130  bcval5  11150  seq3coll  11239  ccatval21sw  11318  caucvgre  11691  efaddlem  12385  nndivdvds  12507  nno  12617  nnoddm1d2  12621  divalglemnn  12629  divalg2  12637  ndvdsadd  12642  gcdmultiple  12741  gcdmultiplez  12742  gcdzeq  12743  sqgcd  12750  dvdssqlem  12751  lcmgcdlem  12799  coprmgcdb  12810  qredeq  12818  qredeu  12819  prmdvdsfz  12861  sqrt2irr  12884  divdenle  12919  phibndlem  12938  hashgcdlem  12960  oddprm  12982  pythagtriplem10  12992  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem16  13002  pythagtriplem19  13005  pclemub  13010  pc2dvds  13053  pcmpt  13066  fldivp1  13071  pcbc  13074  infpnlem1  13082  ballotfilemonn  13165  oddennn  13227  exmidunben  13261  mulgnegnn  13885  znidomb  14932  pellexlem1  15971  lgsval4a  16021  gausslemma2dlem0c  16050  gausslemma2dlem0d  16051  gausslemma2dlem1a  16057  gausslemma2dlem2  16061  gausslemma2dlem3  16062  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem1a1  16085