Theorem nnnn0d 9631

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

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

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 9575

This theorem is used by:  nn0ge2m1nn0  9639  nnzd  9778  eluzge2nn0  9986  modsumfzodifsn  10854  addmodlteq  10856  expnnval  11000  expgt1  11035  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  expnbnd  11122  facwordi  11200  faclbnd  11201  facavg  11206  bcm1k  11220  bcval5  11223  bcm1n  11229  1elfz0hash  11269  pfxfvlsw  11489  wrdeqs1cat  11514  resqrexlemnm  11806  resqrexlemcvg  11807  summodc  12175  zsumdc  12176  bcxmas  12281  geo2sum  12306  geo2lim  12308  geoisum1  12311  geoisum1c  12312  cvgratnnlembern  12315  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  mertenslemi1  12327  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  eftabs  12448  efcllemp  12450  eftlub  12482  eirraplem  12569  dvdsfac  12652  divalglemnqt  12712  divalglemeunn  12713  bitsfzo  12747  bitsfi  12749  gcdval  12761  gcdcl  12768  dvdsgcdidd  12796  mulgcd  12818  rplpwr  12829  rppwr  12830  lcmcl  12875  lcmgcdnn  12885  nprmdvds1  12944  isprm5lem  12945  rpexp  12957  pwbdvdslemn  12969  pwbdvds  12970  nnmaxpw  12978  sqpweven  12980  2sqpwodd  12981  nn0sqrtelqelz  13011  phiprmpw  13029  crth  13031  eulerthlema  13037  eulerthlemth  13039  eulerth  13040  fermltl  13041  odzcllem  13050  odzdvds  13053  odzphi  13054  modprm0  13062  prm23lt5  13071  pythagtriplem6  13078  pythagtriplem7  13079  pcprmpw2  13141  dvdsprmpweqle  13145  pcprod  13154  pcfac  13158  pcbc  13159  expnprm  13161  pockthlem  13164  pockthg  13165  prmunb  13170  mul4sqlem  13201  4sqlem11  13209  4sqlem13m  13211  4sqlem14  13212  4sqlem17  13215  4sqlem18  13216  2expltfac  13248  znf1o  15095  dvply1  15991  efnthr  16176  logbgcd1irraplemexp  16204  pellexlem2  16230  wilthlem1  16232  mpodvdsmulf1o  16284  mersenne  16297  perfect1  16298  perfectlem1  16299  perfectlem2  16300  perfect  16301  pcbcctr  16303  bcmono  16304  bclbnd  16307  bposlem1  16311  bposlem3  16313  bposlem4  16314  bposlem5  16315  bposlem6  16316  lgslem1  16324  lgsval  16328  lgsfvalg  16329  lgsval2lem  16334  lgsvalmod  16343  lgsmod  16350  lgsdirprm  16358  lgsne0  16362  gausslemma2dlem0b  16374  gausslemma2dlem0c  16375  gausslemma2dlem1  16385  gausslemma2dlem7  16392  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgseisen  16398  lgsquadlem2  16402  lgsquadlem3  16403  m1lgs  16409  2lgslem1a  16412  2sqlem3  16441  isclwwlkn  16859  clwwlknccat  16869  clwwlknon  16875  depindlem1  16952  cvgcmp2nlemabs  17287  trilpolemlt1  17297  redcwlpolemeq1  17311  nconstwlpolem0  17320