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

Theorem nn0red 8660
Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1 (𝜑𝐴 ∈ ℕ0)
Assertion
Ref Expression
nn0red (𝜑𝐴 ∈ ℝ)

Proof of Theorem nn0red
StepHypRef Expression
1 nn0ssre 8610 . 2 0 ⊆ ℝ
2 nn0red.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sseldi 3012 1 (𝜑𝐴 ∈ ℝ)
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:  nn0cnd  8661  nn0readdcl  8665  nn01to3  9034  flqmulnn0  9634  modifeq2int  9721  modaddmodup  9722  modaddmodlo  9723  modsumfzodifsn  9731  expnegap0  9861  nn0le2msqd  10023  nn0opthlem2d  10025  nn0opthd  10026  faclbnd6  10048  ibcval5  10067  filtinf  10096  zfz1isolemiso  10140  oddge22np1  10756  nn0oddm1d2  10784  gcdaddm  10850  bezoutlemsup  10873  gcdzeq  10886  dvdssqlem  10894  nn0seqcvgd  10898  lcmneg  10931  mulgcddvds  10951  qredeu  10954  pw2dvdseulemle  11020  pw2dvdseu  11021  nn0sqrtelqelz  11059  nonsq  11060
  Copyright terms: Public domain W3C validator