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

Theorem nnnn0d 9037
Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnnn0d.1 (𝜑𝐴 ∈ ℕ)
Assertion
Ref Expression
nnnn0d (𝜑𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d
StepHypRef Expression
1 nnssnn0 8987 . 2 ℕ ⊆ ℕ0
2 nnnn0d.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3095 1 (𝜑𝐴 ∈ ℕ0)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1480  cn 8727  0cn0 8984
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-n0 8985
This theorem is referenced by:  nn0ge2m1nn0  9045  nnzd  9179  eluzge2nn0  9372  modsumfzodifsn  10176  addmodlteq  10178  expnnval  10303  expgt1  10338  expaddzaplem  10343  expaddzap  10344  expmulzap  10346  expnbnd  10422  facwordi  10493  faclbnd  10494  facavg  10499  bcm1k  10513  bcval5  10516  1elfz0hash  10559  resqrexlemnm  10797  resqrexlemcvg  10798  summodc  11159  zsumdc  11160  bcxmas  11265  geo2sum  11290  geo2lim  11292  geoisum1  11295  geoisum1c  11296  cvgratnnlembern  11299  cvgratnnlemsumlt  11304  cvgratnnlemfm  11305  mertenslemi1  11311  prodmodclem3  11351  prodmodclem2a  11352  eftabs  11369  efcllemp  11371  eftlub  11403  eirraplem  11490  dvdsfac  11565  divalglemnqt  11624  divalglemeunn  11625  gcdval  11655  gcdcl  11662  dvdsgcdidd  11689  mulgcd  11711  rplpwr  11722  rppwr  11723  lcmcl  11760  lcmgcdnn  11770  nprmdvds1  11827  rpexp  11838  pw2dvdslemn  11850  sqpweven  11860  2sqpwodd  11861  nn0sqrtelqelz  11891  phiprmpw  11905  crth  11907  cvgcmp2nlemabs  13241  trilpolemlt1  13248
  Copyright terms: Public domain W3C validator