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 ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ↔ ( ( 4 · 𝐾 ) mod 𝑁 ) = 0 ) ) )

Proof

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