Theorem nnre 8922

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7807  ℕcn 8915

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 4120  ax-cnex 7899  ax-resscn 7900  ax-1re 7902  ax-addrcl 7905

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 3845  df-inn 8916

This theorem is referenced by:  nnrei  8924  peano2nn  8927  nn1suc  8934  nnge1  8938  nnle1eq1  8939  nngt0  8940  nnnlt1  8941  nnap0  8944  nn2ge  8948  nn1gt1  8949  nndivre  8951  nnrecgt0  8953  nnsub  8954  arch  9169  nnrecl  9170  bndndx  9171  nn0ge0  9197  0mnnnnn0  9204  nnnegz  9252  elnnz  9259  elz2  9320  gtndiv  9344  prime  9348  btwnz  9368  qre  9621  elpq  9644  elpqb  9645  nnrp  9659  nnledivrp  9762  fzo1fzo0n0  10178  elfzo0le  10180  fzonmapblen  10182  ubmelfzo  10195  fzonn0p1p1  10208  elfzom1p1elfzo  10209  ubmelm1fzo  10221  subfzo0  10237  adddivflid  10287  flltdivnn0lt  10299  intfracq  10315  flqdiv  10316  m1modnnsub1  10365  addmodid  10367  modfzo0difsn  10390  nnlesq  10618  facndiv  10712  faclbnd  10714  faclbnd3  10716  bcval5  10736  seq3coll  10815  caucvgre  10983  efaddlem  11675  nndivdvds  11796  nno  11903  nnoddm1d2  11907  divalglemnn  11915  divalg2  11923  ndvdsadd  11928  gcdmultiple  12013  gcdmultiplez  12014  gcdzeq  12015  sqgcd  12022  dvdssqlem  12023  lcmgcdlem  12069  coprmgcdb  12080  qredeq  12088  qredeu  12089  prmdvdsfz  12131  sqrt2irr  12154  divdenle  12189  phibndlem  12208  hashgcdlem  12230  oddprm  12251  pythagtriplem10  12261  pythagtriplem12  12267  pythagtriplem14  12269  pythagtriplem16  12271  pythagtriplem19  12274  pclemub  12279  pc2dvds  12321  pcmpt  12333  fldivp1  12338  pcbc  12341  infpnlem1  12349  oddennn  12385  exmidunben  12419  mulgnegnn  12925  lgsval4a  14294