mod2addne

Description: The sums of a nonnegative integer less than the modulus and two integers whose difference is less than the modulus are not equal modulo the modulus. (Contributed by AV, 15-Nov-2025)

		Ref	Expression
	Hypothesis	mod2addne.i	$⊢ I = (0 ..^N)$
	Assertion	mod2addne	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to (X + A) \mod N \neq (X + B) \mod N$

Proof

Step	Hyp	Ref	Expression
1		mod2addne.i	$⊢ I = (0 ..^N)$
2		simp1	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to N \in ℕ$
3		zsubcl	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℤ$
4	3	3adant1	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to A - B \in ℤ$
5	4	3ad2ant2	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to A - B \in ℤ$
6		elfzolt2	$⊢ \|A - B\| \in (1 ..^N) \to \|A - B\| < N$
7	6	3ad2ant3	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to \|A - B\| < N$
8		modlt0b	$⊢ (N \in ℕ \land A - B \in ℤ \land \|A - B\| < N) \to ((A - B) \mod N = 0 \leftrightarrow A - B = 0)$
9	2 5 7 8	syl3anc	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to ((A - B) \mod N = 0 \leftrightarrow A - B = 0)$
10		fveq2	$⊢ A - B = 0 \to \|A - B\| = \|0\|$
11	10	eleq1d	$⊢ A - B = 0 \to (\|A - B\| \in (1 ..^N) \leftrightarrow \|0\| \in (1 ..^N))$
12	11	adantl	$⊢ ((N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \land A - B = 0) \to (\|A - B\| \in (1 ..^N) \leftrightarrow \|0\| \in (1 ..^N))$
13		abs0	$⊢ \|0\| = 0$
14	13	eleq1i	$⊢ \|0\| \in (1 ..^N) \leftrightarrow 0 \in (1 ..^N)$
15	14	a1i	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to (\|0\| \in (1 ..^N) \leftrightarrow 0 \in (1 ..^N))$
16		elfzo1	$⊢ 0 \in (1 ..^N) \leftrightarrow (0 \in ℕ \land N \in ℕ \land 0 < N)$
17		0nnn	$⊢ \neg 0 \in ℕ$
18	17	pm2.21i	$⊢ 0 \in ℕ \to \neg (A - B) \mod N = 0$
19	18	3ad2ant1	$⊢ (0 \in ℕ \land N \in ℕ \land 0 < N) \to \neg (A - B) \mod N = 0$
20	16 19	sylbi	$⊢ 0 \in (1 ..^N) \to \neg (A - B) \mod N = 0$
21	20	a1i	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to (0 \in (1 ..^N) \to \neg (A - B) \mod N = 0)$
22	15 21	sylbid	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to (\|0\| \in (1 ..^N) \to \neg (A - B) \mod N = 0)$
23	22	adantr	$⊢ ((N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \land A - B = 0) \to (\|0\| \in (1 ..^N) \to \neg (A - B) \mod N = 0)$
24	12 23	sylbid	$⊢ ((N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \land A - B = 0) \to (\|A - B\| \in (1 ..^N) \to \neg (A - B) \mod N = 0)$
25	24	ex	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to (A - B = 0 \to (\|A - B\| \in (1 ..^N) \to \neg (A - B) \mod N = 0))$
26	25	com23	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to (\|A - B\| \in (1 ..^N) \to (A - B = 0 \to \neg (A - B) \mod N = 0))$
27	26	3impia	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to (A - B = 0 \to \neg (A - B) \mod N = 0)$
28	9 27	sylbid	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to ((A - B) \mod N = 0 \to \neg (A - B) \mod N = 0)$
29	28	pm2.01d	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to \neg (A - B) \mod N = 0$
30		simp2	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to A \in ℤ$
31	30	adantl	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to A \in ℤ$
32		simp3	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to B \in ℤ$
33	32	adantl	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to B \in ℤ$
34		simpl	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to N \in ℕ$
35	31 33 34	3jca	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to (A \in ℤ \land B \in ℤ \land N \in ℕ)$
36	35	3adant3	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to (A \in ℤ \land B \in ℤ \land N \in ℕ)$
37		difmod0	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ) \to ((A - B) \mod N = 0 \leftrightarrow A \mod N = B \mod N)$
38	36 37	syl	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to ((A - B) \mod N = 0 \leftrightarrow A \mod N = B \mod N)$
39	29 38	mtbid	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to \neg A \mod N = B \mod N$
40		elfzoelz	$⊢ X \in (0 ..^N) \to X \in ℤ$
41	40 1	eleq2s	$⊢ X \in I \to X \in ℤ$
42	41	3ad2ant1	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to X \in ℤ$
43	42	zcnd	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to X \in ℂ$
44	30	zcnd	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to A \in ℂ$
45	43 44	addcomd	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to X + A = A + X$
46	45	oveq1d	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to (X + A) \mod N = (A + X) \mod N$
47	32	zcnd	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to B \in ℂ$
48	43 47	addcomd	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to X + B = B + X$
49	48	oveq1d	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to (X + B) \mod N = (B + X) \mod N$
50	46 49	eqeq12d	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to ((X + A) \mod N = (X + B) \mod N \leftrightarrow (A + X) \mod N = (B + X) \mod N)$
51	50	3ad2ant2	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to ((X + A) \mod N = (X + B) \mod N \leftrightarrow (A + X) \mod N = (B + X) \mod N)$
52		zre	$⊢ A \in ℤ \to A \in ℝ$
53		zre	$⊢ B \in ℤ \to B \in ℝ$
54	52 53	anim12i	$⊢ (A \in ℤ \land B \in ℤ) \to (A \in ℝ \land B \in ℝ)$
55	54	3adant1	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to (A \in ℝ \land B \in ℝ)$
56	55	adantl	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to (A \in ℝ \land B \in ℝ)$
57		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
58	41	zred	$⊢ X \in I \to X \in ℝ$
59	58	3ad2ant1	$⊢ (X \in I \land A \in ℤ \land B \in ℤ) \to X \in ℝ$
60	57 59	anim12ci	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to (X \in ℝ \land N \in ℝ^{+})$
61	56 60	jca	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ)) \to ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land N \in ℝ^{+}))$
62	61	3adant3	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land N \in ℝ^{+}))$
63		modaddb	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land N \in ℝ^{+})) \to (A \mod N = B \mod N \leftrightarrow (A + X) \mod N = (B + X) \mod N)$
64	62 63	syl	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to (A \mod N = B \mod N \leftrightarrow (A + X) \mod N = (B + X) \mod N)$
65	51 64	bitr4d	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to ((X + A) \mod N = (X + B) \mod N \leftrightarrow A \mod N = B \mod N)$
66	65	necon3abid	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to ((X + A) \mod N \neq (X + B) \mod N \leftrightarrow \neg A \mod N = B \mod N)$
67	39 66	mpbird	$⊢ (N \in ℕ \land (X \in I \land A \in ℤ \land B \in ℤ) \land \|A - B\| \in (1 ..^N)) \to (X + A) \mod N \neq (X + B) \mod N$

Metamath Proof Explorer

Theorem mod2addne

Proof