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 ⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
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 ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑃 )