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	⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
	absproddvds.f	⊢ ( 𝜑 → 𝑍 ∈ Fin )
	absproddvds.p	⊢ 𝑃 = ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 )
Assertion	absproddvds	⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		absproddvds.s	⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
2		absproddvds.f	⊢ ( 𝜑 → 𝑍 ∈ Fin )
3		absproddvds.p	⊢ 𝑃 = ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 )
4	2 1	fproddvdsd	⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ∏ 𝑧 ∈ 𝑍 𝑧 )
5	1	sselda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ ℤ )
6	1	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑍 ) → 𝑧 ∈ ℤ )
7	2 6	fprodzcl	⊢ ( 𝜑 → ∏ 𝑧 ∈ 𝑍 𝑧 ∈ ℤ )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∏ 𝑧 ∈ 𝑍 𝑧 ∈ ℤ )
9		dvdsabsb	⊢ ( ( 𝑚 ∈ ℤ ∧ ∏ 𝑧 ∈ 𝑍 𝑧 ∈ ℤ ) → ( 𝑚 ∥ ∏ 𝑧 ∈ 𝑍 𝑧 ↔ 𝑚 ∥ ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 ) ) )
10	5 8 9	syl2anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 ∥ ∏ 𝑧 ∈ 𝑍 𝑧 ↔ 𝑚 ∥ ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 ) ) )
11	10	biimpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 ∥ ∏ 𝑧 ∈ 𝑍 𝑧 → 𝑚 ∥ ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 ) ) )
12	11	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ∏ 𝑧 ∈ 𝑍 𝑧 → ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 ) ) )
13	4 12	mpd	⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 ) )
14	3	breq2i	⊢ ( 𝑚 ∥ 𝑃 ↔ 𝑚 ∥ ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 ) )
15	14	ralbii	⊢ ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑃 ↔ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ( abs ‘ ∏ 𝑧 ∈ 𝑍 𝑧 ) )
16	13 15	sylibr	⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑃 )