cncongr2

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

		Ref	Expression
	Assertion	cncongr2	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) )

Proof

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

Metamath Proof Explorer

Theorem cncongr2

Proof