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

Theorem nn0red 9054
Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1  |-  ( ph  ->  A  e.  NN0 )
Assertion
Ref Expression
nn0red  |-  ( ph  ->  A  e.  RR )

Proof of Theorem nn0red
StepHypRef Expression
1 nn0ssre 9004 . 2  |-  NN0  C_  RR
2 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3099 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1481   RRcr 7642   NN0cn0 9000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-cnex 7734  ax-resscn 7735  ax-1re 7737  ax-addrcl 7740  ax-rnegex 7752
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3079  df-in 3081  df-ss 3088  df-sn 3537  df-int 3779  df-inn 8744  df-n0 9001
This theorem is referenced by:  nn0cnd  9055  nn0readdcl  9059  nn01to3  9435  flqmulnn0  10102  modifeq2int  10189  modaddmodup  10190  modaddmodlo  10191  modsumfzodifsn  10199  expnegap0  10331  nn0le2msqd  10496  nn0opthlem2d  10498  nn0opthd  10499  faclbnd6  10521  bcval5  10540  filtinf  10569  zfz1isolemiso  10613  mertenslemi1  11335  efcllemp  11399  eftlub  11431  oddge22np1  11612  nn0oddm1d2  11640  gcdaddm  11706  bezoutlemsup  11731  gcdzeq  11744  dvdssqlem  11752  nn0seqcvgd  11756  lcmneg  11789  mulgcddvds  11809  qredeu  11812  pw2dvdseulemle  11879  pw2dvdseu  11880  nn0sqrtelqelz  11918  nonsq  11919  ennnfoneleminc  11958  ennnfonelemkh  11959  ennnfonelemex  11961  ennnfonelemim  11971
  Copyright terms: Public domain W3C validator