Theorem nnre 9113

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 7994  ℕcn 9106

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 4201  ax-cnex 8086  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092

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 3923  df-inn 9107

This theorem is referenced by:  nnrei  9115  peano2nn  9118  nn1suc  9125  nnge1  9129  nnle1eq1  9130  nngt0  9131  nnnlt1  9132  nnap0  9135  nn2ge  9139  nn1gt1  9140  nndivre  9142  nnrecgt0  9144  nnsub  9145  arch  9362  nnrecl  9363  bndndx  9364  nn0ge0  9390  0mnnnnn0  9397  nnnegz  9445  elnnz  9452  elz2  9514  gtndiv  9538  prime  9542  btwnz  9562  qre  9816  elpq  9840  elpqb  9841  nnrp  9855  nnledivrp  9958  fzo1fzo0n0  10379  elfzo0le  10381  fzonmapblen  10383  ubmelfzo  10401  fzonn0p1p1  10414  elfzom1p1elfzo  10415  ubmelm1fzo  10427  subfzo0  10443  adddivflid  10507  flltdivnn0lt  10519  intfracq  10537  flqdiv  10538  m1modnnsub1  10587  addmodid  10589  modfzo0difsn  10612  nnlesq  10860  facndiv  10956  faclbnd  10958  faclbnd3  10960  bcval5  10980  seq3coll  11059  ccatval21sw  11135  caucvgre  11487  efaddlem  12180  nndivdvds  12302  nno  12412  nnoddm1d2  12416  divalglemnn  12424  divalg2  12432  ndvdsadd  12437  gcdmultiple  12536  gcdmultiplez  12537  gcdzeq  12538  sqgcd  12545  dvdssqlem  12546  lcmgcdlem  12594  coprmgcdb  12605  qredeq  12613  qredeu  12614  prmdvdsfz  12656  sqrt2irr  12679  divdenle  12714  phibndlem  12733  hashgcdlem  12755  oddprm  12777  pythagtriplem10  12787  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem16  12797  pythagtriplem19  12800  pclemub  12805  pc2dvds  12848  pcmpt  12861  fldivp1  12866  pcbc  12869  infpnlem1  12877  oddennn  12958  exmidunben  12992  mulgnegnn  13664  znidomb  14616  lgsval4a  15695  gausslemma2dlem0c  15724  gausslemma2dlem0d  15725  gausslemma2dlem1a  15731  gausslemma2dlem2  15735  gausslemma2dlem3  15736  lgsquadlem1  15750  lgsquadlem2  15751  2lgslem1a1  15759