# Metamath Proof Explorer

## Theorem cncongr1

Description: One direction of the bicondition in cncongr . Theorem 5.4 in ApostolNT p. 109. (Contributed by AV, 13-Jul-2021)

Ref Expression
Assertion cncongr1 ${⊢}\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}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)$

### Proof

Step Hyp Ref Expression
1 zmulcl ${⊢}\left({A}\in ℤ\wedge {C}\in ℤ\right)\to {A}{C}\in ℤ$
2 1 3adant2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {A}{C}\in ℤ$
3 zmulcl ${⊢}\left({B}\in ℤ\wedge {C}\in ℤ\right)\to {B}{C}\in ℤ$
4 3 3adant1 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {B}{C}\in ℤ$
5 simpl ${⊢}\left({N}\in ℕ\wedge {M}=\frac{{N}}{{C}\mathrm{gcd}{N}}\right)\to {N}\in ℕ$
6 congr ${⊢}\left({A}{C}\in ℤ\wedge {B}{C}\in ℤ\wedge {N}\in ℕ\right)\to \left({A}{C}\mathrm{mod}{N}={B}{C}\mathrm{mod}{N}↔\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{k}\cdot {N}={A}{C}-{B}{C}\right)$
7 2 4 5 6 syl2an3an ${⊢}\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}↔\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{k}\cdot {N}={A}{C}-{B}{C}\right)$
8 simpl ${⊢}\left({C}\in ℤ\wedge {N}\in ℕ\right)\to {C}\in ℤ$
9 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
10 nnne0 ${⊢}{N}\in ℕ\to {N}\ne 0$
11 9 10 jca ${⊢}{N}\in ℕ\to \left({N}\in ℤ\wedge {N}\ne 0\right)$
12 11 adantl ${⊢}\left({C}\in ℤ\wedge {N}\in ℕ\right)\to \left({N}\in ℤ\wedge {N}\ne 0\right)$
13 eqidd ${⊢}\left({C}\in ℤ\wedge {N}\in ℕ\right)\to {C}\mathrm{gcd}{N}={C}\mathrm{gcd}{N}$
14 8 12 13 3jca ${⊢}\left({C}\in ℤ\wedge {N}\in ℕ\right)\to \left({C}\in ℤ\wedge \left({N}\in ℤ\wedge {N}\ne 0\right)\wedge {C}\mathrm{gcd}{N}={C}\mathrm{gcd}{N}\right)$
15 14 ex ${⊢}{C}\in ℤ\to \left({N}\in ℕ\to \left({C}\in ℤ\wedge \left({N}\in ℤ\wedge {N}\ne 0\right)\wedge {C}\mathrm{gcd}{N}={C}\mathrm{gcd}{N}\right)\right)$
16 15 3ad2ant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({N}\in ℕ\to \left({C}\in ℤ\wedge \left({N}\in ℤ\wedge {N}\ne 0\right)\wedge {C}\mathrm{gcd}{N}={C}\mathrm{gcd}{N}\right)\right)$
17 16 com12 ${⊢}{N}\in ℕ\to \left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({C}\in ℤ\wedge \left({N}\in ℤ\wedge {N}\ne 0\right)\wedge {C}\mathrm{gcd}{N}={C}\mathrm{gcd}{N}\right)\right)$
18 17 adantr ${⊢}\left({N}\in ℕ\wedge {M}=\frac{{N}}{{C}\mathrm{gcd}{N}}\right)\to \left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({C}\in ℤ\wedge \left({N}\in ℤ\wedge {N}\ne 0\right)\wedge {C}\mathrm{gcd}{N}={C}\mathrm{gcd}{N}\right)\right)$
19 18 impcom ${⊢}\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}\in ℤ\wedge \left({N}\in ℤ\wedge {N}\ne 0\right)\wedge {C}\mathrm{gcd}{N}={C}\mathrm{gcd}{N}\right)$
20 divgcdcoprmex ${⊢}\left({C}\in ℤ\wedge \left({N}\in ℤ\wedge {N}\ne 0\right)\wedge {C}\mathrm{gcd}{N}={C}\mathrm{gcd}{N}\right)\to \exists {r}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {s}\in ℤ\phantom{\rule{.4em}{0ex}}\left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)$
21 19 20 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 \exists {r}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {s}\in ℤ\phantom{\rule{.4em}{0ex}}\left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)$
22 21 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 {k}\in ℤ\right)\to \exists {r}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {s}\in ℤ\phantom{\rule{.4em}{0ex}}\left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)$
23 oveq2 ${⊢}{N}=\left({C}\mathrm{gcd}{N}\right){s}\to {k}\cdot {N}={k}\left({C}\mathrm{gcd}{N}\right){s}$
24 23 3ad2ant2 ${⊢}\left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\to {k}\cdot {N}={k}\left({C}\mathrm{gcd}{N}\right){s}$
25 24 adantl ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to {k}\cdot {N}={k}\left({C}\mathrm{gcd}{N}\right){s}$
26 oveq2 ${⊢}{C}=\left({C}\mathrm{gcd}{N}\right){r}\to {A}{C}={A}\left({C}\mathrm{gcd}{N}\right){r}$
27 oveq2 ${⊢}{C}=\left({C}\mathrm{gcd}{N}\right){r}\to {B}{C}={B}\left({C}\mathrm{gcd}{N}\right){r}$
28 26 27 oveq12d ${⊢}{C}=\left({C}\mathrm{gcd}{N}\right){r}\to {A}{C}-{B}{C}={A}\left({C}\mathrm{gcd}{N}\right){r}-{B}\left({C}\mathrm{gcd}{N}\right){r}$
29 28 3ad2ant1 ${⊢}\left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\to {A}{C}-{B}{C}={A}\left({C}\mathrm{gcd}{N}\right){r}-{B}\left({C}\mathrm{gcd}{N}\right){r}$
30 29 adantl ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to {A}{C}-{B}{C}={A}\left({C}\mathrm{gcd}{N}\right){r}-{B}\left({C}\mathrm{gcd}{N}\right){r}$
31 25 30 eqeq12d ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to \left({k}\cdot {N}={A}{C}-{B}{C}↔{k}\left({C}\mathrm{gcd}{N}\right){s}={A}\left({C}\mathrm{gcd}{N}\right){r}-{B}\left({C}\mathrm{gcd}{N}\right){r}\right)$
32 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 {k}\in ℤ\right)\to {k}\in ℤ$
33 32 zcnd ${⊢}\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 {k}\in ℤ\right)\to {k}\in ℂ$
34 33 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {k}\in ℂ$
35 simp3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {C}\in ℤ$
36 35 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 {C}\in ℤ$
37 9 adantr ${⊢}\left({N}\in ℕ\wedge {M}=\frac{{N}}{{C}\mathrm{gcd}{N}}\right)\to {N}\in ℤ$
38 37 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 ℤ$
39 36 38 gcdcld ${⊢}\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 {C}\mathrm{gcd}{N}\in {ℕ}_{0}$
40 39 nn0cnd ${⊢}\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 {C}\mathrm{gcd}{N}\in ℂ$
41 40 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {C}\mathrm{gcd}{N}\in ℂ$
42 simpr ${⊢}\left({r}\in ℤ\wedge {s}\in ℤ\right)\to {s}\in ℤ$
43 42 zcnd ${⊢}\left({r}\in ℤ\wedge {s}\in ℤ\right)\to {s}\in ℂ$
44 43 adantl ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {s}\in ℂ$
45 34 41 44 mul12d ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {k}\left({C}\mathrm{gcd}{N}\right){s}=\left({C}\mathrm{gcd}{N}\right){k}{s}$
46 simp1 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {A}\in ℤ$
47 46 zcnd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {A}\in ℂ$
48 47 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}\in ℂ$
49 48 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}\in ℂ$
50 35 ad2antrr ${⊢}\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 {k}\in ℤ\right)\to {C}\in ℤ$
51 5 nnzd ${⊢}\left({N}\in ℕ\wedge {M}=\frac{{N}}{{C}\mathrm{gcd}{N}}\right)\to {N}\in ℤ$
52 51 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 ℤ$
53 52 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 {k}\in ℤ\right)\to {N}\in ℤ$
54 50 53 gcdcld ${⊢}\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 {k}\in ℤ\right)\to {C}\mathrm{gcd}{N}\in {ℕ}_{0}$
55 54 nn0cnd ${⊢}\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 {k}\in ℤ\right)\to {C}\mathrm{gcd}{N}\in ℂ$
56 55 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {C}\mathrm{gcd}{N}\in ℂ$
57 simpl ${⊢}\left({r}\in ℤ\wedge {s}\in ℤ\right)\to {r}\in ℤ$
58 57 zcnd ${⊢}\left({r}\in ℤ\wedge {s}\in ℤ\right)\to {r}\in ℂ$
59 58 adantl ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {r}\in ℂ$
60 49 56 59 mul12d ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}\left({C}\mathrm{gcd}{N}\right){r}=\left({C}\mathrm{gcd}{N}\right){A}{r}$
61 simp2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {B}\in ℤ$
62 61 zcnd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {B}\in ℂ$
63 62 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}\in ℂ$
64 63 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {B}\in ℂ$
65 36 52 gcdcld ${⊢}\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 {C}\mathrm{gcd}{N}\in {ℕ}_{0}$
66 65 nn0cnd ${⊢}\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 {C}\mathrm{gcd}{N}\in ℂ$
67 66 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {C}\mathrm{gcd}{N}\in ℂ$
68 64 67 59 mul12d ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {B}\left({C}\mathrm{gcd}{N}\right){r}=\left({C}\mathrm{gcd}{N}\right){B}{r}$
69 60 68 oveq12d ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}\left({C}\mathrm{gcd}{N}\right){r}-{B}\left({C}\mathrm{gcd}{N}\right){r}=\left({C}\mathrm{gcd}{N}\right){A}{r}-\left({C}\mathrm{gcd}{N}\right){B}{r}$
70 45 69 eqeq12d ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({k}\left({C}\mathrm{gcd}{N}\right){s}={A}\left({C}\mathrm{gcd}{N}\right){r}-{B}\left({C}\mathrm{gcd}{N}\right){r}↔\left({C}\mathrm{gcd}{N}\right){k}{s}=\left({C}\mathrm{gcd}{N}\right){A}{r}-\left({C}\mathrm{gcd}{N}\right){B}{r}\right)$
71 46 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}\in ℤ$
72 71 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}\in ℤ$
73 57 adantl ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {r}\in ℤ$
74 72 73 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}{r}\in ℤ$
75 74 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}{r}\in ℂ$
76 61 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}\in ℤ$
77 76 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {B}\in ℤ$
78 77 73 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {B}{r}\in ℤ$
79 78 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {B}{r}\in ℂ$
80 67 75 79 subdid ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({C}\mathrm{gcd}{N}\right)\left({A}{r}-{B}{r}\right)=\left({C}\mathrm{gcd}{N}\right){A}{r}-\left({C}\mathrm{gcd}{N}\right){B}{r}$
81 80 eqcomd ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({C}\mathrm{gcd}{N}\right){A}{r}-\left({C}\mathrm{gcd}{N}\right){B}{r}=\left({C}\mathrm{gcd}{N}\right)\left({A}{r}-{B}{r}\right)$
82 81 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left(\left({C}\mathrm{gcd}{N}\right){k}{s}=\left({C}\mathrm{gcd}{N}\right){A}{r}-\left({C}\mathrm{gcd}{N}\right){B}{r}↔\left({C}\mathrm{gcd}{N}\right){k}{s}=\left({C}\mathrm{gcd}{N}\right)\left({A}{r}-{B}{r}\right)\right)$
83 32 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {k}\in ℤ$
84 42 adantl ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {s}\in ℤ$
85 83 84 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {k}{s}\in ℤ$
86 85 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {k}{s}\in ℂ$
87 simpl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}\in ℤ$
88 87 57 anim12i ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({A}\in ℤ\wedge {r}\in ℤ\right)$
89 zmulcl ${⊢}\left({A}\in ℤ\wedge {r}\in ℤ\right)\to {A}{r}\in ℤ$
90 88 89 syl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}{r}\in ℤ$
91 simpr ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {B}\in ℤ$
92 91 57 anim12i ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({B}\in ℤ\wedge {r}\in ℤ\right)$
93 zmulcl ${⊢}\left({B}\in ℤ\wedge {r}\in ℤ\right)\to {B}{r}\in ℤ$
94 92 93 syl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {B}{r}\in ℤ$
95 90 94 zsubcld ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}{r}-{B}{r}\in ℤ$
96 95 zcnd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}{r}-{B}{r}\in ℂ$
97 96 ex ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left({r}\in ℤ\wedge {s}\in ℤ\right)\to {A}{r}-{B}{r}\in ℂ\right)$
98 97 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left(\left({r}\in ℤ\wedge {s}\in ℤ\right)\to {A}{r}-{B}{r}\in ℂ\right)$
99 98 ad2antrr ${⊢}\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 {k}\in ℤ\right)\to \left(\left({r}\in ℤ\wedge {s}\in ℤ\right)\to {A}{r}-{B}{r}\in ℂ\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}{r}-{B}{r}\in ℂ$
101 10 adantr ${⊢}\left({N}\in ℕ\wedge {M}=\frac{{N}}{{C}\mathrm{gcd}{N}}\right)\to {N}\ne 0$
102 101 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}\ne 0$
103 gcd2n0cl ${⊢}\left({C}\in ℤ\wedge {N}\in ℤ\wedge {N}\ne 0\right)\to {C}\mathrm{gcd}{N}\in ℕ$
104 36 52 102 103 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 {C}\mathrm{gcd}{N}\in ℕ$
105 nnne0 ${⊢}{C}\mathrm{gcd}{N}\in ℕ\to {C}\mathrm{gcd}{N}\ne 0$
106 104 105 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 {C}\mathrm{gcd}{N}\ne 0$
107 106 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {C}\mathrm{gcd}{N}\ne 0$
108 86 100 67 107 mulcand ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left(\left({C}\mathrm{gcd}{N}\right){k}{s}=\left({C}\mathrm{gcd}{N}\right)\left({A}{r}-{B}{r}\right)↔{k}{s}={A}{r}-{B}{r}\right)$
109 70 82 108 3bitrd ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({k}\left({C}\mathrm{gcd}{N}\right){s}={A}\left({C}\mathrm{gcd}{N}\right){r}-{B}\left({C}\mathrm{gcd}{N}\right){r}↔{k}{s}={A}{r}-{B}{r}\right)$
110 109 adantr ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to \left({k}\left({C}\mathrm{gcd}{N}\right){s}={A}\left({C}\mathrm{gcd}{N}\right){r}-{B}\left({C}\mathrm{gcd}{N}\right){r}↔{k}{s}={A}{r}-{B}{r}\right)$
111 zcn ${⊢}{A}\in ℤ\to {A}\in ℂ$
112 zcn ${⊢}{B}\in ℤ\to {B}\in ℂ$
113 111 112 anim12i ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left({A}\in ℂ\wedge {B}\in ℂ\right)$
114 113 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\in ℂ\wedge {B}\in ℂ\right)$
115 114 ad2antrr ${⊢}\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 {k}\in ℤ\right)\to \left({A}\in ℂ\wedge {B}\in ℂ\right)$
116 115 58 anim12i ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {r}\in ℂ\right)$
117 df-3an ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {r}\in ℂ\right)↔\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {r}\in ℂ\right)$
118 116 117 sylibr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({A}\in ℂ\wedge {B}\in ℂ\wedge {r}\in ℂ\right)$
119 subdir ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {r}\in ℂ\right)\to \left({A}-{B}\right){r}={A}{r}-{B}{r}$
120 118 119 syl ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({A}-{B}\right){r}={A}{r}-{B}{r}$
121 120 eqcomd ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {A}{r}-{B}{r}=\left({A}-{B}\right){r}$
122 121 adantr ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to {A}{r}-{B}{r}=\left({A}-{B}\right){r}$
123 122 eqeq2d ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to \left({k}{s}={A}{r}-{B}{r}↔{k}{s}=\left({A}-{B}\right){r}\right)$
124 5 nncnd ${⊢}\left({N}\in ℕ\wedge {M}=\frac{{N}}{{C}\mathrm{gcd}{N}}\right)\to {N}\in ℂ$
125 124 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 ℂ$
126 125 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {N}\in ℂ$
127 84 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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to {s}\in ℂ$
128 66 106 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({C}\mathrm{gcd}{N}\in ℂ\wedge {C}\mathrm{gcd}{N}\ne 0\right)$
129 128 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({C}\mathrm{gcd}{N}\in ℂ\wedge {C}\mathrm{gcd}{N}\ne 0\right)$
130 divmul2 ${⊢}\left({N}\in ℂ\wedge {s}\in ℂ\wedge \left({C}\mathrm{gcd}{N}\in ℂ\wedge {C}\mathrm{gcd}{N}\ne 0\right)\right)\to \left(\frac{{N}}{{C}\mathrm{gcd}{N}}={s}↔{N}=\left({C}\mathrm{gcd}{N}\right){s}\right)$
131 126 127 129 130 syl3anc ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left(\frac{{N}}{{C}\mathrm{gcd}{N}}={s}↔{N}=\left({C}\mathrm{gcd}{N}\right){s}\right)$
132 simpll ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \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 {k}\in ℤ\right)$
133 73 adantr ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to {r}\in ℤ$
134 5 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 ℕ$
135 134 36 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({N}\in ℕ\wedge {C}\in ℤ\right)$
136 divgcdnnr ${⊢}\left({N}\in ℕ\wedge {C}\in ℤ\right)\to \frac{{N}}{{C}\mathrm{gcd}{N}}\in ℕ$
137 135 136 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 \frac{{N}}{{C}\mathrm{gcd}{N}}\in ℕ$
138 137 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 {k}\in ℤ\right)\to \frac{{N}}{{C}\mathrm{gcd}{N}}\in ℕ$
139 138 ad2antrr ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \frac{{N}}{{C}\mathrm{gcd}{N}}\in ℕ$
140 eleq1 ${⊢}{s}=\frac{{N}}{{C}\mathrm{gcd}{N}}\to \left({s}\in ℕ↔\frac{{N}}{{C}\mathrm{gcd}{N}}\in ℕ\right)$
141 140 eqcoms ${⊢}\frac{{N}}{{C}\mathrm{gcd}{N}}={s}\to \left({s}\in ℕ↔\frac{{N}}{{C}\mathrm{gcd}{N}}\in ℕ\right)$
142 141 adantl ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \left({s}\in ℕ↔\frac{{N}}{{C}\mathrm{gcd}{N}}\in ℕ\right)$
143 139 142 mpbird ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to {s}\in ℕ$
144 133 143 jca ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \left({r}\in ℤ\wedge {s}\in ℕ\right)$
145 132 144 jca ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)$
146 simpr ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \frac{{N}}{{C}\mathrm{gcd}{N}}={s}$
147 145 146 jca ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)$
148 nnz ${⊢}{s}\in ℕ\to {s}\in ℤ$
149 148 adantl ${⊢}\left({r}\in ℤ\wedge {s}\in ℕ\right)\to {s}\in ℤ$
150 149 anim2i ${⊢}\left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to \left({k}\in ℤ\wedge {s}\in ℤ\right)$
151 150 adantl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({k}\in ℤ\wedge {s}\in ℤ\right)$
152 dvdsmul2 ${⊢}\left({k}\in ℤ\wedge {s}\in ℤ\right)\to {s}\parallel {k}{s}$
153 151 152 syl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to {s}\parallel {k}{s}$
154 breq2 ${⊢}{k}{s}=\left({A}-{B}\right){r}\to \left({s}\parallel {k}{s}↔{s}\parallel \left({A}-{B}\right){r}\right)$
155 zsubcl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}-{B}\in ℤ$
156 155 zcnd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}-{B}\in ℂ$
157 156 adantr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to {A}-{B}\in ℂ$
158 zcn ${⊢}{r}\in ℤ\to {r}\in ℂ$
159 158 adantr ${⊢}\left({r}\in ℤ\wedge {s}\in ℕ\right)\to {r}\in ℂ$
160 159 adantl ${⊢}\left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to {r}\in ℂ$
161 160 adantl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to {r}\in ℂ$
162 157 161 mulcomd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({A}-{B}\right){r}={r}\left({A}-{B}\right)$
163 162 breq2d ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({s}\parallel \left({A}-{B}\right){r}↔{s}\parallel {r}\left({A}-{B}\right)\right)$
164 148 anim2i ${⊢}\left({r}\in ℤ\wedge {s}\in ℕ\right)\to \left({r}\in ℤ\wedge {s}\in ℤ\right)$
165 gcdcom ${⊢}\left({r}\in ℤ\wedge {s}\in ℤ\right)\to {r}\mathrm{gcd}{s}={s}\mathrm{gcd}{r}$
166 164 165 syl ${⊢}\left({r}\in ℤ\wedge {s}\in ℕ\right)\to {r}\mathrm{gcd}{s}={s}\mathrm{gcd}{r}$
167 166 eqeq1d ${⊢}\left({r}\in ℤ\wedge {s}\in ℕ\right)\to \left({r}\mathrm{gcd}{s}=1↔{s}\mathrm{gcd}{r}=1\right)$
168 167 adantl ${⊢}\left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to \left({r}\mathrm{gcd}{s}=1↔{s}\mathrm{gcd}{r}=1\right)$
169 168 adantl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({r}\mathrm{gcd}{s}=1↔{s}\mathrm{gcd}{r}=1\right)$
170 164 adantl ${⊢}\left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to \left({r}\in ℤ\wedge {s}\in ℤ\right)$
171 170 ancomd ${⊢}\left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to \left({s}\in ℤ\wedge {r}\in ℤ\right)$
172 155 171 anim12i ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({A}-{B}\in ℤ\wedge \left({s}\in ℤ\wedge {r}\in ℤ\right)\right)$
173 172 ancomd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left(\left({s}\in ℤ\wedge {r}\in ℤ\right)\wedge {A}-{B}\in ℤ\right)$
174 df-3an ${⊢}\left({s}\in ℤ\wedge {r}\in ℤ\wedge {A}-{B}\in ℤ\right)↔\left(\left({s}\in ℤ\wedge {r}\in ℤ\right)\wedge {A}-{B}\in ℤ\right)$
175 173 174 sylibr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({s}\in ℤ\wedge {r}\in ℤ\wedge {A}-{B}\in ℤ\right)$
176 coprmdvds ${⊢}\left({s}\in ℤ\wedge {r}\in ℤ\wedge {A}-{B}\in ℤ\right)\to \left(\left({s}\parallel {r}\left({A}-{B}\right)\wedge {s}\mathrm{gcd}{r}=1\right)\to {s}\parallel \left({A}-{B}\right)\right)$
177 175 176 syl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left(\left({s}\parallel {r}\left({A}-{B}\right)\wedge {s}\mathrm{gcd}{r}=1\right)\to {s}\parallel \left({A}-{B}\right)\right)$
178 simpr ${⊢}\left({r}\in ℤ\wedge {s}\in ℕ\right)\to {s}\in ℕ$
179 178 adantl ${⊢}\left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to {s}\in ℕ$
180 179 anim2i ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge {s}\in ℕ\right)$
181 180 ancomd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({s}\in ℕ\wedge \left({A}\in ℤ\wedge {B}\in ℤ\right)\right)$
182 3anass ${⊢}\left({s}\in ℕ\wedge {A}\in ℤ\wedge {B}\in ℤ\right)↔\left({s}\in ℕ\wedge \left({A}\in ℤ\wedge {B}\in ℤ\right)\right)$
183 181 182 sylibr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({s}\in ℕ\wedge {A}\in ℤ\wedge {B}\in ℤ\right)$
184 moddvds ${⊢}\left({s}\in ℕ\wedge {A}\in ℤ\wedge {B}\in ℤ\right)\to \left({A}\mathrm{mod}{s}={B}\mathrm{mod}{s}↔{s}\parallel \left({A}-{B}\right)\right)$
185 183 184 syl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({A}\mathrm{mod}{s}={B}\mathrm{mod}{s}↔{s}\parallel \left({A}-{B}\right)\right)$
186 177 185 sylibrd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left(\left({s}\parallel {r}\left({A}-{B}\right)\wedge {s}\mathrm{gcd}{r}=1\right)\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)$
187 186 expcomd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({s}\mathrm{gcd}{r}=1\to \left({s}\parallel {r}\left({A}-{B}\right)\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
188 169 187 sylbid ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({r}\mathrm{gcd}{s}=1\to \left({s}\parallel {r}\left({A}-{B}\right)\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
189 188 com23 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({s}\parallel {r}\left({A}-{B}\right)\to \left({r}\mathrm{gcd}{s}=1\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
190 163 189 sylbid ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({s}\parallel \left({A}-{B}\right){r}\to \left({r}\mathrm{gcd}{s}=1\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
191 190 com3l ${⊢}{s}\parallel \left({A}-{B}\right){r}\to \left({r}\mathrm{gcd}{s}=1\to \left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
192 154 191 syl6bi ${⊢}{k}{s}=\left({A}-{B}\right){r}\to \left({s}\parallel {k}{s}\to \left({r}\mathrm{gcd}{s}=1\to \left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)\right)$
193 192 com14 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({s}\parallel {k}{s}\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)\right)$
194 153 193 mpd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\right)\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
195 194 ex ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)\right)$
196 195 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left(\left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)\right)$
197 196 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 \left(\left({k}\in ℤ\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)\right)$
198 197 impl ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
199 198 adantr ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
200 199 imp ${⊢}\left(\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\wedge {r}\mathrm{gcd}{s}=1\right)\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)$
201 eqtr2 ${⊢}\left(\frac{{N}}{{C}\mathrm{gcd}{N}}={M}\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to {M}={s}$
202 oveq2 ${⊢}{M}={s}\to {A}\mathrm{mod}{M}={A}\mathrm{mod}{s}$
203 oveq2 ${⊢}{M}={s}\to {B}\mathrm{mod}{M}={B}\mathrm{mod}{s}$
204 202 203 eqeq12d ${⊢}{M}={s}\to \left({A}\mathrm{mod}{M}={B}\mathrm{mod}{M}↔{A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)$
205 201 204 syl ${⊢}\left(\frac{{N}}{{C}\mathrm{gcd}{N}}={M}\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \left({A}\mathrm{mod}{M}={B}\mathrm{mod}{M}↔{A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)$
206 205 ex ${⊢}\frac{{N}}{{C}\mathrm{gcd}{N}}={M}\to \left(\frac{{N}}{{C}\mathrm{gcd}{N}}={s}\to \left({A}\mathrm{mod}{M}={B}\mathrm{mod}{M}↔{A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
207 206 eqcoms ${⊢}{M}=\frac{{N}}{{C}\mathrm{gcd}{N}}\to \left(\frac{{N}}{{C}\mathrm{gcd}{N}}={s}\to \left({A}\mathrm{mod}{M}={B}\mathrm{mod}{M}↔{A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
208 207 adantl ${⊢}\left({N}\in ℕ\wedge {M}=\frac{{N}}{{C}\mathrm{gcd}{N}}\right)\to \left(\frac{{N}}{{C}\mathrm{gcd}{N}}={s}\to \left({A}\mathrm{mod}{M}={B}\mathrm{mod}{M}↔{A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
209 208 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(\frac{{N}}{{C}\mathrm{gcd}{N}}={s}\to \left({A}\mathrm{mod}{M}={B}\mathrm{mod}{M}↔{A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
210 209 ad2antrr ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\to \left(\frac{{N}}{{C}\mathrm{gcd}{N}}={s}\to \left({A}\mathrm{mod}{M}={B}\mathrm{mod}{M}↔{A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)\right)$
211 210 imp ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \left({A}\mathrm{mod}{M}={B}\mathrm{mod}{M}↔{A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)$
212 211 adantr ${⊢}\left(\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\wedge {r}\mathrm{gcd}{s}=1\right)\to \left({A}\mathrm{mod}{M}={B}\mathrm{mod}{M}↔{A}\mathrm{mod}{s}={B}\mathrm{mod}{s}\right)$
213 200 212 sylibrd ${⊢}\left(\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\wedge {r}\mathrm{gcd}{s}=1\right)\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)$
214 213 ex ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℕ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)\right)$
215 147 214 syl ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \frac{{N}}{{C}\mathrm{gcd}{N}}={s}\right)\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)\right)$
216 215 ex ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left(\frac{{N}}{{C}\mathrm{gcd}{N}}={s}\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)\right)\right)$
217 131 216 sylbird ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({N}=\left({C}\mathrm{gcd}{N}\right){s}\to \left({r}\mathrm{gcd}{s}=1\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)\right)\right)$
218 217 com3l ${⊢}{N}=\left({C}\mathrm{gcd}{N}\right){s}\to \left({r}\mathrm{gcd}{s}=1\to \left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)\right)\right)$
219 218 a1i ${⊢}{C}=\left({C}\mathrm{gcd}{N}\right){r}\to \left({N}=\left({C}\mathrm{gcd}{N}\right){s}\to \left({r}\mathrm{gcd}{s}=1\to \left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)\right)\right)\right)$
220 219 3imp ${⊢}\left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\to \left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)\right)$
221 220 impcom ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to \left({k}{s}=\left({A}-{B}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)$
222 123 221 sylbid ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to \left({k}{s}={A}{r}-{B}{r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)$
223 110 222 sylbid ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to \left({k}\left({C}\mathrm{gcd}{N}\right){s}={A}\left({C}\mathrm{gcd}{N}\right){r}-{B}\left({C}\mathrm{gcd}{N}\right){r}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)$
224 31 223 sylbid ${⊢}\left(\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\wedge \left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\right)\to \left({k}\cdot {N}={A}{C}-{B}{C}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)$
225 224 ex ${⊢}\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 {k}\in ℤ\right)\wedge \left({r}\in ℤ\wedge {s}\in ℤ\right)\right)\to \left(\left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\to \left({k}\cdot {N}={A}{C}-{B}{C}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)\right)$
226 225 rexlimdvva ${⊢}\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 {k}\in ℤ\right)\to \left(\exists {r}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {s}\in ℤ\phantom{\rule{.4em}{0ex}}\left({C}=\left({C}\mathrm{gcd}{N}\right){r}\wedge {N}=\left({C}\mathrm{gcd}{N}\right){s}\wedge {r}\mathrm{gcd}{s}=1\right)\to \left({k}\cdot {N}={A}{C}-{B}{C}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)\right)$
227 22 226 mpd ${⊢}\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 {k}\in ℤ\right)\to \left({k}\cdot {N}={A}{C}-{B}{C}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)$
228 227 rexlimdva ${⊢}\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}\cdot {N}={A}{C}-{B}{C}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)$
229 7 228 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}{C}\mathrm{mod}{N}={B}{C}\mathrm{mod}{N}\to {A}\mathrm{mod}{M}={B}\mathrm{mod}{M}\right)$