# Metamath Proof Explorer

## Theorem cncongr2

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

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

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