Theorem nnnn0d 9228

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℕcn 8918  ℕ₀cn0 9175

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-n0 9176

This theorem is referenced by:  nn0ge2m1nn0  9236  nnzd  9373  eluzge2nn0  9568  modsumfzodifsn  10395  addmodlteq  10397  expnnval  10522  expgt1  10557  expaddzaplem  10562  expaddzap  10563  expmulzap  10565  expnbnd  10643  facwordi  10719  faclbnd  10720  facavg  10725  bcm1k  10739  bcval5  10742  1elfz0hash  10785  resqrexlemnm  11026  resqrexlemcvg  11027  summodc  11390  zsumdc  11391  bcxmas  11496  geo2sum  11521  geo2lim  11523  geoisum1  11526  geoisum1c  11527  cvgratnnlembern  11530  cvgratnnlemsumlt  11535  cvgratnnlemfm  11536  mertenslemi1  11542  prodmodclem3  11582  prodmodclem2a  11583  zproddc  11586  fprodseq  11590  eftabs  11663  efcllemp  11665  eftlub  11697  eirraplem  11783  dvdsfac  11865  divalglemnqt  11924  divalglemeunn  11925  gcdval  11959  gcdcl  11966  dvdsgcdidd  11994  mulgcd  12016  rplpwr  12027  rppwr  12028  lcmcl  12071  lcmgcdnn  12081  nprmdvds1  12139  isprm5lem  12140  rpexp  12152  pw2dvdslemn  12164  sqpweven  12174  2sqpwodd  12175  nn0sqrtelqelz  12205  phiprmpw  12221  crth  12223  eulerthlema  12229  eulerthlemth  12231  eulerth  12232  fermltl  12233  odzcllem  12241  odzdvds  12244  odzphi  12245  modprm0  12253  prm23lt5  12262  pythagtriplem6  12269  pythagtriplem7  12270  pcprmpw2  12331  dvdsprmpweqle  12335  pcprod  12343  pcfac  12347  pcbc  12348  expnprm  12350  pockthlem  12353  pockthg  12354  prmunb  12359  mul4sqlem  12390  logbgcd1irraplemexp  14356  lgslem1  14371  lgsval  14375  lgsfvalg  14376  lgsval2lem  14381  lgsvalmod  14390  lgsmod  14397  lgsdirprm  14405  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2sqlem3  14434  cvgcmp2nlemabs  14750  trilpolemlt1  14759  redcwlpolemeq1  14772  nconstwlpolem0  14780