Metamath Proof Explorer

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	$⊢ φ \to Z \subseteq ℤ$
		absproddvds.f	$⊢ φ \to Z \in Fin$
		absproddvds.p	$⊢ P = \|\prod_{z \in Z} z\|$
	Assertion	absproddvds	$⊢ φ \to \forall m \in Z m ∥ P$

Proof

Step	Hyp	Ref	Expression
1		absproddvds.s	$⊢ φ \to Z \subseteq ℤ$
2		absproddvds.f	$⊢ φ \to Z \in Fin$
3		absproddvds.p	$⊢ P = \|\prod_{z \in Z} z\|$
4	2 1	fproddvdsd	$⊢ φ \to \forall m \in Z m ∥ \prod_{z \in Z} z$
5	1	sselda	$⊢ (φ \land m \in Z) \to m \in ℤ$
6	1	sselda	$⊢ (φ \land z \in Z) \to z \in ℤ$
7	2 6	fprodzcl	$⊢ φ \to \prod_{z \in Z} z \in ℤ$
8	7	adantr	$⊢ (φ \land m \in Z) \to \prod_{z \in Z} z \in ℤ$
9		dvdsabsb	$⊢ (m \in ℤ \land \prod_{z \in Z} z \in ℤ) \to (m ∥ \prod_{z \in Z} z \leftrightarrow m ∥ \|\prod_{z \in Z} z\|)$
10	5 8 9	syl2anc	$⊢ (φ \land m \in Z) \to (m ∥ \prod_{z \in Z} z \leftrightarrow m ∥ \|\prod_{z \in Z} z\|)$
11	10	biimpd	$⊢ (φ \land m \in Z) \to (m ∥ \prod_{z \in Z} z \to m ∥ \|\prod_{z \in Z} z\|)$
12	11	ralimdva	$⊢ φ \to (\forall m \in Z m ∥ \prod_{z \in Z} z \to \forall m \in Z m ∥ \|\prod_{z \in Z} z\|)$
13	4 12	mpd	$⊢ φ \to \forall m \in Z m ∥ \|\prod_{z \in Z} z\|$
14	3	breq2i	$⊢ m ∥ P \leftrightarrow m ∥ \|\prod_{z \in Z} z\|$
15	14	ralbii	$⊢ \forall m \in Z m ∥ P \leftrightarrow \forall m \in Z m ∥ \|\prod_{z \in Z} z\|$
16	13 15	sylibr	$⊢ φ \to \forall m \in Z m ∥ P$