cncongr2

Description: The other direction of the bicondition in cncongr . (Contributed by AV, 11-Jul-2021)

		Ref	Expression
	Assertion	cncongr2	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A \mod M = B \mod M \to A C \mod N = B C \mod N)$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ A \in ℤ \to A \in ℂ$
2	1	mul01d	$⊢ A \in ℤ \to A \cdot 0 = 0$
3	2	3ad2ant1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \cdot 0 = 0$
4		zcn	$⊢ B \in ℤ \to B \in ℂ$
5	4	mul01d	$⊢ B \in ℤ \to B \cdot 0 = 0$
6	5	3ad2ant2	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B \cdot 0 = 0$
7	3 6	eqtr4d	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \cdot 0 = B \cdot 0$
8	7	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to A \cdot 0 = B \cdot 0$
9	8	oveq1d	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to A \cdot 0 \mod N = B \cdot 0 \mod N$
10	9	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land A \mod M = B \mod M) \to A \cdot 0 \mod N = B \cdot 0 \mod N$
11		oveq2	$⊢ C = 0 \to A C = A \cdot 0$
12	11	oveq1d	$⊢ C = 0 \to A C \mod N = A \cdot 0 \mod N$
13		oveq2	$⊢ C = 0 \to B C = B \cdot 0$
14	13	oveq1d	$⊢ C = 0 \to B C \mod N = B \cdot 0 \mod N$
15	12 14	eqeq12d	$⊢ C = 0 \to (A C \mod N = B C \mod N \leftrightarrow A \cdot 0 \mod N = B \cdot 0 \mod N)$
16	10 15	syl5ibr	$⊢ C = 0 \to ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land A \mod M = B \mod M) \to A C \mod N = B C \mod N)$
17		oveq2	$⊢ M = \frac{N}{C \gcd N} \to A \mod M = A \mod (\frac{N}{C \gcd N})$
18		oveq2	$⊢ M = \frac{N}{C \gcd N} \to B \mod M = B \mod (\frac{N}{C \gcd N})$
19	17 18	eqeq12d	$⊢ M = \frac{N}{C \gcd N} \to (A \mod M = B \mod M \leftrightarrow A \mod (\frac{N}{C \gcd N}) = B \mod (\frac{N}{C \gcd N}))$
20	19	adantl	$⊢ (N \in ℕ \land M = \frac{N}{C \gcd N}) \to (A \mod M = B \mod M \leftrightarrow A \mod (\frac{N}{C \gcd N}) = B \mod (\frac{N}{C \gcd N}))$
21	20	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A \mod M = B \mod M \leftrightarrow A \mod (\frac{N}{C \gcd N}) = B \mod (\frac{N}{C \gcd N}))$
22		simpl	$⊢ (N \in ℕ \land M = \frac{N}{C \gcd N}) \to N \in ℕ$
23		simp3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to C \in ℤ$
24		divgcdnnr	$⊢ (N \in ℕ \land C \in ℤ) \to \frac{N}{C \gcd N} \in ℕ$
25	22 23 24	syl2anr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to \frac{N}{C \gcd N} \in ℕ$
26		simpl1	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to A \in ℤ$
27		simpl2	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to B \in ℤ$
28		moddvds	$⊢ (\frac{N}{C \gcd N} \in ℕ \land A \in ℤ \land B \in ℤ) \to (A \mod (\frac{N}{C \gcd N}) = B \mod (\frac{N}{C \gcd N}) \leftrightarrow (\frac{N}{C \gcd N}) ∥ (A - B))$
29	25 26 27 28	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A \mod (\frac{N}{C \gcd N}) = B \mod (\frac{N}{C \gcd N}) \leftrightarrow (\frac{N}{C \gcd N}) ∥ (A - B))$
30	25	nnzd	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to \frac{N}{C \gcd N} \in ℤ$
31		zsubcl	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℤ$
32	31	3adant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A - B \in ℤ$
33	32	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to A - B \in ℤ$
34	30 33	jca	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (\frac{N}{C \gcd N} \in ℤ \land A - B \in ℤ)$
35		divides	$⊢ (\frac{N}{C \gcd N} \in ℤ \land A - B \in ℤ) \to ((\frac{N}{C \gcd N}) ∥ (A - B) \leftrightarrow \exists k \in ℤ k (\frac{N}{C \gcd N}) = A - B)$
36	34 35	syl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to ((\frac{N}{C \gcd N}) ∥ (A - B) \leftrightarrow \exists k \in ℤ k (\frac{N}{C \gcd N}) = A - B)$
37	21 29 36	3bitrd	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A \mod M = B \mod M \leftrightarrow \exists k \in ℤ k (\frac{N}{C \gcd N}) = A - B)$
38		simpr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to k \in ℤ$
39	30	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \to \frac{N}{C \gcd N} \in ℤ$
40	39	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to \frac{N}{C \gcd N} \in ℤ$
41	38 40	zmulcld	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to k (\frac{N}{C \gcd N}) \in ℤ$
42	41	zcnd	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to k (\frac{N}{C \gcd N}) \in ℂ$
43	31	zcnd	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℂ$
44	43	3adant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A - B \in ℂ$
45	44	ad3antrrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to A - B \in ℂ$
46	23	zcnd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to C \in ℂ$
47	46	ad3antrrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to C \in ℂ$
48		simpr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \to C \neq 0$
49	48	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to C \neq 0$
50	42 45 47 49	mulcan2d	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to (k (\frac{N}{C \gcd N}) C = (A - B) C \leftrightarrow k (\frac{N}{C \gcd N}) = A - B)$
51		zcn	$⊢ C \in ℤ \to C \in ℂ$
52		subdir	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to (A - B) C = A C - B C$
53	1 4 51 52	syl3an	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (A - B) C = A C - B C$
54	53	ad3antrrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to (A - B) C = A C - B C$
55	54	eqeq2d	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to (k (\frac{N}{C \gcd N}) C = (A - B) C \leftrightarrow k (\frac{N}{C \gcd N}) C = A C - B C)$
56	50 55	bitr3d	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to (k (\frac{N}{C \gcd N}) = A - B \leftrightarrow k (\frac{N}{C \gcd N}) C = A C - B C)$
57		nnz	$⊢ N \in ℕ \to N \in ℤ$
58	57	adantr	$⊢ (N \in ℕ \land k \in ℤ) \to N \in ℤ$
59		simpr	$⊢ (N \in ℕ \land k \in ℤ) \to k \in ℤ$
60	59	zcnd	$⊢ (N \in ℕ \land k \in ℤ) \to k \in ℂ$
61	60	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to k \in ℂ$
62	46	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to C \in ℂ$
63		simpl	$⊢ (N \in ℕ \land k \in ℤ) \to N \in ℕ$
64	63	nnzd	$⊢ (N \in ℕ \land k \in ℤ) \to N \in ℤ$
65	23 64	anim12i	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to (C \in ℤ \land N \in ℤ)$
66		gcdcl	$⊢ (C \in ℤ \land N \in ℤ) \to C \gcd N \in ℕ_{0}$
67	65 66	syl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to C \gcd N \in ℕ_{0}$
68	67	nn0cnd	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to C \gcd N \in ℂ$
69		nnne0	$⊢ N \in ℕ \to N \neq 0$
70	69	neneqd	$⊢ N \in ℕ \to \neg N = 0$
71	70	adantr	$⊢ (N \in ℕ \land k \in ℤ) \to \neg N = 0$
72	71	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to \neg N = 0$
73	72	intnand	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to \neg (C = 0 \land N = 0)$
74		gcdeq0	$⊢ (C \in ℤ \land N \in ℤ) \to (C \gcd N = 0 \leftrightarrow (C = 0 \land N = 0))$
75	65 74	syl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to (C \gcd N = 0 \leftrightarrow (C = 0 \land N = 0))$
76	75	necon3abid	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to (C \gcd N \neq 0 \leftrightarrow \neg (C = 0 \land N = 0))$
77	73 76	mpbird	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to C \gcd N \neq 0$
78	61 62 68 77	divassd	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to \frac{k C}{C \gcd N} = k (\frac{C}{C \gcd N})$
79	59	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to k \in ℤ$
80	57 69	jca	$⊢ N \in ℕ \to (N \in ℤ \land N \neq 0)$
81	80	adantr	$⊢ (N \in ℕ \land k \in ℤ) \to (N \in ℤ \land N \neq 0)$
82	23 81	anim12i	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to (C \in ℤ \land (N \in ℤ \land N \neq 0))$
83		3anass	$⊢ (C \in ℤ \land N \in ℤ \land N \neq 0) \leftrightarrow (C \in ℤ \land (N \in ℤ \land N \neq 0))$
84	82 83	sylibr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to (C \in ℤ \land N \in ℤ \land N \neq 0)$
85		divgcdz	$⊢ (C \in ℤ \land N \in ℤ \land N \neq 0) \to \frac{C}{C \gcd N} \in ℤ$
86	84 85	syl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to \frac{C}{C \gcd N} \in ℤ$
87	79 86	zmulcld	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to k (\frac{C}{C \gcd N}) \in ℤ$
88	78 87	eqeltrd	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to \frac{k C}{C \gcd N} \in ℤ$
89		dvdsmul1	$⊢ (N \in ℤ \land \frac{k C}{C \gcd N} \in ℤ) \to N ∥ N (\frac{k C}{C \gcd N})$
90	58 88 89	syl2an2	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to N ∥ N (\frac{k C}{C \gcd N})$
91	63	nncnd	$⊢ (N \in ℕ \land k \in ℤ) \to N \in ℂ$
92	91	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to N \in ℂ$
93		divmulasscom	$⊢ ((k \in ℂ \land N \in ℂ \land C \in ℂ) \land (C \gcd N \in ℂ \land C \gcd N \neq 0)) \to k (\frac{N}{C \gcd N}) C = N (\frac{k C}{C \gcd N})$
94	61 92 62 68 77 93	syl32anc	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to k (\frac{N}{C \gcd N}) C = N (\frac{k C}{C \gcd N})$
95	90 94	breqtrrd	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land k \in ℤ)) \to N ∥ k (\frac{N}{C \gcd N}) C$
96	95	exp32	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (N \in ℕ \to (k \in ℤ \to N ∥ k (\frac{N}{C \gcd N}) C))$
97	96	adantrd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to ((N \in ℕ \land M = \frac{N}{C \gcd N}) \to (k \in ℤ \to N ∥ k (\frac{N}{C \gcd N}) C))$
98	97	imp	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (k \in ℤ \to N ∥ k (\frac{N}{C \gcd N}) C)$
99	98	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \to (k \in ℤ \to N ∥ k (\frac{N}{C \gcd N}) C)$
100	99	imp	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to N ∥ k (\frac{N}{C \gcd N}) C$
101		breq2	$⊢ k (\frac{N}{C \gcd N}) C = A C - B C \to (N ∥ k (\frac{N}{C \gcd N}) C \leftrightarrow N ∥ (A C - B C))$
102	100 101	syl5ibcom	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to (k (\frac{N}{C \gcd N}) C = A C - B C \to N ∥ (A C - B C))$
103	56 102	sylbid	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \land k \in ℤ) \to (k (\frac{N}{C \gcd N}) = A - B \to N ∥ (A C - B C))$
104	103	rexlimdva	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \to (\exists k \in ℤ k (\frac{N}{C \gcd N}) = A - B \to N ∥ (A C - B C))$
105	22	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to N \in ℕ$
106		zmulcl	$⊢ (A \in ℤ \land C \in ℤ) \to A C \in ℤ$
107	106	3adant2	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A C \in ℤ$
108	107	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to A C \in ℤ$
109		zmulcl	$⊢ (B \in ℤ \land C \in ℤ) \to B C \in ℤ$
110	109	3adant1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B C \in ℤ$
111	110	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to B C \in ℤ$
112		moddvds	$⊢ (N \in ℕ \land A C \in ℤ \land B C \in ℤ) \to (A C \mod N = B C \mod N \leftrightarrow N ∥ (A C - B C))$
113	105 108 111 112	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A C \mod N = B C \mod N \leftrightarrow N ∥ (A C - B C))$
114	113	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \to (A C \mod N = B C \mod N \leftrightarrow N ∥ (A C - B C))$
115	104 114	sylibrd	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land C \neq 0) \to (\exists k \in ℤ k (\frac{N}{C \gcd N}) = A - B \to A C \mod N = B C \mod N)$
116	115	ex	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (C \neq 0 \to (\exists k \in ℤ k (\frac{N}{C \gcd N}) = A - B \to A C \mod N = B C \mod N))$
117	116	com23	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (\exists k \in ℤ k (\frac{N}{C \gcd N}) = A - B \to (C \neq 0 \to A C \mod N = B C \mod N))$
118	37 117	sylbid	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A \mod M = B \mod M \to (C \neq 0 \to A C \mod N = B C \mod N))$
119	118	imp	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land A \mod M = B \mod M) \to (C \neq 0 \to A C \mod N = B C \mod N)$
120	119	com12	$⊢ C \neq 0 \to ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land A \mod M = B \mod M) \to A C \mod N = B C \mod N)$
121	16 120	pm2.61ine	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land A \mod M = B \mod M) \to A C \mod N = B C \mod N$
122	121	ex	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A \mod M = B \mod M \to A C \mod N = B C \mod N)$

Metamath Proof Explorer

Theorem cncongr2

Proof