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

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 
|- ( ph -> A e. Fin )
fprodfvdvdsd.b 
|- ( ph -> A C_ B )
fprodfvdvdsd.f 
|- ( ph -> F : B --> ZZ )
Assertion fprodfvdvdsd 
|- ( ph -> A. x e. A ( F ` x ) || prod_ k e. A ( F ` k ) )

Proof

Step Hyp Ref Expression
1 fprodfvdvdsd.a 
 |-  ( ph -> A e. Fin )
2 fprodfvdvdsd.b 
 |-  ( ph -> A C_ B )
3 fprodfvdvdsd.f 
 |-  ( ph -> F : B --> ZZ )
4 1 adantr 
 |-  ( ( ph /\ x e. A ) -> A e. Fin )
5 diffi 
 |-  ( A e. Fin -> ( A \ { x } ) e. Fin )
6 4 5 syl 
 |-  ( ( ph /\ x e. A ) -> ( A \ { x } ) e. Fin )
7 3 adantr 
 |-  ( ( ph /\ k e. ( A \ { x } ) ) -> F : B --> ZZ )
8 2 ssdifssd 
 |-  ( ph -> ( A \ { x } ) C_ B )
9 8 sselda 
 |-  ( ( ph /\ k e. ( A \ { x } ) ) -> k e. B )
10 7 9 ffvelcdmd 
 |-  ( ( ph /\ k e. ( A \ { x } ) ) -> ( F ` k ) e. ZZ )
11 10 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ k e. ( A \ { x } ) ) -> ( F ` k ) e. ZZ )
12 6 11 fprodzcl 
 |-  ( ( ph /\ x e. A ) -> prod_ k e. ( A \ { x } ) ( F ` k ) e. ZZ )
13 3 adantr 
 |-  ( ( ph /\ x e. A ) -> F : B --> ZZ )
14 2 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. B )
15 13 14 ffvelcdmd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. ZZ )
16 dvdsmul2 
 |-  ( ( prod_ k e. ( A \ { x } ) ( F ` k ) e. ZZ /\ ( F ` x ) e. ZZ ) -> ( F ` x ) || ( prod_ k e. ( A \ { x } ) ( F ` k ) x. ( F ` x ) ) )
17 12 15 16 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) || ( prod_ k e. ( A \ { x } ) ( F ` k ) x. ( F ` x ) ) )
18 17 ralrimiva 
 |-  ( ph -> A. x e. A ( F ` x ) || ( prod_ k e. ( A \ { x } ) ( F ` k ) x. ( F ` x ) ) )
19 neldifsnd 
 |-  ( ( ph /\ x e. A ) -> -. x e. ( A \ { x } ) )
20 disjsn 
 |-  ( ( ( A \ { x } ) i^i { x } ) = (/) <-> -. x e. ( A \ { x } ) )
21 19 20 sylibr 
 |-  ( ( ph /\ x e. A ) -> ( ( A \ { x } ) i^i { x } ) = (/) )
22 difsnid 
 |-  ( x e. A -> ( ( A \ { x } ) u. { x } ) = A )
23 22 eqcomd 
 |-  ( x e. A -> A = ( ( A \ { x } ) u. { x } ) )
24 23 adantl 
 |-  ( ( ph /\ x e. A ) -> A = ( ( A \ { x } ) u. { x } ) )
25 13 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ k e. A ) -> F : B --> ZZ )
26 2 adantr 
 |-  ( ( ph /\ x e. A ) -> A C_ B )
27 26 sselda 
 |-  ( ( ( ph /\ x e. A ) /\ k e. A ) -> k e. B )
28 25 27 ffvelcdmd 
 |-  ( ( ( ph /\ x e. A ) /\ k e. A ) -> ( F ` k ) e. ZZ )
29 28 zcnd 
 |-  ( ( ( ph /\ x e. A ) /\ k e. A ) -> ( F ` k ) e. CC )
30 21 24 4 29 fprodsplit 
 |-  ( ( ph /\ x e. A ) -> prod_ k e. A ( F ` k ) = ( prod_ k e. ( A \ { x } ) ( F ` k ) x. prod_ k e. { x } ( F ` k ) ) )
31 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
32 15 zcnd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. CC )
33 fveq2 
 |-  ( k = x -> ( F ` k ) = ( F ` x ) )
34 33 prodsn 
 |-  ( ( x e. A /\ ( F ` x ) e. CC ) -> prod_ k e. { x } ( F ` k ) = ( F ` x ) )
35 31 32 34 syl2anc 
 |-  ( ( ph /\ x e. A ) -> prod_ k e. { x } ( F ` k ) = ( F ` x ) )
36 35 oveq2d 
 |-  ( ( ph /\ x e. A ) -> ( prod_ k e. ( A \ { x } ) ( F ` k ) x. prod_ k e. { x } ( F ` k ) ) = ( prod_ k e. ( A \ { x } ) ( F ` k ) x. ( F ` x ) ) )
37 30 36 eqtrd 
 |-  ( ( ph /\ x e. A ) -> prod_ k e. A ( F ` k ) = ( prod_ k e. ( A \ { x } ) ( F ` k ) x. ( F ` x ) ) )
38 37 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) || prod_ k e. A ( F ` k ) <-> ( F ` x ) || ( prod_ k e. ( A \ { x } ) ( F ` k ) x. ( F ` x ) ) ) )
39 38 ralbidva 
 |-  ( ph -> ( A. x e. A ( F ` x ) || prod_ k e. A ( F ` k ) <-> A. x e. A ( F ` x ) || ( prod_ k e. ( A \ { x } ) ( F ` k ) x. ( F ` x ) ) ) )
40 18 39 mpbird 
 |-  ( ph -> A. x e. A ( F ` x ) || prod_ k e. A ( F ` k ) )