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

Metamath Proof Explorer

Theorem fproddvdsd

Description: A finite product of integers is divisible by any of its factors. (Contributed by AV, 14-Aug-2020) (Proof shortened by AV, 2-Aug-2021)

Ref Expression
Hypotheses fproddvdsd.f 
|- ( ph -> A e. Fin )
fproddvdsd.s 
|- ( ph -> A C_ ZZ )
Assertion fproddvdsd 
|- ( ph -> A. x e. A x || prod_ k e. A k )

Proof

Step Hyp Ref Expression
1 fproddvdsd.f 
 |-  ( ph -> A e. Fin )
2 fproddvdsd.s 
 |-  ( ph -> A C_ ZZ )
3 f1oi 
 |-  ( _I |` ZZ ) : ZZ -1-1-onto-> ZZ
4 f1of 
 |-  ( ( _I |` ZZ ) : ZZ -1-1-onto-> ZZ -> ( _I |` ZZ ) : ZZ --> ZZ )
5 3 4 mp1i 
 |-  ( ph -> ( _I |` ZZ ) : ZZ --> ZZ )
6 1 2 5 fprodfvdvdsd 
 |-  ( ph -> A. x e. A ( ( _I |` ZZ ) ` x ) || prod_ k e. A ( ( _I |` ZZ ) ` k ) )
7 2 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. ZZ )
8 fvresi 
 |-  ( x e. ZZ -> ( ( _I |` ZZ ) ` x ) = x )
9 7 8 syl 
 |-  ( ( ph /\ x e. A ) -> ( ( _I |` ZZ ) ` x ) = x )
10 9 eqcomd 
 |-  ( ( ph /\ x e. A ) -> x = ( ( _I |` ZZ ) ` x ) )
11 2 sseld 
 |-  ( ph -> ( k e. A -> k e. ZZ ) )
12 11 adantr 
 |-  ( ( ph /\ x e. A ) -> ( k e. A -> k e. ZZ ) )
13 12 imp 
 |-  ( ( ( ph /\ x e. A ) /\ k e. A ) -> k e. ZZ )
14 fvresi 
 |-  ( k e. ZZ -> ( ( _I |` ZZ ) ` k ) = k )
15 13 14 syl 
 |-  ( ( ( ph /\ x e. A ) /\ k e. A ) -> ( ( _I |` ZZ ) ` k ) = k )
16 15 eqcomd 
 |-  ( ( ( ph /\ x e. A ) /\ k e. A ) -> k = ( ( _I |` ZZ ) ` k ) )
17 16 prodeq2dv 
 |-  ( ( ph /\ x e. A ) -> prod_ k e. A k = prod_ k e. A ( ( _I |` ZZ ) ` k ) )
18 10 17 breq12d 
 |-  ( ( ph /\ x e. A ) -> ( x || prod_ k e. A k <-> ( ( _I |` ZZ ) ` x ) || prod_ k e. A ( ( _I |` ZZ ) ` k ) ) )
19 18 ralbidva 
 |-  ( ph -> ( A. x e. A x || prod_ k e. A k <-> A. x e. A ( ( _I |` ZZ ) ` x ) || prod_ k e. A ( ( _I |` ZZ ) ` k ) ) )
20 6 19 mpbird 
 |-  ( ph -> A. x e. A x || prod_ k e. A k )