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

Theorem nn0re 8615
Description: A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0re (𝐴 ∈ ℕ0𝐴 ∈ ℝ)

Proof of Theorem nn0re
StepHypRef Expression
1 nn0ssre 8610 . 2 0 ⊆ ℝ
21sseli 3010 1 (𝐴 ∈ ℕ0𝐴 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1436  cr 7293  0cn0 8606
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3932  ax-cnex 7380  ax-resscn 7381  ax-1re 7383  ax-addrcl 7386  ax-rnegex 7398
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-un 2992  df-in 2994  df-ss 3001  df-sn 3437  df-int 3672  df-inn 8358  df-n0 8607
This theorem is referenced by:  nn0nlt0  8632  nn0le0eq0  8634  nn0p1gt0  8635  elnnnn0c  8651  nn0addge1  8652  nn0addge2  8653  nn0ge2m1nn  8666  nn0nndivcl  8668  xnn0xr  8674  nn0nepnf  8677  xnn0nemnf  8680  elnn0z  8696  elznn0nn  8697  nn0lt10b  8760  nn0ge0div  8766  nn0fz0  9461  elfz0fzfz0  9465  fz0fzelfz0  9466  fz0fzdiffz0  9469  fzctr  9472  difelfzle  9473  difelfznle  9474  elfzo0le  9524  fzonmapblen  9526  fzofzim  9527  elfzodifsumelfzo  9540  fzonn0p1  9550  fzonn0p1p1  9552  elfzom1p1elfzo  9553  ubmelm1fzo  9565  fvinim0ffz  9580  subfzo0  9581  adddivflid  9627  divfl0  9631  flltdivnn0lt  9639  addmodid  9707  modfzo0difsn  9730  inftonninf  9775  bernneq  9970  bernneq3  9972  facwordi  10044  faclbnd  10045  faclbnd3  10047  faclbnd6  10048  facubnd  10049  facavg  10050  bcval4  10056  ibcval5  10067  bcpasc  10070  fihashneq0  10099  dvdseq  10724  oddge22np1  10756  nn0ehalf  10778  nn0o  10782  nn0oddm1d2  10784  gcdn0gt0  10844  nn0gcdid0  10847  absmulgcd  10881  nn0seqcvgd  10898  algcvgblem  10906  ialgcvga  10908  lcmgcdnn  10939  prmfac1  11006  nonsq  11060  hashgcdlem  11078
  Copyright terms: Public domain W3C validator