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	$⊢ φ \to A \in Fin$
	fprodmodd.b	$⊢ (φ \land k \in A) \to B \in ℤ$
	fprodmodd.c	$⊢ (φ \land k \in A) \to C \in ℤ$
	fprodmodd.m	$⊢ φ \to M \in ℕ$
	fprodmodd.p	$⊢ (φ \land k \in A) \to B \mod M = C \mod M$
Assertion	fprodmodd	$⊢ φ \to \prod_{k \in A} B \mod M = \prod_{k \in A} C \mod M$

Proof

Step	Hyp	Ref	Expression
1		fprodmodd.a	$⊢ φ \to A \in Fin$
2		fprodmodd.b	$⊢ (φ \land k \in A) \to B \in ℤ$
3		fprodmodd.c	$⊢ (φ \land k \in A) \to C \in ℤ$
4		fprodmodd.m	$⊢ φ \to M \in ℕ$
5		fprodmodd.p	$⊢ (φ \land k \in A) \to B \mod M = C \mod M$
6		prodeq1	$⊢ x = \emptyset \to \prod_{k \in x} B = \prod_{k \in \emptyset} B$
7	6	oveq1d	$⊢ x = \emptyset \to \prod_{k \in x} B \mod M = \prod_{k \in \emptyset} B \mod M$
8		prodeq1	$⊢ x = \emptyset \to \prod_{k \in x} C = \prod_{k \in \emptyset} C$
9	8	oveq1d	$⊢ x = \emptyset \to \prod_{k \in x} C \mod M = \prod_{k \in \emptyset} C \mod M$
10	7 9	eqeq12d	$⊢ x = \emptyset \to (\prod_{k \in x} B \mod M = \prod_{k \in x} C \mod M \leftrightarrow \prod_{k \in \emptyset} B \mod M = \prod_{k \in \emptyset} C \mod M)$
11		prodeq1	$⊢ x = y \to \prod_{k \in x} B = \prod_{k \in y} B$
12	11	oveq1d	$⊢ x = y \to \prod_{k \in x} B \mod M = \prod_{k \in y} B \mod M$
13		prodeq1	$⊢ x = y \to \prod_{k \in x} C = \prod_{k \in y} C$
14	13	oveq1d	$⊢ x = y \to \prod_{k \in x} C \mod M = \prod_{k \in y} C \mod M$
15	12 14	eqeq12d	$⊢ x = y \to (\prod_{k \in x} B \mod M = \prod_{k \in x} C \mod M \leftrightarrow \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M)$
16		prodeq1	$⊢ x = y \cup \{i\} \to \prod_{k \in x} B = \prod_{k \in y \cup \{i\}} B$
17	16	oveq1d	$⊢ x = y \cup \{i\} \to \prod_{k \in x} B \mod M = \prod_{k \in y \cup \{i\}} B \mod M$
18		prodeq1	$⊢ x = y \cup \{i\} \to \prod_{k \in x} C = \prod_{k \in y \cup \{i\}} C$
19	18	oveq1d	$⊢ x = y \cup \{i\} \to \prod_{k \in x} C \mod M = \prod_{k \in y \cup \{i\}} C \mod M$
20	17 19	eqeq12d	$⊢ x = y \cup \{i\} \to (\prod_{k \in x} B \mod M = \prod_{k \in x} C \mod M \leftrightarrow \prod_{k \in y \cup \{i\}} B \mod M = \prod_{k \in y \cup \{i\}} C \mod M)$
21		prodeq1	$⊢ x = A \to \prod_{k \in x} B = \prod_{k \in A} B$
22	21	oveq1d	$⊢ x = A \to \prod_{k \in x} B \mod M = \prod_{k \in A} B \mod M$
23		prodeq1	$⊢ x = A \to \prod_{k \in x} C = \prod_{k \in A} C$
24	23	oveq1d	$⊢ x = A \to \prod_{k \in x} C \mod M = \prod_{k \in A} C \mod M$
25	22 24	eqeq12d	$⊢ x = A \to (\prod_{k \in x} B \mod M = \prod_{k \in x} C \mod M \leftrightarrow \prod_{k \in A} B \mod M = \prod_{k \in A} C \mod M)$
26		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
27	26	a1i	$⊢ φ \to \prod_{k \in \emptyset} B = 1$
28	27	oveq1d	$⊢ φ \to \prod_{k \in \emptyset} B \mod M = 1 \mod M$
29		prod0	$⊢ \prod_{k \in \emptyset} C = 1$
30	29	eqcomi	$⊢ 1 = \prod_{k \in \emptyset} C$
31	30	oveq1i	$⊢ 1 \mod M = \prod_{k \in \emptyset} C \mod M$
32	28 31	eqtrdi	$⊢ φ \to \prod_{k \in \emptyset} B \mod M = \prod_{k \in \emptyset} C \mod M$
33		nfv	$⊢ Ⅎ k (φ \land (y \subseteq A \land i \in (A ∖ y)))$
34		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ i / k ⦌ B$
35		ssfi	$⊢ (A \in Fin \land y \subseteq A) \to y \in Fin$
36	35	ex	$⊢ A \in Fin \to (y \subseteq A \to y \in Fin)$
37	36 1	syl11	$⊢ y \subseteq A \to (φ \to y \in Fin)$
38	37	adantr	$⊢ (y \subseteq A \land i \in (A ∖ y)) \to (φ \to y \in Fin)$
39	38	impcom	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to y \in Fin$
40		simpr	$⊢ (y \subseteq A \land i \in (A ∖ y)) \to i \in (A ∖ y)$
41	40	adantl	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to i \in (A ∖ y)$
42		eldifn	$⊢ i \in (A ∖ y) \to \neg i \in y$
43	42	adantl	$⊢ (y \subseteq A \land i \in (A ∖ y)) \to \neg i \in y$
44	43	adantl	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to \neg i \in y$
45		simpll	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land k \in y) \to φ$
46		ssel	$⊢ y \subseteq A \to (k \in y \to k \in A)$
47	46	adantr	$⊢ (y \subseteq A \land i \in (A ∖ y)) \to (k \in y \to k \in A)$
48	47	adantl	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to (k \in y \to k \in A)$
49	48	imp	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land k \in y) \to k \in A$
50	45 49 2	syl2anc	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land k \in y) \to B \in ℤ$
51	50	zcnd	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land k \in y) \to B \in ℂ$
52		csbeq1a	$⊢ k = i \to B = ⦋ i / k ⦌ B$
53		eldifi	$⊢ i \in (A ∖ y) \to i \in A$
54	53	adantl	$⊢ (y \subseteq A \land i \in (A ∖ y)) \to i \in A$
55	2	ralrimiva	$⊢ φ \to \forall k \in A B \in ℤ$
56		rspcsbela	$⊢ (i \in A \land \forall k \in A B \in ℤ) \to ⦋ i / k ⦌ B \in ℤ$
57	54 55 56	syl2anr	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to ⦋ i / k ⦌ B \in ℤ$
58	57	zcnd	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to ⦋ i / k ⦌ B \in ℂ$
59	33 34 39 41 44 51 52 58	fprodsplitsn	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to \prod_{k \in y \cup \{i\}} B = \prod_{k \in y} B ⦋ i / k ⦌ B$
60	59	oveq1d	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to \prod_{k \in y \cup \{i\}} B \mod M = \prod_{k \in y} B ⦋ i / k ⦌ B \mod M$
61	60	adantr	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to \prod_{k \in y \cup \{i\}} B \mod M = \prod_{k \in y} B ⦋ i / k ⦌ B \mod M$
62	39 50	fprodzcl	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to \prod_{k \in y} B \in ℤ$
63	62	adantr	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to \prod_{k \in y} B \in ℤ$
64	45 49 3	syl2anc	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land k \in y) \to C \in ℤ$
65	39 64	fprodzcl	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to \prod_{k \in y} C \in ℤ$
66	65	adantr	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to \prod_{k \in y} C \in ℤ$
67	57	adantr	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to ⦋ i / k ⦌ B \in ℤ$
68	3	ralrimiva	$⊢ φ \to \forall k \in A C \in ℤ$
69		rspcsbela	$⊢ (i \in A \land \forall k \in A C \in ℤ) \to ⦋ i / k ⦌ C \in ℤ$
70	54 68 69	syl2anr	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to ⦋ i / k ⦌ C \in ℤ$
71	70	adantr	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to ⦋ i / k ⦌ C \in ℤ$
72	4	nnrpd	$⊢ φ \to M \in ℝ^{+}$
73	72	adantr	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to M \in ℝ^{+}$
74	73	adantr	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to M \in ℝ^{+}$
75		simpr	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M$
76	5	ralrimiva	$⊢ φ \to \forall k \in A B \mod M = C \mod M$
77		rspsbca	$⊢ (i \in A \land \forall k \in A B \mod M = C \mod M) \to \underset{˙}{[} i / k \underset{˙}{]} B \mod M = C \mod M$
78	54 76 77	syl2anr	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to \underset{˙}{[} i / k \underset{˙}{]} B \mod M = C \mod M$
79		vex	$⊢ i \in V$
80		sbceqg	$⊢ i \in V \to (\underset{˙}{[} i / k \underset{˙}{]} B \mod M = C \mod M \leftrightarrow ⦋ i / k ⦌ (B \mod M) = ⦋ i / k ⦌ (C \mod M))$
81	79 80	mp1i	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to (\underset{˙}{[} i / k \underset{˙}{]} B \mod M = C \mod M \leftrightarrow ⦋ i / k ⦌ (B \mod M) = ⦋ i / k ⦌ (C \mod M))$
82	78 81	mpbid	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to ⦋ i / k ⦌ (B \mod M) = ⦋ i / k ⦌ (C \mod M)$
83		csbov1g	$⊢ i \in V \to ⦋ 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 \in V \to ⦋ 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	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to ⦋ i / k ⦌ B \mod M = ⦋ i / k ⦌ C \mod M$
88	87	adantr	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to ⦋ i / k ⦌ B \mod M = ⦋ i / k ⦌ C \mod M$
89	63 66 67 71 74 75 88	modmul12d	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to \prod_{k \in y} B ⦋ i / k ⦌ B \mod M = \prod_{k \in y} C ⦋ i / k ⦌ C \mod M$
90		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ i / k ⦌ C$
91	64	zcnd	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land k \in y) \to C \in ℂ$
92		csbeq1a	$⊢ k = i \to C = ⦋ i / k ⦌ C$
93	70	zcnd	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to ⦋ i / k ⦌ C \in ℂ$
94	33 90 39 41 44 91 92 93	fprodsplitsn	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to \prod_{k \in y \cup \{i\}} C = \prod_{k \in y} C ⦋ i / k ⦌ C$
95	94	oveq1d	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to \prod_{k \in y \cup \{i\}} C \mod M = \prod_{k \in y} C ⦋ i / k ⦌ C \mod M$
96	95	eqcomd	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to \prod_{k \in y} C ⦋ i / k ⦌ C \mod M = \prod_{k \in y \cup \{i\}} C \mod M$
97	96	adantr	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to \prod_{k \in y} C ⦋ i / k ⦌ C \mod M = \prod_{k \in y \cup \{i\}} C \mod M$
98	61 89 97	3eqtrd	$⊢ ((φ \land (y \subseteq A \land i \in (A ∖ y))) \land \prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M) \to \prod_{k \in y \cup \{i\}} B \mod M = \prod_{k \in y \cup \{i\}} C \mod M$
99	98	ex	$⊢ (φ \land (y \subseteq A \land i \in (A ∖ y))) \to (\prod_{k \in y} B \mod M = \prod_{k \in y} C \mod M \to \prod_{k \in y \cup \{i\}} B \mod M = \prod_{k \in y \cup \{i\}} C \mod M)$
100	10 15 20 25 32 99 1	findcard2d	$⊢ φ \to \prod_{k \in A} B \mod M = \prod_{k \in A} C \mod M$

Metamath Proof Explorer

Theorem fprodmodd

Proof