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