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

Theorem nn0re 8416
Description: A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0re  |-  ( A  e.  NN0  ->  A  e.  RR )

Proof of Theorem nn0re
StepHypRef Expression
1 nn0ssre 8411 . 2  |-  NN0  C_  RR
21sseli 3004 1  |-  ( A  e.  NN0  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   RRcr 7094   NN0cn0 8407
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-cnex 7181  ax-resscn 7182  ax-1re 7184  ax-addrcl 7187  ax-rnegex 7199
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2612  df-un 2986  df-in 2988  df-ss 2995  df-sn 3422  df-int 3657  df-inn 8159  df-n0 8408
This theorem is referenced by:  nn0nlt0  8433  nn0le0eq0  8435  nn0p1gt0  8436  elnnnn0c  8452  nn0addge1  8453  nn0addge2  8454  nn0ge2m1nn  8467  nn0nndivcl  8469  xnn0xr  8475  nn0nepnf  8478  xnn0nemnf  8481  elnn0z  8497  elznn0nn  8498  nn0lt10b  8561  nn0ge0div  8567  nn0fz0  9262  elfz0fzfz0  9266  fz0fzelfz0  9267  fz0fzdiffz0  9270  fzctr  9273  difelfzle  9274  difelfznle  9275  elfzo0le  9323  fzonmapblen  9325  fzofzim  9326  elfzodifsumelfzo  9339  fzonn0p1  9349  fzonn0p1p1  9351  elfzom1p1elfzo  9352  ubmelm1fzo  9364  fvinim0ffz  9379  subfzo0  9380  adddivflid  9426  divfl0  9430  flltdivnn0lt  9438  addmodid  9506  modfzo0difsn  9529  bernneq  9742  bernneq3  9744  facwordi  9816  faclbnd  9817  faclbnd3  9819  faclbnd6  9820  facubnd  9821  facavg  9822  bcval4  9828  ibcval5  9839  bcpasc  9842  fihashneq0  9871  dvdseq  10456  oddge22np1  10488  nn0ehalf  10510  nn0o  10514  nn0oddm1d2  10516  gcdn0gt0  10576  nn0gcdid0  10579  absmulgcd  10613  nn0seqcvgd  10630  algcvgblem  10638  ialgcvga  10640  lcmgcdnn  10671  prmfac1  10738  nonsq  10792  hashgcdlem  10810
  Copyright terms: Public domain W3C validator