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 φAFin
fproddvdsd.s φA
Assertion fproddvdsd φxAxkAk

Proof

Step Hyp Ref Expression
1 fproddvdsd.f φAFin
2 fproddvdsd.s φA
3 f1oi I:1-1 onto
4 f1of I:1-1 ontoI:
5 3 4 mp1i φI:
6 1 2 5 fprodfvdvdsd φxAIxkAIk
7 2 sselda φxAx
8 fvresi xIx=x
9 7 8 syl φxAIx=x
10 9 eqcomd φxAx=Ix
11 2 sseld φkAk
12 11 adantr φxAkAk
13 12 imp φxAkAk
14 fvresi kIk=k
15 13 14 syl φxAkAIk=k
16 15 eqcomd φxAkAk=Ik
17 16 prodeq2dv φxAkAk=kAIk
18 10 17 breq12d φxAxkAkIxkAIk
19 18 ralbidva φxAxkAkxAIxkAIk
20 6 19 mpbird φxAxkAk