Theorem nnnn0d 9247

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

Syntax hints:   → wi 4   ∈ wcel 2160  ℕcn 8937  ℕ₀cn0 9194

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-n0 9195

This theorem is referenced by:  nn0ge2m1nn0  9255  nnzd  9392  eluzge2nn0  9587  modsumfzodifsn  10414  addmodlteq  10416  expnnval  10541  expgt1  10576  expaddzaplem  10581  expaddzap  10582  expmulzap  10584  expnbnd  10662  facwordi  10738  faclbnd  10739  facavg  10744  bcm1k  10758  bcval5  10761  1elfz0hash  10804  resqrexlemnm  11045  resqrexlemcvg  11046  summodc  11409  zsumdc  11410  bcxmas  11515  geo2sum  11540  geo2lim  11542  geoisum1  11545  geoisum1c  11546  cvgratnnlembern  11549  cvgratnnlemsumlt  11554  cvgratnnlemfm  11555  mertenslemi1  11561  prodmodclem3  11601  prodmodclem2a  11602  zproddc  11605  fprodseq  11609  eftabs  11682  efcllemp  11684  eftlub  11716  eirraplem  11802  dvdsfac  11884  divalglemnqt  11943  divalglemeunn  11944  gcdval  11978  gcdcl  11985  dvdsgcdidd  12013  mulgcd  12035  rplpwr  12046  rppwr  12047  lcmcl  12090  lcmgcdnn  12100  nprmdvds1  12158  isprm5lem  12159  rpexp  12171  pw2dvdslemn  12183  sqpweven  12193  2sqpwodd  12194  nn0sqrtelqelz  12224  phiprmpw  12240  crth  12242  eulerthlema  12248  eulerthlemth  12250  eulerth  12251  fermltl  12252  odzcllem  12260  odzdvds  12263  odzphi  12264  modprm0  12272  prm23lt5  12281  pythagtriplem6  12288  pythagtriplem7  12289  pcprmpw2  12350  dvdsprmpweqle  12354  pcprod  12362  pcfac  12366  pcbc  12367  expnprm  12369  pockthlem  12372  pockthg  12373  prmunb  12378  mul4sqlem  12409  logbgcd1irraplemexp  14770  lgslem1  14785  lgsval  14789  lgsfvalg  14790  lgsval2lem  14795  lgsvalmod  14804  lgsmod  14811  lgsdirprm  14819  lgsne0  14823  lgseisenlem1  14834  lgseisenlem2  14835  m1lgs  14836  2sqlem3  14848  cvgcmp2nlemabs  15165  trilpolemlt1  15174  redcwlpolemeq1  15187  nconstwlpolem0  15196