This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → Z ⊆ ℤ
absproddvds.f ⊢ φ → Z ∈ Fin
absproddvds.p ⊢ P = ∏ z ∈ Z z
Assertion absproddvds ⊢ φ → ∀ m ∈ Z m ∥ P

Proof

Step Hyp Ref Expression
1 absproddvds.s ⊢ φ → Z ⊆ ℤ
2 absproddvds.f ⊢ φ → Z ∈ Fin
3 absproddvds.p ⊢ P = ∏ z ∈ Z z
4 2 1 fproddvdsd ⊢ φ → ∀ m ∈ Z m ∥ ∏ z ∈ Z z
5 1 sselda ⊢ φ ∧ m ∈ Z → m ∈ ℤ
6 1 sselda ⊢ φ ∧ z ∈ Z → z ∈ ℤ
7 2 6 fprodzcl ⊢ φ → ∏ z ∈ Z z ∈ ℤ
8 7 adantr ⊢ φ ∧ m ∈ Z → ∏ z ∈ Z z ∈ ℤ
9 dvdsabsb ⊢ m ∈ ℤ ∧ ∏ z ∈ Z z ∈ ℤ → m ∥ ∏ z ∈ Z z ↔ m ∥ ∏ z ∈ Z z
10 5 8 9 syl2anc ⊢ φ ∧ m ∈ Z → m ∥ ∏ z ∈ Z z ↔ m ∥ ∏ z ∈ Z z
11 10 biimpd ⊢ φ ∧ m ∈ Z → m ∥ ∏ z ∈ Z z → m ∥ ∏ z ∈ Z z
12 11 ralimdva ⊢ φ → ∀ m ∈ Z m ∥ ∏ z ∈ Z z → ∀ m ∈ Z m ∥ ∏ z ∈ Z z
13 4 12 mpd ⊢ φ → ∀ m ∈ Z m ∥ ∏ z ∈ Z z
14 3 breq2i ⊢ m ∥ P ↔ m ∥ ∏ z ∈ Z z
15 14 ralbii ⊢ ∀ m ∈ Z m ∥ P ↔ ∀ m ∈ Z m ∥ ∏ z ∈ Z z
16 13 15 sylibr ⊢ φ → ∀ m ∈ Z m ∥ P