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

Theorem nnnn0d 8696
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 8646 . 2 ℕ ⊆ ℕ0
2 nnnn0d.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3021 1 (𝜑𝐴 ∈ ℕ0)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1438  cn 8394  0cn0 8643
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-n0 8644
This theorem is referenced by:  nn0ge2m1nn0  8704  nnzd  8837  eluzge2nn0  9027  modsumfzodifsn  9768  addmodlteq  9770  expnnval  9923  expgt1  9958  expaddzaplem  9963  expaddzap  9964  expmulzap  9966  expnbnd  10042  facwordi  10113  faclbnd  10114  facavg  10119  bcm1k  10133  ibcval5  10136  1elfz0hash  10179  resqrexlemnm  10416  resqrexlemcvg  10417  isummo  10737  zisum  10738  bcxmas  10845  geo2sum  10869  geo2lim  10871  geoisum1  10874  geoisum1c  10875  cvgratnnlembern  10878  cvgratnnlemsumlt  10883  cvgratnnlemfm  10884  dvdsfac  10954  divalglemnqt  11013  divalglemeunn  11014  gcdval  11044  gcdcl  11051  mulgcd  11098  rplpwr  11109  rppwr  11110  lcmcl  11147  lcmgcdnn  11157  nprmdvds1  11214  rpexp  11225  pw2dvdslemn  11236  sqpweven  11246  2sqpwodd  11247  nn0sqrtelqelz  11277  phiprmpw  11291  crth  11293
  Copyright terms: Public domain W3C validator