Theorem nnnn0d 9321

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

Step	Hyp	Ref	Expression
1		nnssnn0 9271	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3182	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2167  ℕcn 9009  ℕ₀cn0 9268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-n0 9269

This theorem is referenced by:  nn0ge2m1nn0  9329  nnzd  9466  eluzge2nn0  9662  modsumfzodifsn  10507  addmodlteq  10509  expnnval  10653  expgt1  10688  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  expnbnd  10774  facwordi  10851  faclbnd  10852  facavg  10857  bcm1k  10871  bcval5  10874  1elfz0hash  10917  resqrexlemnm  11202  resqrexlemcvg  11203  summodc  11567  zsumdc  11568  bcxmas  11673  geo2sum  11698  geo2lim  11700  geoisum1  11703  geoisum1c  11704  cvgratnnlembern  11707  cvgratnnlemsumlt  11712  cvgratnnlemfm  11713  mertenslemi1  11719  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  eftabs  11840  efcllemp  11842  eftlub  11874  eirraplem  11961  dvdsfac  12044  divalglemnqt  12104  divalglemeunn  12105  bitsfzo  12139  bitsfi  12141  gcdval  12153  gcdcl  12160  dvdsgcdidd  12188  mulgcd  12210  rplpwr  12221  rppwr  12222  lcmcl  12267  lcmgcdnn  12277  nprmdvds1  12335  isprm5lem  12336  rpexp  12348  pw2dvdslemn  12360  sqpweven  12370  2sqpwodd  12371  nn0sqrtelqelz  12401  phiprmpw  12417  crth  12419  eulerthlema  12425  eulerthlemth  12427  eulerth  12428  fermltl  12429  odzcllem  12438  odzdvds  12441  odzphi  12442  modprm0  12450  prm23lt5  12459  pythagtriplem6  12466  pythagtriplem7  12467  pcprmpw2  12529  dvdsprmpweqle  12533  pcprod  12542  pcfac  12546  pcbc  12547  expnprm  12549  pockthlem  12552  pockthg  12553  prmunb  12558  mul4sqlem  12589  4sqlem11  12597  4sqlem13m  12599  4sqlem14  12600  4sqlem17  12603  4sqlem18  12604  2expltfac  12635  znf1o  14285  dvply1  15109  logbgcd1irraplemexp  15312  wilthlem1  15324  mpodvdsmulf1o  15334  mersenne  15341  perfect1  15342  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgslem1  15349  lgsval  15353  lgsfvalg  15354  lgsval2lem  15359  lgsvalmod  15368  lgsmod  15375  lgsdirprm  15383  lgsne0  15387  gausslemma2dlem0b  15399  gausslemma2dlem0c  15400  gausslemma2dlem1  15410  gausslemma2dlem7  15417  gausslemma2d  15418  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgseisen  15423  lgsquadlem2  15427  lgsquadlem3  15428  m1lgs  15434  2lgslem1a  15437  2sqlem3  15466  cvgcmp2nlemabs  15789  trilpolemlt1  15798  redcwlpolemeq1  15811  nconstwlpolem0  15820