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 ) )