Metamath Proof Explorer

Theorem fprodmodd

Description: If all factors of two finite products are equal modulo M , the products are equal modulo M . (Contributed by AV, 7-Jul-2021)

Ref Expression
Hypotheses fprodmodd.a 
|- ( ph -> A e. Fin )
fprodmodd.b 
|- ( ( ph /\ k e. A ) -> B e. ZZ )
fprodmodd.c 
|- ( ( ph /\ k e. A ) -> C e. ZZ )
fprodmodd.m 
|- ( ph -> M e. NN )
fprodmodd.p 
|- ( ( ph /\ k e. A ) -> ( B mod M ) = ( C mod M ) )
Assertion fprodmodd 
|- ( ph -> ( prod_ k e. A B mod M ) = ( prod_ k e. A C mod M ) )

Proof

Step Hyp Ref Expression
1 fprodmodd.a 
 |-  ( ph -> A e. Fin )
2 fprodmodd.b 
 |-  ( ( ph /\ k e. A ) -> B e. ZZ )
3 fprodmodd.c 
 |-  ( ( ph /\ k e. A ) -> C e. ZZ )
4 fprodmodd.m 
 |-  ( ph -> M e. NN )
5 fprodmodd.p 
 |-  ( ( ph /\ k e. A ) -> ( B mod M ) = ( C mod M ) )
6 prodeq1 
 |-  ( x = (/) -> prod_ k e. x B = prod_ k e. (/) B )
7 6 oveq1d 
 |-  ( x = (/) -> ( prod_ k e. x B mod M ) = ( prod_ k e. (/) B mod M ) )
8 prodeq1 
 |-  ( x = (/) -> prod_ k e. x C = prod_ k e. (/) C )
9 8 oveq1d 
 |-  ( x = (/) -> ( prod_ k e. x C mod M ) = ( prod_ k e. (/) C mod M ) )
10 7 9 eqeq12d 
 |-  ( x = (/) -> ( ( prod_ k e. x B mod M ) = ( prod_ k e. x C mod M ) <-> ( prod_ k e. (/) B mod M ) = ( prod_ k e. (/) C mod M ) ) )
11 prodeq1 
 |-  ( x = y -> prod_ k e. x B = prod_ k e. y B )
12 11 oveq1d 
 |-  ( x = y -> ( prod_ k e. x B mod M ) = ( prod_ k e. y B mod M ) )
13 prodeq1 
 |-  ( x = y -> prod_ k e. x C = prod_ k e. y C )
14 13 oveq1d 
 |-  ( x = y -> ( prod_ k e. x C mod M ) = ( prod_ k e. y C mod M ) )
15 12 14 eqeq12d 
 |-  ( x = y -> ( ( prod_ k e. x B mod M ) = ( prod_ k e. x C mod M ) <-> ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) )
16 prodeq1 
 |-  ( x = ( y u. { i } ) -> prod_ k e. x B = prod_ k e. ( y u. { i } ) B )
17 16 oveq1d 
 |-  ( x = ( y u. { i } ) -> ( prod_ k e. x B mod M ) = ( prod_ k e. ( y u. { i } ) B mod M ) )
18 prodeq1 
 |-  ( x = ( y u. { i } ) -> prod_ k e. x C = prod_ k e. ( y u. { i } ) C )
19 18 oveq1d 
 |-  ( x = ( y u. { i } ) -> ( prod_ k e. x C mod M ) = ( prod_ k e. ( y u. { i } ) C mod M ) )
20 17 19 eqeq12d 
 |-  ( x = ( y u. { i } ) -> ( ( prod_ k e. x B mod M ) = ( prod_ k e. x C mod M ) <-> ( prod_ k e. ( y u. { i } ) B mod M ) = ( prod_ k e. ( y u. { i } ) C mod M ) ) )
21 prodeq1 
 |-  ( x = A -> prod_ k e. x B = prod_ k e. A B )
22 21 oveq1d 
 |-  ( x = A -> ( prod_ k e. x B mod M ) = ( prod_ k e. A B mod M ) )
23 prodeq1 
 |-  ( x = A -> prod_ k e. x C = prod_ k e. A C )
24 23 oveq1d 
 |-  ( x = A -> ( prod_ k e. x C mod M ) = ( prod_ k e. A C mod M ) )
25 22 24 eqeq12d 
 |-  ( x = A -> ( ( prod_ k e. x B mod M ) = ( prod_ k e. x C mod M ) <-> ( prod_ k e. A B mod M ) = ( prod_ k e. A C mod M ) ) )
26 prod0 
 |-  prod_ k e. (/) B = 1
27 26 a1i 
 |-  ( ph -> prod_ k e. (/) B = 1 )
28 27 oveq1d 
 |-  ( ph -> ( prod_ k e. (/) B mod M ) = ( 1 mod M ) )
29 prod0 
 |-  prod_ k e. (/) C = 1
30 29 eqcomi 
 |-  1 = prod_ k e. (/) C
31 30 oveq1i 
 |-  ( 1 mod M ) = ( prod_ k e. (/) C mod M )
32 28 31 eqtrdi 
 |-  ( ph -> ( prod_ k e. (/) B mod M ) = ( prod_ k e. (/) C mod M ) )
33 nfv 
 |-  F/ k ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) )
34 nfcsb1v 
 |-  F/_ k [_ i / k ]_ B
35 ssfi 
 |-  ( ( A e. Fin /\ y C_ A ) -> y e. Fin )
36 35 ex 
 |-  ( A e. Fin -> ( y C_ A -> y e. Fin ) )
37 36 1 syl11 
 |-  ( y C_ A -> ( ph -> y e. Fin ) )
38 37 adantr 
 |-  ( ( y C_ A /\ i e. ( A \ y ) ) -> ( ph -> y e. Fin ) )
39 38 impcom 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> y e. Fin )
40 simpr 
 |-  ( ( y C_ A /\ i e. ( A \ y ) ) -> i e. ( A \ y ) )
41 40 adantl 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> i e. ( A \ y ) )
42 eldifn 
 |-  ( i e. ( A \ y ) -> -. i e. y )
43 42 adantl 
 |-  ( ( y C_ A /\ i e. ( A \ y ) ) -> -. i e. y )
44 43 adantl 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> -. i e. y )
45 simpll 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ k e. y ) -> ph )
46 ssel 
 |-  ( y C_ A -> ( k e. y -> k e. A ) )
47 46 adantr 
 |-  ( ( y C_ A /\ i e. ( A \ y ) ) -> ( k e. y -> k e. A ) )
48 47 adantl 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> ( k e. y -> k e. A ) )
49 48 imp 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ k e. y ) -> k e. A )
50 45 49 2 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ k e. y ) -> B e. ZZ )
51 50 zcnd 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ k e. y ) -> B e. CC )
52 csbeq1a 
 |-  ( k = i -> B = [_ i / k ]_ B )
53 eldifi 
 |-  ( i e. ( A \ y ) -> i e. A )
54 53 adantl 
 |-  ( ( y C_ A /\ i e. ( A \ y ) ) -> i e. A )
55 2 ralrimiva 
 |-  ( ph -> A. k e. A B e. ZZ )
56 rspcsbela 
 |-  ( ( i e. A /\ A. k e. A B e. ZZ ) -> [_ i / k ]_ B e. ZZ )
57 54 55 56 syl2anr 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> [_ i / k ]_ B e. ZZ )
58 57 zcnd 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> [_ i / k ]_ B e. CC )
59 33 34 39 41 44 51 52 58 fprodsplitsn 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> prod_ k e. ( y u. { i } ) B = ( prod_ k e. y B x. [_ i / k ]_ B ) )
60 59 oveq1d 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> ( prod_ k e. ( y u. { i } ) B mod M ) = ( ( prod_ k e. y B x. [_ i / k ]_ B ) mod M ) )
61 60 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> ( prod_ k e. ( y u. { i } ) B mod M ) = ( ( prod_ k e. y B x. [_ i / k ]_ B ) mod M ) )
62 39 50 fprodzcl 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> prod_ k e. y B e. ZZ )
63 62 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> prod_ k e. y B e. ZZ )
64 45 49 3 syl2anc 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ k e. y ) -> C e. ZZ )
65 39 64 fprodzcl 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> prod_ k e. y C e. ZZ )
66 65 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> prod_ k e. y C e. ZZ )
67 57 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> [_ i / k ]_ B e. ZZ )
68 3 ralrimiva 
 |-  ( ph -> A. k e. A C e. ZZ )
69 rspcsbela 
 |-  ( ( i e. A /\ A. k e. A C e. ZZ ) -> [_ i / k ]_ C e. ZZ )
70 54 68 69 syl2anr 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> [_ i / k ]_ C e. ZZ )
71 70 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> [_ i / k ]_ C e. ZZ )
72 4 nnrpd 
 |-  ( ph -> M e. RR+ )
73 72 adantr 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> M e. RR+ )
74 73 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> M e. RR+ )
75 simpr 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) )
76 5 ralrimiva 
 |-  ( ph -> A. k e. A ( B mod M ) = ( C mod M ) )
77 rspsbca 
 |-  ( ( i e. A /\ A. k e. A ( B mod M ) = ( C mod M ) ) -> [. i / k ]. ( B mod M ) = ( C mod M ) )
78 54 76 77 syl2anr 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> [. i / k ]. ( B mod M ) = ( C mod M ) )
79 vex 
 |-  i e. _V
80 sbceqg 
 |-  ( i e. _V -> ( [. i / k ]. ( B mod M ) = ( C mod M ) <-> [_ i / k ]_ ( B mod M ) = [_ i / k ]_ ( C mod M ) ) )
81 79 80 mp1i 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> ( [. i / k ]. ( B mod M ) = ( C mod M ) <-> [_ i / k ]_ ( B mod M ) = [_ i / k ]_ ( C mod M ) ) )
82 78 81 mpbid 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> [_ i / k ]_ ( B mod M ) = [_ i / k ]_ ( C mod M ) )
83 csbov1g 
 |-  ( i e. _V -> [_ i / k ]_ ( B mod M ) = ( [_ i / k ]_ B mod M ) )
84 83 elv 
 |-  [_ i / k ]_ ( B mod M ) = ( [_ i / k ]_ B mod M )
85 csbov1g 
 |-  ( i e. _V -> [_ i / k ]_ ( C mod M ) = ( [_ i / k ]_ C mod M ) )
86 85 elv 
 |-  [_ i / k ]_ ( C mod M ) = ( [_ i / k ]_ C mod M )
87 82 84 86 3eqtr3g 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> ( [_ i / k ]_ B mod M ) = ( [_ i / k ]_ C mod M ) )
88 87 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> ( [_ i / k ]_ B mod M ) = ( [_ i / k ]_ C mod M ) )
89 63 66 67 71 74 75 88 modmul12d 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> ( ( prod_ k e. y B x. [_ i / k ]_ B ) mod M ) = ( ( prod_ k e. y C x. [_ i / k ]_ C ) mod M ) )
90 nfcsb1v 
 |-  F/_ k [_ i / k ]_ C
91 64 zcnd 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ k e. y ) -> C e. CC )
92 csbeq1a 
 |-  ( k = i -> C = [_ i / k ]_ C )
93 70 zcnd 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> [_ i / k ]_ C e. CC )
94 33 90 39 41 44 91 92 93 fprodsplitsn 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> prod_ k e. ( y u. { i } ) C = ( prod_ k e. y C x. [_ i / k ]_ C ) )
95 94 oveq1d 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> ( prod_ k e. ( y u. { i } ) C mod M ) = ( ( prod_ k e. y C x. [_ i / k ]_ C ) mod M ) )
96 95 eqcomd 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> ( ( prod_ k e. y C x. [_ i / k ]_ C ) mod M ) = ( prod_ k e. ( y u. { i } ) C mod M ) )
97 96 adantr 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> ( ( prod_ k e. y C x. [_ i / k ]_ C ) mod M ) = ( prod_ k e. ( y u. { i } ) C mod M ) )
98 61 89 97 3eqtrd 
 |-  ( ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) /\ ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) ) -> ( prod_ k e. ( y u. { i } ) B mod M ) = ( prod_ k e. ( y u. { i } ) C mod M ) )
99 98 ex 
 |-  ( ( ph /\ ( y C_ A /\ i e. ( A \ y ) ) ) -> ( ( prod_ k e. y B mod M ) = ( prod_ k e. y C mod M ) -> ( prod_ k e. ( y u. { i } ) B mod M ) = ( prod_ k e. ( y u. { i } ) C mod M ) ) )
100 10 15 20 25 32 99 1 findcard2d 
 |-  ( ph -> ( prod_ k e. A B mod M ) = ( prod_ k e. A C mod M ) )