Theorem nnnn0d 9368

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℕcn 9056  ℕ₀cn0 9315

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-n0 9316

This theorem is referenced by:  nn0ge2m1nn0  9376  nnzd  9514  eluzge2nn0  9710  modsumfzodifsn  10563  addmodlteq  10565  expnnval  10709  expgt1  10744  expaddzaplem  10749  expaddzap  10750  expmulzap  10752  expnbnd  10830  facwordi  10907  faclbnd  10908  facavg  10913  bcm1k  10927  bcval5  10930  1elfz0hash  10973  pfxfvlsw  11171  wrdeqs1cat  11196  resqrexlemnm  11404  resqrexlemcvg  11405  summodc  11769  zsumdc  11770  bcxmas  11875  geo2sum  11900  geo2lim  11902  geoisum1  11905  geoisum1c  11906  cvgratnnlembern  11909  cvgratnnlemsumlt  11914  cvgratnnlemfm  11915  mertenslemi1  11921  prodmodclem3  11961  prodmodclem2a  11962  zproddc  11965  fprodseq  11969  eftabs  12042  efcllemp  12044  eftlub  12076  eirraplem  12163  dvdsfac  12246  divalglemnqt  12306  divalglemeunn  12307  bitsfzo  12341  bitsfi  12343  gcdval  12355  gcdcl  12362  dvdsgcdidd  12390  mulgcd  12412  rplpwr  12423  rppwr  12424  lcmcl  12469  lcmgcdnn  12479  nprmdvds1  12537  isprm5lem  12538  rpexp  12550  pw2dvdslemn  12562  sqpweven  12572  2sqpwodd  12573  nn0sqrtelqelz  12603  phiprmpw  12619  crth  12621  eulerthlema  12627  eulerthlemth  12629  eulerth  12630  fermltl  12631  odzcllem  12640  odzdvds  12643  odzphi  12644  modprm0  12652  prm23lt5  12661  pythagtriplem6  12668  pythagtriplem7  12669  pcprmpw2  12731  dvdsprmpweqle  12735  pcprod  12744  pcfac  12748  pcbc  12749  expnprm  12751  pockthlem  12754  pockthg  12755  prmunb  12760  mul4sqlem  12791  4sqlem11  12799  4sqlem13m  12801  4sqlem14  12802  4sqlem17  12805  4sqlem18  12806  2expltfac  12837  znf1o  14488  dvply1  15312  logbgcd1irraplemexp  15515  wilthlem1  15527  mpodvdsmulf1o  15537  mersenne  15544  perfect1  15545  perfectlem1  15546  perfectlem2  15547  perfect  15548  lgslem1  15552  lgsval  15556  lgsfvalg  15557  lgsval2lem  15562  lgsvalmod  15571  lgsmod  15578  lgsdirprm  15586  lgsne0  15590  gausslemma2dlem0b  15602  gausslemma2dlem0c  15603  gausslemma2dlem1  15613  gausslemma2dlem7  15620  gausslemma2d  15621  lgseisenlem1  15622  lgseisenlem2  15623  lgseisenlem3  15624  lgseisenlem4  15625  lgseisen  15626  lgsquadlem2  15630  lgsquadlem3  15631  m1lgs  15637  2lgslem1a  15640  2sqlem3  15669  cvgcmp2nlemabs  16112  trilpolemlt1  16121  redcwlpolemeq1  16134  nconstwlpolem0  16143