Theorem modm1p1ne

Description: If an integer minus one equals another integer plus one modulo an integer greater than 4, then the first integer plus one is not equal to the second integer minus one modulo the same modulus. (Contributed by AV, 15-Nov-2025)

	Ref	Expression
Hypothesis	modm1nep1.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	modm1p1ne	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) → ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ ( ( 𝑋 − 1 ) mod 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		modm1nep1.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ↔ ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) )
3		4nn0	⊢ 4 ∈ ℕ0
4	3	a1i	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 4 ∈ ℕ0 )
5		simp2	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 𝑁 ∈ ℤ )
6		0red	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 0 ∈ ℝ )
7		5re	⊢ 5 ∈ ℝ
8	7	a1i	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 5 ∈ ℝ )
9		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
10	9	3ad2ant2	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
11		5pos	⊢ 0 < 5
12	11	a1i	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 0 < 5 )
13		simp3	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 5 ≤ 𝑁 )
14	6 8 10 12 13	ltletrd	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 0 < 𝑁 )
15		elnnz	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
16	5 14 15	sylanbrc	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 𝑁 ∈ ℕ )
17		4re	⊢ 4 ∈ ℝ
18	17	a1i	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 4 ∈ ℝ )
19		4lt5	⊢ 4 < 5
20	19	a1i	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 4 < 5 )
21	18 8 10 20 13	ltletrd	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 4 < 𝑁 )
22		elfzo0	⊢ ( 4 ∈ ( 0 ..^ 𝑁 ) ↔ ( 4 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 4 < 𝑁 ) )
23	4 16 21 22	syl3anbrc	⊢ ( ( 5 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) → 4 ∈ ( 0 ..^ 𝑁 ) )
24	2 23	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 4 ∈ ( 0 ..^ 𝑁 ) )
25		zmodidfzoimp	⊢ ( 4 ∈ ( 0 ..^ 𝑁 ) → ( 4 mod 𝑁 ) = 4 )
26	24 25	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → ( 4 mod 𝑁 ) = 4 )
27		4ne0	⊢ 4 ≠ 0
28	27	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 4 ≠ 0 )
29	26 28	eqnetrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → ( 4 mod 𝑁 ) ≠ 0 )
30		df-ne	⊢ ( ( ( 4 · 1 ) mod 𝑁 ) ≠ 0 ↔ ¬ ( ( 4 · 1 ) mod 𝑁 ) = 0 )
31		4cn	⊢ 4 ∈ ℂ
32	31	mulridi	⊢ ( 4 · 1 ) = 4
33	32	oveq1i	⊢ ( ( 4 · 1 ) mod 𝑁 ) = ( 4 mod 𝑁 )
34	33	neeq1i	⊢ ( ( ( 4 · 1 ) mod 𝑁 ) ≠ 0 ↔ ( 4 mod 𝑁 ) ≠ 0 )
35	30 34	bitr3i	⊢ ( ¬ ( ( 4 · 1 ) mod 𝑁 ) = 0 ↔ ( 4 mod 𝑁 ) ≠ 0 )
36	29 35	sylibr	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → ¬ ( ( 4 · 1 ) mod 𝑁 ) = 0 )
37	36	3ad2ant1	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ¬ ( ( 4 · 1 ) mod 𝑁 ) = 0 )
38	37	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) → ¬ ( ( 4 · 1 ) mod 𝑁 ) = 0 )
39		uzuzle35	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
40		eluz3nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
41	39 40	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 𝑁 ∈ ℕ )
42	41	3ad2ant1	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → 𝑁 ∈ ℕ )
43		elfzoelz	⊢ ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → 𝑋 ∈ ℤ )
44	43 1	eleq2s	⊢ ( 𝑋 ∈ 𝐼 → 𝑋 ∈ ℤ )
45	44	3ad2ant2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → 𝑋 ∈ ℤ )
46		elfzoelz	⊢ ( 𝑌 ∈ ( 0 ..^ 𝑁 ) → 𝑌 ∈ ℤ )
47	46 1	eleq2s	⊢ ( 𝑌 ∈ 𝐼 → 𝑌 ∈ ℤ )
48	47	3ad2ant3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → 𝑌 ∈ ℤ )
49		1zzd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → 1 ∈ ℤ )
50		modmkpkne	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) ↔ ( ( 4 · 1 ) mod 𝑁 ) = 0 ) ) )
51	42 45 48 49 50	syl13anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) ↔ ( ( 4 · 1 ) mod 𝑁 ) = 0 ) ) )
52	51	imp	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) ↔ ( ( 4 · 1 ) mod 𝑁 ) = 0 ) )
53	38 52	mtbird	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) → ¬ ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) )
54	53	neqned	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) → ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ ( ( 𝑋 − 1 ) mod 𝑁 ) )
55	54	ex	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) → ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ ( ( 𝑋 − 1 ) mod 𝑁 ) ) )