Theorem nnre 9042

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

Syntax hints:   → wi 4   ∈ wcel 2175  ℝcr 7923  ℕcn 9035

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-sep 4161  ax-cnex 8015  ax-resscn 8016  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-v 2773  df-in 3171  df-ss 3178  df-int 3885  df-inn 9036

This theorem is referenced by:  nnrei  9044  peano2nn  9047  nn1suc  9054  nnge1  9058  nnle1eq1  9059  nngt0  9060  nnnlt1  9061  nnap0  9064  nn2ge  9068  nn1gt1  9069  nndivre  9071  nnrecgt0  9073  nnsub  9074  arch  9291  nnrecl  9292  bndndx  9293  nn0ge0  9319  0mnnnnn0  9326  nnnegz  9374  elnnz  9381  elz2  9443  gtndiv  9467  prime  9471  btwnz  9491  qre  9745  elpq  9769  elpqb  9770  nnrp  9784  nnledivrp  9887  fzo1fzo0n0  10305  elfzo0le  10307  fzonmapblen  10309  ubmelfzo  10327  fzonn0p1p1  10340  elfzom1p1elfzo  10341  ubmelm1fzo  10353  subfzo0  10369  adddivflid  10433  flltdivnn0lt  10445  intfracq  10463  flqdiv  10464  m1modnnsub1  10513  addmodid  10515  modfzo0difsn  10538  nnlesq  10786  facndiv  10882  faclbnd  10884  faclbnd3  10886  bcval5  10906  seq3coll  10985  ccatval21sw  11059  caucvgre  11263  efaddlem  11956  nndivdvds  12078  nno  12188  nnoddm1d2  12192  divalglemnn  12200  divalg2  12208  ndvdsadd  12213  gcdmultiple  12312  gcdmultiplez  12313  gcdzeq  12314  sqgcd  12321  dvdssqlem  12322  lcmgcdlem  12370  coprmgcdb  12381  qredeq  12389  qredeu  12390  prmdvdsfz  12432  sqrt2irr  12455  divdenle  12490  phibndlem  12509  hashgcdlem  12531  oddprm  12553  pythagtriplem10  12563  pythagtriplem12  12569  pythagtriplem14  12571  pythagtriplem16  12573  pythagtriplem19  12576  pclemub  12581  pc2dvds  12624  pcmpt  12637  fldivp1  12642  pcbc  12645  infpnlem1  12653  oddennn  12734  exmidunben  12768  mulgnegnn  13439  znidomb  14391  lgsval4a  15470  gausslemma2dlem0c  15499  gausslemma2dlem0d  15500  gausslemma2dlem1a  15506  gausslemma2dlem2  15510  gausslemma2dlem3  15511  lgsquadlem1  15525  lgsquadlem2  15526  2lgslem1a1  15534