Theorem nnre 8926

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7810  ℕcn 8919

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 4122  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908

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 2740  df-in 3136  df-ss 3143  df-int 3846  df-inn 8920

This theorem is referenced by:  nnrei  8928  peano2nn  8931  nn1suc  8938  nnge1  8942  nnle1eq1  8943  nngt0  8944  nnnlt1  8945  nnap0  8948  nn2ge  8952  nn1gt1  8953  nndivre  8955  nnrecgt0  8957  nnsub  8958  arch  9173  nnrecl  9174  bndndx  9175  nn0ge0  9201  0mnnnnn0  9208  nnnegz  9256  elnnz  9263  elz2  9324  gtndiv  9348  prime  9352  btwnz  9372  qre  9625  elpq  9648  elpqb  9649  nnrp  9663  nnledivrp  9766  fzo1fzo0n0  10183  elfzo0le  10185  fzonmapblen  10187  ubmelfzo  10200  fzonn0p1p1  10213  elfzom1p1elfzo  10214  ubmelm1fzo  10226  subfzo0  10242  adddivflid  10292  flltdivnn0lt  10304  intfracq  10320  flqdiv  10321  m1modnnsub1  10370  addmodid  10372  modfzo0difsn  10395  nnlesq  10624  facndiv  10719  faclbnd  10721  faclbnd3  10723  bcval5  10743  seq3coll  10822  caucvgre  10990  efaddlem  11682  nndivdvds  11803  nno  11911  nnoddm1d2  11915  divalglemnn  11923  divalg2  11931  ndvdsadd  11936  gcdmultiple  12021  gcdmultiplez  12022  gcdzeq  12023  sqgcd  12030  dvdssqlem  12031  lcmgcdlem  12077  coprmgcdb  12088  qredeq  12096  qredeu  12097  prmdvdsfz  12139  sqrt2irr  12162  divdenle  12197  phibndlem  12216  hashgcdlem  12238  oddprm  12259  pythagtriplem10  12269  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  pythagtriplem19  12282  pclemub  12287  pc2dvds  12329  pcmpt  12341  fldivp1  12346  pcbc  12349  infpnlem1  12357  oddennn  12393  exmidunben  12427  mulgnegnn  12993  lgsval4a  14426