Theorem nnre 8989

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℝcr 7871  ℕcn 8982

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762  df-in 3159  df-ss 3166  df-int 3871  df-inn 8983

This theorem is referenced by:  nnrei  8991  peano2nn  8994  nn1suc  9001  nnge1  9005  nnle1eq1  9006  nngt0  9007  nnnlt1  9008  nnap0  9011  nn2ge  9015  nn1gt1  9016  nndivre  9018  nnrecgt0  9020  nnsub  9021  arch  9237  nnrecl  9238  bndndx  9239  nn0ge0  9265  0mnnnnn0  9272  nnnegz  9320  elnnz  9327  elz2  9388  gtndiv  9412  prime  9416  btwnz  9436  qre  9690  elpq  9714  elpqb  9715  nnrp  9729  nnledivrp  9832  fzo1fzo0n0  10250  elfzo0le  10252  fzonmapblen  10254  ubmelfzo  10267  fzonn0p1p1  10280  elfzom1p1elfzo  10281  ubmelm1fzo  10293  subfzo0  10309  adddivflid  10361  flltdivnn0lt  10373  intfracq  10391  flqdiv  10392  m1modnnsub1  10441  addmodid  10443  modfzo0difsn  10466  nnlesq  10714  facndiv  10810  faclbnd  10812  faclbnd3  10814  bcval5  10834  seq3coll  10913  caucvgre  11125  efaddlem  11817  nndivdvds  11939  nno  12047  nnoddm1d2  12051  divalglemnn  12059  divalg2  12067  ndvdsadd  12072  gcdmultiple  12157  gcdmultiplez  12158  gcdzeq  12159  sqgcd  12166  dvdssqlem  12167  lcmgcdlem  12215  coprmgcdb  12226  qredeq  12234  qredeu  12235  prmdvdsfz  12277  sqrt2irr  12300  divdenle  12335  phibndlem  12354  hashgcdlem  12376  oddprm  12397  pythagtriplem10  12407  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem16  12417  pythagtriplem19  12420  pclemub  12425  pc2dvds  12468  pcmpt  12481  fldivp1  12486  pcbc  12489  infpnlem1  12497  oddennn  12549  exmidunben  12583  mulgnegnn  13202  znidomb  14146  lgsval4a  15138  gausslemma2dlem0c  15167  gausslemma2dlem0d  15168  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  gausslemma2dlem3  15179  lgsquadlem1  15191