Metamath Proof Explorer

Theorem modp2nep1

Description: A nonnegative integer less than a modulus greater than 4 plus one/plus two are not equal modulo the modulus. (Contributed by AV, 22-Nov-2025)

Ref Expression
Hypothesis modm1nep1.i ⊢ I = 0 ..^ N
Assertion modp2nep1 ⊢ N ∈ ℤ ≥ 5 ∧ Y ∈ I → Y + 2 mod N ≠ Y + 1 mod N

Proof

Step Hyp Ref Expression
1 modm1nep1.i ⊢ I = 0 ..^ N
2 eluz5nn ⊢ N ∈ ℤ ≥ 5 → N ∈ ℕ
3 2 adantr ⊢ N ∈ ℤ ≥ 5 ∧ Y ∈ I → N ∈ ℕ
4 simpr ⊢ N ∈ ℤ ≥ 5 ∧ Y ∈ I → Y ∈ I
5 2z ⊢ 2 ∈ ℤ
6 5 a1i ⊢ N ∈ ℤ ≥ 5 ∧ Y ∈ I → 2 ∈ ℤ
7 1zzd ⊢ N ∈ ℤ ≥ 5 ∧ Y ∈ I → 1 ∈ ℤ
8 2m1e1 ⊢ 2 − 1 = 1
9 8 fveq2i ⊢ 2 − 1 = 1
10 abs1 ⊢ 1 = 1
11 9 10 eqtri ⊢ 2 − 1 = 1
12 eluz2 ⊢ N ∈ ℤ ≥ 5 ↔ 5 ∈ ℤ ∧ N ∈ ℤ ∧ 5 ≤ N
13 1red ⊢ 5 ∈ ℤ ∧ N ∈ ℤ ∧ 5 ≤ N → 1 ∈ ℝ
14 5re ⊢ 5 ∈ ℝ
15 14 a1i ⊢ 5 ∈ ℤ ∧ N ∈ ℤ ∧ 5 ≤ N → 5 ∈ ℝ
16 zre ⊢ N ∈ ℤ → N ∈ ℝ
17 16 3ad2ant2 ⊢ 5 ∈ ℤ ∧ N ∈ ℤ ∧ 5 ≤ N → N ∈ ℝ
18 1lt5 ⊢ 1 < 5
19 18 a1i ⊢ 5 ∈ ℤ ∧ N ∈ ℤ ∧ 5 ≤ N → 1 < 5
20 simp3 ⊢ 5 ∈ ℤ ∧ N ∈ ℤ ∧ 5 ≤ N → 5 ≤ N
21 13 15 17 19 20 ltletrd ⊢ 5 ∈ ℤ ∧ N ∈ ℤ ∧ 5 ≤ N → 1 < N
22 12 21 sylbi ⊢ N ∈ ℤ ≥ 5 → 1 < N
23 1elfzo1 ⊢ 1 ∈ 1 ..^ N ↔ N ∈ ℕ ∧ 1 < N
24 2 22 23 sylanbrc ⊢ N ∈ ℤ ≥ 5 → 1 ∈ 1 ..^ N
25 24 adantr ⊢ N ∈ ℤ ≥ 5 ∧ Y ∈ I → 1 ∈ 1 ..^ N
26 11 25 eqeltrid ⊢ N ∈ ℤ ≥ 5 ∧ Y ∈ I → 2 − 1 ∈ 1 ..^ N
27 1 mod2addne ⊢ N ∈ ℕ ∧ Y ∈ I ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ ∧ 2 − 1 ∈ 1 ..^ N → Y + 2 mod N ≠ Y + 1 mod N
28 3 4 6 7 26 27 syl131anc ⊢ N ∈ ℤ ≥ 5 ∧ Y ∈ I → Y + 2 mod N ≠ Y + 1 mod N