Theorem nnnn0d 9625

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕcn 9307  ℕ₀cn0 9568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-n0 9569

This theorem is used by:  nn0ge2m1nn0  9633  nnzd  9772  eluzge2nn0  9980  modsumfzodifsn  10848  addmodlteq  10850  expnnval  10994  expgt1  11029  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  expnbnd  11116  facwordi  11194  faclbnd  11195  facavg  11200  bcm1k  11214  bcval5  11217  bcm1n  11223  1elfz0hash  11263  pfxfvlsw  11483  wrdeqs1cat  11508  resqrexlemnm  11800  resqrexlemcvg  11801  summodc  12169  zsumdc  12170  bcxmas  12275  geo2sum  12300  geo2lim  12302  geoisum1  12305  geoisum1c  12306  cvgratnnlembern  12309  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  mertenslemi1  12321  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  eftabs  12442  efcllemp  12444  eftlub  12476  eirraplem  12563  dvdsfac  12646  divalglemnqt  12706  divalglemeunn  12707  bitsfzo  12741  bitsfi  12743  gcdval  12755  gcdcl  12762  dvdsgcdidd  12790  mulgcd  12812  rplpwr  12823  rppwr  12824  lcmcl  12869  lcmgcdnn  12879  nprmdvds1  12938  isprm5lem  12939  rpexp  12951  pwbdvdslemn  12963  pwbdvds  12964  nnmaxpw  12972  sqpweven  12974  2sqpwodd  12975  nn0sqrtelqelz  13005  phiprmpw  13023  crth  13025  eulerthlema  13031  eulerthlemth  13033  eulerth  13034  fermltl  13035  odzcllem  13044  odzdvds  13047  odzphi  13048  modprm0  13056  prm23lt5  13065  pythagtriplem6  13072  pythagtriplem7  13073  pcprmpw2  13135  dvdsprmpweqle  13139  pcprod  13148  pcfac  13152  pcbc  13153  expnprm  13155  pockthlem  13158  pockthg  13159  prmunb  13164  mul4sqlem  13195  4sqlem11  13203  4sqlem13m  13205  4sqlem14  13206  4sqlem17  13209  4sqlem18  13210  2expltfac  13242  znf1o  15070  dvply1  15957  logbgcd1irraplemexp  16165  pellexlem2  16191  wilthlem1  16193  mpodvdsmulf1o  16245  mersenne  16258  perfect1  16259  perfectlem1  16260  perfectlem2  16261  perfect  16262  pcbcctr  16264  bcmono  16265  bclbnd  16268  bposlem1  16272  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  lgslem1  16285  lgsval  16289  lgsfvalg  16290  lgsval2lem  16295  lgsvalmod  16304  lgsmod  16311  lgsdirprm  16319  lgsne0  16323  gausslemma2dlem0b  16335  gausslemma2dlem0c  16336  gausslemma2dlem1  16346  gausslemma2dlem7  16353  gausslemma2d  16354  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgseisen  16359  lgsquadlem2  16363  lgsquadlem3  16364  m1lgs  16370  2lgslem1a  16373  2sqlem3  16402  isclwwlkn  16820  clwwlknccat  16830  clwwlknon  16836  depindlem1  16913  cvgcmp2nlemabs  17247  trilpolemlt1  17257  redcwlpolemeq1  17271  nconstwlpolem0  17280