Metamath Proof Explorer

Theorem cncongr2

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

Ref Expression
Assertion cncongr2 
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( N e. NN /\ M = ( N / ( C gcd N ) ) ) ) -> ( ( A mod M ) = ( B mod M ) -> ( ( A x. C ) mod N ) = ( ( B x. C ) mod N ) ) )

Proof

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