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 )