Theorem nnnn0d 9231

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℕcn 8921  ℕ₀cn0 9178

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-n0 9179

This theorem is referenced by:  nn0ge2m1nn0  9239  nnzd  9376  eluzge2nn0  9571  modsumfzodifsn  10398  addmodlteq  10400  expnnval  10525  expgt1  10560  expaddzaplem  10565  expaddzap  10566  expmulzap  10568  expnbnd  10646  facwordi  10722  faclbnd  10723  facavg  10728  bcm1k  10742  bcval5  10745  1elfz0hash  10788  resqrexlemnm  11029  resqrexlemcvg  11030  summodc  11393  zsumdc  11394  bcxmas  11499  geo2sum  11524  geo2lim  11526  geoisum1  11529  geoisum1c  11530  cvgratnnlembern  11533  cvgratnnlemsumlt  11538  cvgratnnlemfm  11539  mertenslemi1  11545  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  eftabs  11666  efcllemp  11668  eftlub  11700  eirraplem  11786  dvdsfac  11868  divalglemnqt  11927  divalglemeunn  11928  gcdval  11962  gcdcl  11969  dvdsgcdidd  11997  mulgcd  12019  rplpwr  12030  rppwr  12031  lcmcl  12074  lcmgcdnn  12084  nprmdvds1  12142  isprm5lem  12143  rpexp  12155  pw2dvdslemn  12167  sqpweven  12177  2sqpwodd  12178  nn0sqrtelqelz  12208  phiprmpw  12224  crth  12226  eulerthlema  12232  eulerthlemth  12234  eulerth  12235  fermltl  12236  odzcllem  12244  odzdvds  12247  odzphi  12248  modprm0  12256  prm23lt5  12265  pythagtriplem6  12272  pythagtriplem7  12273  pcprmpw2  12334  dvdsprmpweqle  12338  pcprod  12346  pcfac  12350  pcbc  12351  expnprm  12353  pockthlem  12356  pockthg  12357  prmunb  12362  mul4sqlem  12393  logbgcd1irraplemexp  14425  lgslem1  14440  lgsval  14444  lgsfvalg  14445  lgsval2lem  14450  lgsvalmod  14459  lgsmod  14466  lgsdirprm  14474  lgsne0  14478  lgseisenlem1  14489  lgseisenlem2  14490  m1lgs  14491  2sqlem3  14503  cvgcmp2nlemabs  14819  trilpolemlt1  14828  redcwlpolemeq1  14841  nconstwlpolem0  14850