ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnre GIF version

Theorem nnre 7997
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
Assertion
Ref Expression
nnre (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Proof of Theorem nnre
StepHypRef Expression
1 nnssre 7994 . 2 ℕ ⊆ ℝ
21sseli 2969 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  cr 6946  cn 7990
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903  ax-cnex 7033  ax-resscn 7034  ax-1re 7036  ax-addrcl 7039
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-v 2576  df-in 2952  df-ss 2959  df-int 3644  df-inn 7991
This theorem is referenced by:  nnrei  7999  peano2nn  8002  nn1suc  8009  nnge1  8013  nnle1eq1  8014  nngt0  8015  nnnlt1  8016  nnap0  8019  nn2ge  8022  nn1gt1  8023  nndivre  8025  nnrecgt0  8027  nnsub  8028  arch  8236  nnrecl  8237  bndndx  8238  nn0ge0  8264  0mnnnnn0  8271  nnnegz  8305  elnnz  8312  elz2  8370  gtndiv  8393  prime  8396  btwnz  8416  qre  8657  nnrp  8690  nnledivrp  8784  fzo1fzo0n0  9141  elfzo0le  9143  fzonmapblen  9145  ubmelfzo  9158  fzonn0p1p1  9171  elfzom1p1elfzo  9172  ubmelm1fzo  9184  subfzo0  9199  adddivflid  9242  flltdivnn0lt  9254  intfracq  9270  flqdiv  9271  m1modnnsub1  9320  addmodid  9322  modfzo0difsn  9345  nnlesq  9522  facndiv  9607  faclbnd  9609  faclbnd3  9611  ibcval5  9631  caucvgre  9808  nndivdvds  10114  nno  10218  nnoddm1d2  10222  divalglemnn  10230  divalg2  10238  ndvdsadd  10243  sqrt2irr  10251
  Copyright terms: Public domain W3C validator