Metamath Proof Explorer


Theorem fprodfvdvdsd

Description: A finite product of integers is divisible by any of its factors being function values. (Contributed by AV, 1-Aug-2021)

Ref Expression
Hypotheses fprodfvdvdsd.a φAFin
fprodfvdvdsd.b φAB
fprodfvdvdsd.f φF:B
Assertion fprodfvdvdsd φxAFxkAFk

Proof

Step Hyp Ref Expression
1 fprodfvdvdsd.a φAFin
2 fprodfvdvdsd.b φAB
3 fprodfvdvdsd.f φF:B
4 1 adantr φxAAFin
5 diffi AFinAxFin
6 4 5 syl φxAAxFin
7 3 adantr φkAxF:B
8 2 ssdifssd φAxB
9 8 sselda φkAxkB
10 7 9 ffvelrnd φkAxFk
11 10 adantlr φxAkAxFk
12 6 11 fprodzcl φxAkAxFk
13 3 adantr φxAF:B
14 2 sselda φxAxB
15 13 14 ffvelrnd φxAFx
16 dvdsmul2 kAxFkFxFxkAxFkFx
17 12 15 16 syl2anc φxAFxkAxFkFx
18 17 ralrimiva φxAFxkAxFkFx
19 neldifsnd φxA¬xAx
20 disjsn Axx=¬xAx
21 19 20 sylibr φxAAxx=
22 difsnid xAAxx=A
23 22 eqcomd xAA=Axx
24 23 adantl φxAA=Axx
25 13 adantr φxAkAF:B
26 2 adantr φxAAB
27 26 sselda φxAkAkB
28 25 27 ffvelrnd φxAkAFk
29 28 zcnd φxAkAFk
30 21 24 4 29 fprodsplit φxAkAFk=kAxFkkxFk
31 simpr φxAxA
32 15 zcnd φxAFx
33 fveq2 k=xFk=Fx
34 33 prodsn xAFxkxFk=Fx
35 31 32 34 syl2anc φxAkxFk=Fx
36 35 oveq2d φxAkAxFkkxFk=kAxFkFx
37 30 36 eqtrd φxAkAFk=kAxFkFx
38 37 breq2d φxAFxkAFkFxkAxFkFx
39 38 ralbidva φxAFxkAFkxAFxkAxFkFx
40 18 39 mpbird φxAFxkAFk