Theorem nnnn0d 9330

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 9280	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3190	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2175  ℕcn 9018  ℕ₀cn0 9277

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-n0 9278

This theorem is referenced by:  nn0ge2m1nn0  9338  nnzd  9476  eluzge2nn0  9672  modsumfzodifsn  10522  addmodlteq  10524  expnnval  10668  expgt1  10703  expaddzaplem  10708  expaddzap  10709  expmulzap  10711  expnbnd  10789  facwordi  10866  faclbnd  10867  facavg  10872  bcm1k  10886  bcval5  10889  1elfz0hash  10932  resqrexlemnm  11248  resqrexlemcvg  11249  summodc  11613  zsumdc  11614  bcxmas  11719  geo2sum  11744  geo2lim  11746  geoisum1  11749  geoisum1c  11750  cvgratnnlembern  11753  cvgratnnlemsumlt  11758  cvgratnnlemfm  11759  mertenslemi1  11765  prodmodclem3  11805  prodmodclem2a  11806  zproddc  11809  fprodseq  11813  eftabs  11886  efcllemp  11888  eftlub  11920  eirraplem  12007  dvdsfac  12090  divalglemnqt  12150  divalglemeunn  12151  bitsfzo  12185  bitsfi  12187  gcdval  12199  gcdcl  12206  dvdsgcdidd  12234  mulgcd  12256  rplpwr  12267  rppwr  12268  lcmcl  12313  lcmgcdnn  12323  nprmdvds1  12381  isprm5lem  12382  rpexp  12394  pw2dvdslemn  12406  sqpweven  12416  2sqpwodd  12417  nn0sqrtelqelz  12447  phiprmpw  12463  crth  12465  eulerthlema  12471  eulerthlemth  12473  eulerth  12474  fermltl  12475  odzcllem  12484  odzdvds  12487  odzphi  12488  modprm0  12496  prm23lt5  12505  pythagtriplem6  12512  pythagtriplem7  12513  pcprmpw2  12575  dvdsprmpweqle  12579  pcprod  12588  pcfac  12592  pcbc  12593  expnprm  12595  pockthlem  12598  pockthg  12599  prmunb  12604  mul4sqlem  12635  4sqlem11  12643  4sqlem13m  12645  4sqlem14  12646  4sqlem17  12649  4sqlem18  12650  2expltfac  12681  znf1o  14331  dvply1  15155  logbgcd1irraplemexp  15358  wilthlem1  15370  mpodvdsmulf1o  15380  mersenne  15387  perfect1  15388  perfectlem1  15389  perfectlem2  15390  perfect  15391  lgslem1  15395  lgsval  15399  lgsfvalg  15400  lgsval2lem  15405  lgsvalmod  15414  lgsmod  15421  lgsdirprm  15429  lgsne0  15433  gausslemma2dlem0b  15445  gausslemma2dlem0c  15446  gausslemma2dlem1  15456  gausslemma2dlem7  15463  gausslemma2d  15464  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgseisenlem4  15468  lgseisen  15469  lgsquadlem2  15473  lgsquadlem3  15474  m1lgs  15480  2lgslem1a  15483  2sqlem3  15512  cvgcmp2nlemabs  15835  trilpolemlt1  15844  redcwlpolemeq1  15857  nconstwlpolem0  15866