Metamath Proof Explorer

Theorem modmkpkne

Description: If an integer minus a constant equals another integer plus the constant modulo N , then the first integer plus the constant equals the second integer minus the constant modulo N iff the fourfold of the constant is a multiple of N . (Contributed by AV, 15-Nov-2025)

Ref Expression
Assertion modmkpkne 
|- ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 zsubcl 
 |-  ( ( Y e. ZZ /\ K e. ZZ ) -> ( Y - K ) e. ZZ )
2 1 3adant1 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( Y - K ) e. ZZ )
3 zaddcl 
 |-  ( ( X e. ZZ /\ K e. ZZ ) -> ( X + K ) e. ZZ )
4 3 3adant2 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( X + K ) e. ZZ )
5 simpl 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> N e. NN )
6 difmod0 
 |-  ( ( ( Y - K ) e. ZZ /\ ( X + K ) e. ZZ /\ N e. NN ) -> ( ( ( ( Y - K ) - ( X + K ) ) mod N ) = 0 <-> ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) ) )
7 2 4 5 6 syl2an23an 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( Y - K ) - ( X + K ) ) mod N ) = 0 <-> ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) ) )
8 zcn 
 |-  ( Y e. ZZ -> Y e. CC )
9 8 3ad2ant2 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> Y e. CC )
10 zcn 
 |-  ( K e. ZZ -> K e. CC )
11 10 3ad2ant3 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> K e. CC )
12 zcn 
 |-  ( X e. ZZ -> X e. CC )
13 12 3ad2ant1 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> X e. CC )
14 9 11 13 11 subsubadd23 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( ( Y - K ) - ( X + K ) ) = ( ( Y - X ) - ( K + K ) ) )
15 10 2timesd 
 |-  ( K e. ZZ -> ( 2 x. K ) = ( K + K ) )
16 15 eqcomd 
 |-  ( K e. ZZ -> ( K + K ) = ( 2 x. K ) )
17 16 3ad2ant3 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( K + K ) = ( 2 x. K ) )
18 17 oveq2d 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( ( Y - X ) - ( K + K ) ) = ( ( Y - X ) - ( 2 x. K ) ) )
19 14 18 eqtrd 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( ( Y - K ) - ( X + K ) ) = ( ( Y - X ) - ( 2 x. K ) ) )
20 19 adantl 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( Y - K ) - ( X + K ) ) = ( ( Y - X ) - ( 2 x. K ) ) )
21 20 oveq1d 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( Y - K ) - ( X + K ) ) mod N ) = ( ( ( Y - X ) - ( 2 x. K ) ) mod N ) )
22 21 eqeq1d 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( Y - K ) - ( X + K ) ) mod N ) = 0 <-> ( ( ( Y - X ) - ( 2 x. K ) ) mod N ) = 0 ) )
23 zsubcl 
 |-  ( ( Y e. ZZ /\ X e. ZZ ) -> ( Y - X ) e. ZZ )
24 23 ancoms 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( Y - X ) e. ZZ )
25 24 3adant3 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( Y - X ) e. ZZ )
26 2z 
 |-  2 e. ZZ
27 26 a1i 
 |-  ( K e. ZZ -> 2 e. ZZ )
28 id 
 |-  ( K e. ZZ -> K e. ZZ )
29 27 28 zmulcld 
 |-  ( K e. ZZ -> ( 2 x. K ) e. ZZ )
30 29 3ad2ant3 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( 2 x. K ) e. ZZ )
31 difmod0 
 |-  ( ( ( Y - X ) e. ZZ /\ ( 2 x. K ) e. ZZ /\ N e. NN ) -> ( ( ( ( Y - X ) - ( 2 x. K ) ) mod N ) = 0 <-> ( ( Y - X ) mod N ) = ( ( 2 x. K ) mod N ) ) )
32 25 30 5 31 syl2an23an 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( Y - X ) - ( 2 x. K ) ) mod N ) = 0 <-> ( ( Y - X ) mod N ) = ( ( 2 x. K ) mod N ) ) )
33 22 32 bitrd 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( Y - K ) - ( X + K ) ) mod N ) = 0 <-> ( ( Y - X ) mod N ) = ( ( 2 x. K ) mod N ) ) )
34 9 adantl 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> Y e. CC )
35 11 adantl 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> K e. CC )
36 13 adantl 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> X e. CC )
37 34 35 36 35 addsubsub23 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( Y + K ) - ( X - K ) ) = ( ( Y - X ) + ( K + K ) ) )
38 17 adantl 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( K + K ) = ( 2 x. K ) )
39 38 oveq2d 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( Y - X ) + ( K + K ) ) = ( ( Y - X ) + ( 2 x. K ) ) )
40 37 39 eqtrd 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( Y + K ) - ( X - K ) ) = ( ( Y - X ) + ( 2 x. K ) ) )
41 40 oveq1d 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( Y + K ) - ( X - K ) ) mod N ) = ( ( ( Y - X ) + ( 2 x. K ) ) mod N ) )
42 41 eqeq1d 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( Y + K ) - ( X - K ) ) mod N ) = 0 <-> ( ( ( Y - X ) + ( 2 x. K ) ) mod N ) = 0 ) )
43 summodnegmod 
 |-  ( ( ( Y - X ) e. ZZ /\ ( 2 x. K ) e. ZZ /\ N e. NN ) -> ( ( ( ( Y - X ) + ( 2 x. K ) ) mod N ) = 0 <-> ( ( Y - X ) mod N ) = ( -u ( 2 x. K ) mod N ) ) )
44 25 30 5 43 syl2an23an 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( Y - X ) + ( 2 x. K ) ) mod N ) = 0 <-> ( ( Y - X ) mod N ) = ( -u ( 2 x. K ) mod N ) ) )
45 42 44 bitrd 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( Y + K ) - ( X - K ) ) mod N ) = 0 <-> ( ( Y - X ) mod N ) = ( -u ( 2 x. K ) mod N ) ) )
46 45 adantr 
 |-  ( ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) /\ ( ( Y - X ) mod N ) = ( ( 2 x. K ) mod N ) ) -> ( ( ( ( Y + K ) - ( X - K ) ) mod N ) = 0 <-> ( ( Y - X ) mod N ) = ( -u ( 2 x. K ) mod N ) ) )
47 zaddcl 
 |-  ( ( Y e. ZZ /\ K e. ZZ ) -> ( Y + K ) e. ZZ )
48 47 3adant1 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( Y + K ) e. ZZ )
49 zsubcl 
 |-  ( ( X e. ZZ /\ K e. ZZ ) -> ( X - K ) e. ZZ )
50 49 3adant2 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( X - K ) e. ZZ )
51 difmod0 
 |-  ( ( ( Y + K ) e. ZZ /\ ( X - K ) e. ZZ /\ N e. NN ) -> ( ( ( ( Y + K ) - ( X - K ) ) mod N ) = 0 <-> ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) ) )
52 48 50 5 51 syl2an23an 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( Y + K ) - ( X - K ) ) mod N ) = 0 <-> ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) ) )
53 52 adantr 
 |-  ( ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) /\ ( ( Y - X ) mod N ) = ( ( 2 x. K ) mod N ) ) -> ( ( ( ( Y + K ) - ( X - K ) ) mod N ) = 0 <-> ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) ) )
54 eqeq1 
 |-  ( ( ( Y - X ) mod N ) = ( ( 2 x. K ) mod N ) -> ( ( ( Y - X ) mod N ) = ( -u ( 2 x. K ) mod N ) <-> ( ( 2 x. K ) mod N ) = ( -u ( 2 x. K ) mod N ) ) )
55 2t2e4 
 |-  ( 2 x. 2 ) = 4
56 55 eqcomi 
 |-  4 = ( 2 x. 2 )
57 56 oveq1i 
 |-  ( 4 x. K ) = ( ( 2 x. 2 ) x. K )
58 2cnd 
 |-  ( K e. ZZ -> 2 e. CC )
59 58 58 10 mulassd 
 |-  ( K e. ZZ -> ( ( 2 x. 2 ) x. K ) = ( 2 x. ( 2 x. K ) ) )
60 29 zcnd 
 |-  ( K e. ZZ -> ( 2 x. K ) e. CC )
61 60 2timesd 
 |-  ( K e. ZZ -> ( 2 x. ( 2 x. K ) ) = ( ( 2 x. K ) + ( 2 x. K ) ) )
62 59 61 eqtrd 
 |-  ( K e. ZZ -> ( ( 2 x. 2 ) x. K ) = ( ( 2 x. K ) + ( 2 x. K ) ) )
63 57 62 eqtrid 
 |-  ( K e. ZZ -> ( 4 x. K ) = ( ( 2 x. K ) + ( 2 x. K ) ) )
64 63 3ad2ant3 
 |-  ( ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) -> ( 4 x. K ) = ( ( 2 x. K ) + ( 2 x. K ) ) )
65 64 adantl 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( 4 x. K ) = ( ( 2 x. K ) + ( 2 x. K ) ) )
66 65 oveq1d 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( 4 x. K ) mod N ) = ( ( ( 2 x. K ) + ( 2 x. K ) ) mod N ) )
67 66 eqeq1d 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( 4 x. K ) mod N ) = 0 <-> ( ( ( 2 x. K ) + ( 2 x. K ) ) mod N ) = 0 ) )
68 summodnegmod 
 |-  ( ( ( 2 x. K ) e. ZZ /\ ( 2 x. K ) e. ZZ /\ N e. NN ) -> ( ( ( ( 2 x. K ) + ( 2 x. K ) ) mod N ) = 0 <-> ( ( 2 x. K ) mod N ) = ( -u ( 2 x. K ) mod N ) ) )
69 30 30 5 68 syl2an23an 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( 2 x. K ) + ( 2 x. K ) ) mod N ) = 0 <-> ( ( 2 x. K ) mod N ) = ( -u ( 2 x. K ) mod N ) ) )
70 67 69 bitr2d 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( 2 x. K ) mod N ) = ( -u ( 2 x. K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) )
71 54 70 sylan9bbr 
 |-  ( ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) /\ ( ( Y - X ) mod N ) = ( ( 2 x. K ) mod N ) ) -> ( ( ( Y - X ) mod N ) = ( -u ( 2 x. K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) )
72 46 53 71 3bitr3d 
 |-  ( ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) /\ ( ( Y - X ) mod N ) = ( ( 2 x. K ) mod N ) ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) )
73 72 ex 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( Y - X ) mod N ) = ( ( 2 x. K ) mod N ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) ) )
74 33 73 sylbid 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( ( Y - K ) - ( X + K ) ) mod N ) = 0 -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) ) )
75 7 74 sylbird 
 |-  ( ( N e. NN /\ ( X e. ZZ /\ Y e. ZZ /\ K e. ZZ ) ) -> ( ( ( Y - K ) mod N ) = ( ( X + K ) mod N ) -> ( ( ( Y + K ) mod N ) = ( ( X - K ) mod N ) <-> ( ( 4 x. K ) mod N ) = 0 ) ) )