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 \in ℕ \land (X \in ℤ \land Y \in ℤ \land K \in ℤ)) \to ((Y - K) \mod N = (X + K) \mod N \to ((Y + K) \mod N = (X - K) \mod N \leftrightarrow 4 K \mod N = 0))$

Proof

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

Metamath Proof Explorer

Theorem modmkpkne

Proof