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

Theorem nn0red 8461
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 8411 . 2  |-  NN0  C_  RR
2 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3006 1  |-  ( ph  ->  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:  nn0cnd  8462  nn0readdcl  8466  nn01to3  8835  flqmulnn0  9433  modifeq2int  9520  modaddmodup  9521  modaddmodlo  9522  modsumfzodifsn  9530  expnegap0  9633  nn0le2msqd  9795  nn0opthlem2d  9797  nn0opthd  9798  faclbnd6  9820  ibcval5  9839  filtinf  9868  oddge22np1  10488  nn0oddm1d2  10516  gcdaddm  10582  bezoutlemsup  10605  gcdzeq  10618  dvdssqlem  10626  nn0seqcvgd  10630  lcmneg  10663  mulgcddvds  10683  qredeu  10686  pw2dvdseulemle  10752  pw2dvdseu  10753  nn0sqrtelqelz  10791  nonsq  10792
  Copyright terms: Public domain W3C validator