Theorem absproddvds

Description: The absolute value of the product of the elements of a finite subset of the integers is divisible by each element of this subset. (Contributed by AV, 21-Aug-2020)

	Ref	Expression
Hypotheses	absproddvds.s	|- ( ph -> Z C_ ZZ )
	absproddvds.f	|- ( ph -> Z e. Fin )
	absproddvds.p	|- P = ( abs ` prod_ z e. Z z )
Assertion	absproddvds	|- ( ph -> A. m e. Z m || P )

Proof

Step	Hyp	Ref	Expression
1		absproddvds.s	|- ( ph -> Z C_ ZZ )
2		absproddvds.f	|- ( ph -> Z e. Fin )
3		absproddvds.p	|- P = ( abs ` prod_ z e. Z z )
4	2 1	fproddvdsd	|- ( ph -> A. m e. Z m || prod_ z e. Z z )
5	1	sselda	|- ( ( ph /\ m e. Z ) -> m e. ZZ )
6	1	sselda	|- ( ( ph /\ z e. Z ) -> z e. ZZ )
7	2 6	fprodzcl	|- ( ph -> prod_ z e. Z z e. ZZ )
8	7	adantr	|- ( ( ph /\ m e. Z ) -> prod_ z e. Z z e. ZZ )
9		dvdsabsb	|- ( ( m e. ZZ /\ prod_ z e. Z z e. ZZ ) -> ( m || prod_ z e. Z z <-> m || ( abs ` prod_ z e. Z z ) ) )
10	5 8 9	syl2anc	|- ( ( ph /\ m e. Z ) -> ( m || prod_ z e. Z z <-> m || ( abs ` prod_ z e. Z z ) ) )
11	10	biimpd	|- ( ( ph /\ m e. Z ) -> ( m || prod_ z e. Z z -> m || ( abs ` prod_ z e. Z z ) ) )
12	11	ralimdva	|- ( ph -> ( A. m e. Z m || prod_ z e. Z z -> A. m e. Z m || ( abs ` prod_ z e. Z z ) ) )
13	4 12	mpd	|- ( ph -> A. m e. Z m || ( abs ` prod_ z e. Z z ) )
14	3	breq2i	|- ( m || P <-> m || ( abs ` prod_ z e. Z z ) )
15	14	ralbii	|- ( A. m e. Z m || P <-> A. m e. Z m || ( abs ` prod_ z e. Z z ) )
16	13 15	sylibr	|- ( ph -> A. m e. Z m || P )