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 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fprodmodd.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
fprodmodd.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℤ )
fprodmodd.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fprodmodd.p ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 mod 𝑀 ) = ( 𝐶 mod 𝑀 ) )
Assertion fprodmodd ( 𝜑 → ( ∏ 𝑘 ∈ 𝐴 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝐴 𝐶 mod 𝑀 ) )

Proof

Step Hyp Ref Expression
1 fprodmodd.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fprodmodd.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
3 fprodmodd.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℤ )
4 fprodmodd.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 fprodmodd.p ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 mod 𝑀 ) = ( 𝐶 mod 𝑀 ) )
6 prodeq1 ⊢ ( 𝑥 = ∅ → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ ∅ 𝐵 )
7 6 oveq1d ⊢ ( 𝑥 = ∅ → ( ∏ 𝑘 ∈ 𝑥 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ ∅ 𝐵 mod 𝑀 ) )
8 prodeq1 ⊢ ( 𝑥 = ∅ → ∏ 𝑘 ∈ 𝑥 𝐶 = ∏ 𝑘 ∈ ∅ 𝐶 )
9 8 oveq1d ⊢ ( 𝑥 = ∅ → ( ∏ 𝑘 ∈ 𝑥 𝐶 mod 𝑀 ) = ( ∏ 𝑘 ∈ ∅ 𝐶 mod 𝑀 ) )
10 7 9 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( ∏ 𝑘 ∈ 𝑥 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑥 𝐶 mod 𝑀 ) ↔ ( ∏ 𝑘 ∈ ∅ 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ ∅ 𝐶 mod 𝑀 ) ) )
11 prodeq1 ⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ 𝑦 𝐵 )
12 11 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ∏ 𝑘 ∈ 𝑥 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) )
13 prodeq1 ⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ 𝑥 𝐶 = ∏ 𝑘 ∈ 𝑦 𝐶 )
14 13 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ∏ 𝑘 ∈ 𝑥 𝐶 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) )
15 12 14 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ∏ 𝑘 ∈ 𝑥 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑥 𝐶 mod 𝑀 ) ↔ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) )
16 prodeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑖 } ) → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐵 )
17 16 oveq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑖 } ) → ( ∏ 𝑘 ∈ 𝑥 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐵 mod 𝑀 ) )
18 prodeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑖 } ) → ∏ 𝑘 ∈ 𝑥 𝐶 = ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐶 )
19 18 oveq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑖 } ) → ( ∏ 𝑘 ∈ 𝑥 𝐶 mod 𝑀 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐶 mod 𝑀 ) )
20 17 19 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑖 } ) → ( ( ∏ 𝑘 ∈ 𝑥 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑥 𝐶 mod 𝑀 ) ↔ ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐶 mod 𝑀 ) ) )
21 prodeq1 ⊢ ( 𝑥 = 𝐴 → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐵 )
22 21 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ∏ 𝑘 ∈ 𝑥 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 mod 𝑀 ) )
23 prodeq1 ⊢ ( 𝑥 = 𝐴 → ∏ 𝑘 ∈ 𝑥 𝐶 = ∏ 𝑘 ∈ 𝐴 𝐶 )
24 23 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ∏ 𝑘 ∈ 𝑥 𝐶 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝐴 𝐶 mod 𝑀 ) )
25 22 24 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ∏ 𝑘 ∈ 𝑥 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑥 𝐶 mod 𝑀 ) ↔ ( ∏ 𝑘 ∈ 𝐴 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝐴 𝐶 mod 𝑀 ) ) )
26 prod0 ⊢ ∏ 𝑘 ∈ ∅ 𝐵 = 1
27 26 a1i ⊢ ( 𝜑 → ∏ 𝑘 ∈ ∅ 𝐵 = 1 )
28 27 oveq1d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ∅ 𝐵 mod 𝑀 ) = ( 1 mod 𝑀 ) )
29 prod0 ⊢ ∏ 𝑘 ∈ ∅ 𝐶 = 1
30 29 eqcomi ⊢ 1 = ∏ 𝑘 ∈ ∅ 𝐶
31 30 oveq1i ⊢ ( 1 mod 𝑀 ) = ( ∏ 𝑘 ∈ ∅ 𝐶 mod 𝑀 )
32 28 31 eqtrdi ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ∅ 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ ∅ 𝐶 mod 𝑀 ) )
33 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) )
34 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵
35 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ∈ Fin )
36 35 ex ⊢ ( 𝐴 ∈ Fin → ( 𝑦 ⊆ 𝐴 → 𝑦 ∈ Fin ) )
37 36 1 syl11 ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝜑 → 𝑦 ∈ Fin ) )
38 37 adantr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝜑 → 𝑦 ∈ Fin ) )
39 38 impcom ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑦 ∈ Fin )
40 simpr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) )
41 40 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) )
42 eldifn ⊢ ( 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) → ¬ 𝑖 ∈ 𝑦 )
43 42 adantl ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) → ¬ 𝑖 ∈ 𝑦 )
44 43 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ¬ 𝑖 ∈ 𝑦 )
45 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
46 ssel ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
47 46 adantr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
48 47 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴 ) )
49 48 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
50 45 49 2 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℤ )
51 50 zcnd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℂ )
52 csbeq1a ⊢ ( 𝑘 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
53 eldifi ⊢ ( 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) → 𝑖 ∈ 𝐴 )
54 53 adantl ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑖 ∈ 𝐴 )
55 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ )
56 rspcsbela ⊢ ( ( 𝑖 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℤ )
57 54 55 56 syl2anr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℤ )
58 57 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ )
59 33 34 39 41 44 51 52 58 fprodsplitsn ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐵 = ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) )
60 59 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐵 mod 𝑀 ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) mod 𝑀 ) )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐵 mod 𝑀 ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) mod 𝑀 ) )
62 39 50 fprodzcl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ∏ 𝑘 ∈ 𝑦 𝐵 ∈ ℤ )
64 45 49 3 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐶 ∈ ℤ )
65 39 64 fprodzcl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ 𝑦 𝐶 ∈ ℤ )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ∏ 𝑘 ∈ 𝑦 𝐶 ∈ ℤ )
67 57 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℤ )
68 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℤ )
69 rspcsbela ⊢ ( ( 𝑖 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℤ ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ ℤ )
70 54 68 69 syl2anr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ ℤ )
71 70 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ ℤ )
72 4 nnrpd ⊢ ( 𝜑 → 𝑀 ∈ ℝ+ )
73 72 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑀 ∈ ℝ+ )
74 73 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → 𝑀 ∈ ℝ+ )
75 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) )
76 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑀 ) = ( 𝐶 mod 𝑀 ) )
77 rspsbca ⊢ ( ( 𝑖 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐵 mod 𝑀 ) = ( 𝐶 mod 𝑀 ) ) → [ 𝑖 / 𝑘 ] ( 𝐵 mod 𝑀 ) = ( 𝐶 mod 𝑀 ) )
78 54 76 77 syl2anr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → [ 𝑖 / 𝑘 ] ( 𝐵 mod 𝑀 ) = ( 𝐶 mod 𝑀 ) )
79 vex ⊢ 𝑖 ∈ V
80 sbceqg ⊢ ( 𝑖 ∈ V → ( [ 𝑖 / 𝑘 ] ( 𝐵 mod 𝑀 ) = ( 𝐶 mod 𝑀 ) ↔ ⦋ 𝑖 / 𝑘 ⦌ ( 𝐵 mod 𝑀 ) = ⦋ 𝑖 / 𝑘 ⦌ ( 𝐶 mod 𝑀 ) ) )
81 79 80 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( [ 𝑖 / 𝑘 ] ( 𝐵 mod 𝑀 ) = ( 𝐶 mod 𝑀 ) ↔ ⦋ 𝑖 / 𝑘 ⦌ ( 𝐵 mod 𝑀 ) = ⦋ 𝑖 / 𝑘 ⦌ ( 𝐶 mod 𝑀 ) ) )
82 78 81 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑖 / 𝑘 ⦌ ( 𝐵 mod 𝑀 ) = ⦋ 𝑖 / 𝑘 ⦌ ( 𝐶 mod 𝑀 ) )
83 csbov1g ⊢ ( 𝑖 ∈ V → ⦋ 𝑖 / 𝑘 ⦌ ( 𝐵 mod 𝑀 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐵 mod 𝑀 ) )
84 83 elv ⊢ ⦋ 𝑖 / 𝑘 ⦌ ( 𝐵 mod 𝑀 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐵 mod 𝑀 )
85 csbov1g ⊢ ( 𝑖 ∈ V → ⦋ 𝑖 / 𝑘 ⦌ ( 𝐶 mod 𝑀 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 mod 𝑀 ) )
86 85 elv ⊢ ⦋ 𝑖 / 𝑘 ⦌ ( 𝐶 mod 𝑀 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 mod 𝑀 )
87 82 84 86 3eqtr3g ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐵 mod 𝑀 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 mod 𝑀 ) )
88 87 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ( ⦋ 𝑖 / 𝑘 ⦌ 𝐵 mod 𝑀 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 mod 𝑀 ) )
89 63 66 67 71 74 75 88 modmul12d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ( ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) mod 𝑀 ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐶 · ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ) mod 𝑀 ) )
90 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐶
91 64 zcnd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐶 ∈ ℂ )
92 csbeq1a ⊢ ( 𝑘 = 𝑖 → 𝐶 = ⦋ 𝑖 / 𝑘 ⦌ 𝐶 )
93 70 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ∈ ℂ )
94 33 90 39 41 44 91 92 93 fprodsplitsn ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐶 = ( ∏ 𝑘 ∈ 𝑦 𝐶 · ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ) )
95 94 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐶 mod 𝑀 ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐶 · ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ) mod 𝑀 ) )
96 95 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( ∏ 𝑘 ∈ 𝑦 𝐶 · ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ) mod 𝑀 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐶 mod 𝑀 ) )
97 96 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ( ( ∏ 𝑘 ∈ 𝑦 𝐶 · ⦋ 𝑖 / 𝑘 ⦌ 𝐶 ) mod 𝑀 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐶 mod 𝑀 ) )
98 61 89 97 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) ) → ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐶 mod 𝑀 ) )
99 98 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑖 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( ∏ 𝑘 ∈ 𝑦 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝑦 𝐶 mod 𝑀 ) → ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑖 } ) 𝐶 mod 𝑀 ) ) )
100 10 15 20 25 32 99 1 findcard2d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝐴 𝐵 mod 𝑀 ) = ( ∏ 𝑘 ∈ 𝐴 𝐶 mod 𝑀 ) )