Theorem zmulcld 9608

Description: Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
zred.1	|- ( ph -> A e. ZZ )
zaddcld.1	|- ( ph -> B e. ZZ )

Assertion

Ref	Expression
zmulcld	|- ( ph -> ( A x. B ) e. ZZ )

Proof of Theorem zmulcld

Step	Hyp	Ref	Expression
1		zred.1	. 2 |- ( ph -> A e. ZZ )
2		zaddcld.1	. 2 |- ( ph -> B e. ZZ )
3		zmulcl 9533	. 2 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A x. B ) e. ZZ )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A x. B ) e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2202  (class class class)co 6018   x. cmul 8037   ZZcz 9479

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-mulrcl 8131  ax-addcom 8132  ax-mulcom 8133  ax-addass 8134  ax-mulass 8135  ax-distr 8136  ax-i2m1 8137  ax-1rid 8139  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-sub 8352  df-neg 8353  df-inn 9144  df-n0 9403  df-z 9480

This theorem is referenced by:  qapne  9873  qtri3or  10501  2tnp1ge0ge0  10562  flhalf  10563  intfracq  10583  zmodcl  10607  modqmul1  10640  addmodlteq  10661  sqoddm1div8  10956  eirraplem  12356  dvdscmulr  12399  dvdsmulcr  12400  modmulconst  12402  dvds2ln  12403  dvdsmod  12441  3dvds  12443  even2n  12453  2tp1odd  12463  ltoddhalfle  12472  m1expo  12479  m1exp1  12480  divalglemqt  12498  modremain  12508  flodddiv4  12515  bits0e  12528  bits0o  12529  bitsp1e  12531  bitsp1o  12532  bitsmod  12535  bitscmp  12537  bitsinv1lem  12540  gcdaddm  12573  gcdmultipled  12582  bezoutlemnewy  12585  bezoutlemstep  12586  bezoutlembi  12594  mulgcd  12605  dvdsmulgcd  12614  bezoutr  12621  lcmval  12653  lcmcllem  12657  lcmgcdlem  12667  mulgcddvds  12684  rpmulgcd2  12685  divgcdcoprm0  12691  cncongr1  12693  cncongr2  12694  prmind2  12710  exprmfct  12728  2sqpwodd  12766  hashdvds  12811  phimullem  12815  eulerthlem1  12817  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  prmdiv  12825  prmdiveq  12826  pythagtriplem2  12857  pythagtrip  12874  pcpremul  12884  pcqmul  12894  pcaddlem  12930  prmpwdvds  12946  4sqlem5  12973  4sqlem10  12978  4sqlem14  12995  oddennn  13031  mulgass  13764  mulgmodid  13766  znunit  14692  znrrg  14693  mpodvdsmulf1o  15733  lgsval  15752  lgsdir2lem5  15780  lgsdirprm  15782  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  gausslemma2dlem1a  15806  gausslemma2dlem1cl  15807  gausslemma2dlem1f1o  15808  gausslemma2dlem2  15810  gausslemma2dlem3  15811  gausslemma2dlem4  15812  gausslemma2dlem5a  15813  gausslemma2dlem5  15814  gausslemma2dlem6  15815  gausslemma2dlem7  15816  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgseisen  15822  lgsquadlem1  15825  lgsquad2lem1  15829  lgsquad3  15832  2lgslem1a1  15834  2lgslem1a2  15835  2lgslem1b  15837  2lgslem3b1  15846  2lgslem3c1  15847  2lgsoddprmlem2  15854  2sqlem3  15865  2sqlem4  15866