Theorem nn0zd 9475

Description: A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nn0zd.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0zd	⊢ (𝜑 → 𝐴 ∈ ℤ)

Proof of Theorem nn0zd

Step	Hyp	Ref	Expression
1		nn0ssz 9372	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3190	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2175  ℕ₀cn0 9277  ℤcz 9354

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-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4478  ax-setind 4583  ax-cnex 7998  ax-resscn 7999  ax-1cn 8000  ax-1re 8001  ax-icn 8002  ax-addcl 8003  ax-addrcl 8004  ax-mulcl 8005  ax-addcom 8007  ax-addass 8009  ax-distr 8011  ax-i2m1 8012  ax-0lt1 8013  ax-0id 8015  ax-rnegex 8016  ax-cnre 8018  ax-pre-ltirr 8019  ax-pre-ltwlin 8020  ax-pre-lttrn 8021  ax-pre-ltadd 8023

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-reu 2490  df-rab 2492  df-v 2773  df-sbc 2998  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-id 4338  df-xp 4679  df-rel 4680  df-cnv 4681  df-co 4682  df-dm 4683  df-iota 5229  df-fun 5270  df-fv 5276  df-riota 5889  df-ov 5937  df-oprab 5938  df-mpo 5939  df-pnf 8091  df-mnf 8092  df-xr 8093  df-ltxr 8094  df-le 8095  df-sub 8227  df-neg 8228  df-inn 9019  df-n0 9278  df-z 9355

This theorem is referenced by:  nnzd  9476  xnn0dcle  9906  xnn0letri  9907  fseq1p1m1  10198  difelfznle  10239  flltdivnn0lt  10428  zmodfz  10472  addmodid  10498  modaddmodup  10513  modaddmodlo  10514  modsumfzodifsn  10522  addmodlteq  10524  expnegzap  10699  expaddzaplem  10708  expaddzap  10709  expmulzap  10711  nn0ltexp2  10835  nn0opthd  10848  facdiv  10864  facwordi  10866  faclbnd  10867  facavg  10872  bcval  10875  bcval5  10889  bcpasc  10892  hashfiv01gt1  10908  isfinite4im  10918  fihashneq0  10920  fseq1hash  10927  fnfz0hash  10958  ffzo0hash  10960  zfz1isolemiso  10965  wrdfin  10988  wrdffz  10990  wrdsymb0  11001  wrdlenge1n0  11002  lswwrd  11015  ccatfvalfi  11023  ccatcl  11024  ccatlen  11026  ccatval2  11029  ccatval3  11030  ccatvalfn  11032  ccatsymb  11033  ccatval21sw  11036  ccatass  11039  ccatrn  11040  lswccatn0lsw  11042  resqrexlemga  11253  zabscl  11316  fsum0diaglem  11670  modfsummodlemstep  11687  binomlem  11713  binom1p  11715  binom1dif  11717  arisum2  11729  geosergap  11736  geoserap  11737  pwm1geoserap1  11738  geolim2  11742  cvgratnnlemrate  11760  mertenslemi1  11765  mertenslem2  11766  mertensabs  11767  efcvgfsum  11897  efaddlem  11904  dvdsdc  12028  divalglemnn  12148  divalgmod  12157  bitsfzolem  12184  bitsfzo  12185  bitsmod  12186  bitsfi  12187  bitsinv1lem  12191  bitsinv1  12192  zeqzmulgcd  12210  gcd0id  12219  gcdneg  12222  gcdaddm  12224  modgcd  12231  gcdmultipled  12233  bezoutlemnewy  12236  bezoutlemstep  12237  bezoutlemmain  12238  bezoutlemzz  12242  bezoutlemmo  12246  bezoutlemle  12248  bezoutlemsup  12249  dfgcd3  12250  dvdsgcdb  12253  gcdass  12255  mulgcd  12256  gcdzeq  12262  dvdsmulgcd  12265  bezoutr  12272  bezoutr1  12273  nn0seqcvgd  12282  algfx  12293  eucalgval2  12294  eucalginv  12297  eucalglt  12298  eucalg  12300  gcddvdslcm  12314  lcmneg  12315  lcmgcdlem  12318  lcmdvds  12320  lcmgcdeq  12324  lcmdvdsb  12325  lcmass  12326  mulgcddvds  12335  rpmulgcd2  12336  qredeu  12338  divgcdcoprm0  12342  divgcdcoprmex  12343  cncongr1  12344  cncongr2  12345  sqnprm  12377  rpexp  12394  sqpweven  12416  2sqpwodd  12417  divnumden  12437  phivalfi  12453  phicl2  12455  phiprmpw  12463  crth  12465  phimullem  12466  eulerthlemfi  12469  eulerthlema  12471  hashgcdeq  12481  phisum  12482  odzdvds  12487  powm2modprm  12494  coprimeprodsq  12499  pcprendvds  12532  pcpremul  12535  pceu  12537  pcdiv  12544  pcqcl  12548  pcdvdsb  12562  pc2dvds  12572  pcprmpw2  12575  dvdsprmpweqle  12579  pcadd  12582  fldivp1  12590  pcfaclem  12591  pcfac  12592  pcbc  12593  pockthlem  12598  1arith  12609  mul4sqlem  12635  4sqlemafi  12637  4sqlemffi  12638  4sqleminfi  12639  4sqexercise1  12640  4sqlemsdc  12642  4sqlem11  12643  4sqlem12  12644  4sqlem14  12646  ennnfoneleminc  12701  ennnfonelemrnh  12706  ennnfonelemim  12714  znunit  14339  psrbaglesuppg  14352  psrbagfi  14353  psr1clfi  14368  elply2  15125  plyf  15127  elplyd  15131  ply1termlem  15132  ply1term  15133  plyaddlem1  15137  plymullem1  15138  plyaddlem  15139  plycoeid3  15147  plycolemc  15148  plycjlemc  15150  plycn  15152  plyrecj  15153  dvply1  15155  dvply2g  15156  wilthlem1  15370  sgmppw  15382  lgsval  15399  lgsfvalg  15400  lgsfcl2  15401  lgsval2lem  15405  lgsmod  15421  lgsdir2  15428  lgsne0  15433  lgsprme0  15437  gausslemma2dlem0h  15451  gausslemma2dlem0i  15452  gausslemma2dlem2  15457  gausslemma2dlem6  15462  gausslemma2d  15464  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgseisenlem4  15468  lgsquadlem1  15472  lgsquadlem2  15473  m1lgs  15480  2lgslem1a  15483  2lgslem3a  15488  2lgslem3b  15489  2lgslem3c  15490  2lgslem3d  15491  2lgslem3d1  15495  2lgs  15499  2lgsoddprmlem2  15501  2lgsoddprm  15508  2sqlem8  15518  nninffeq  15821