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 
|- ( 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 )