Metamath Proof Explorer

Theorem m1modne

Description: A nonnegative integer is not itself minus 1 modulo an integer greater than 1 and the nonnegative integer. (Contributed by AV, 6-Sep-2025)

Ref Expression
Assertion m1modne ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → A − 1 mod N ≠ A

Proof

Step Hyp Ref Expression
1 eluz2nn ⊢ N ∈ ℤ ≥ 2 → N ∈ ℕ
2 1 adantr ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → N ∈ ℕ
3 elfzoelz ⊢ A ∈ 0 ..^ N → A ∈ ℤ
4 1zzd ⊢ A ∈ 0 ..^ N → 1 ∈ ℤ
5 3 4 zsubcld ⊢ A ∈ 0 ..^ N → A − 1 ∈ ℤ
6 3 5 jca ⊢ A ∈ 0 ..^ N → A ∈ ℤ ∧ A − 1 ∈ ℤ
7 6 adantl ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → A ∈ ℤ ∧ A − 1 ∈ ℤ
8 3 zcnd ⊢ A ∈ 0 ..^ N → A ∈ ℂ
9 8 adantl ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → A ∈ ℂ
10 1cnd ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → 1 ∈ ℂ
11 9 10 nncand ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → A − A − 1 = 1
12 1le1 ⊢ 1 ≤ 1
13 breq2 ⊢ A − A − 1 = 1 → 1 ≤ A − A − 1 ↔ 1 ≤ 1
14 13 adantl ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N ∧ A − A − 1 = 1 → 1 ≤ A − A − 1 ↔ 1 ≤ 1
15 12 14 mpbiri ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N ∧ A − A − 1 = 1 → 1 ≤ A − A − 1
16 eluz2gt1 ⊢ N ∈ ℤ ≥ 2 → 1 < N
17 16 adantr ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → 1 < N
18 17 adantr ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N ∧ A − A − 1 = 1 → 1 < N
19 breq1 ⊢ A − A − 1 = 1 → A − A − 1 < N ↔ 1 < N
20 19 adantl ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N ∧ A − A − 1 = 1 → A − A − 1 < N ↔ 1 < N
21 18 20 mpbird ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N ∧ A − A − 1 = 1 → A − A − 1 < N
22 15 21 jca ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N ∧ A − A − 1 = 1 → 1 ≤ A − A − 1 ∧ A − A − 1 < N
23 11 22 mpdan ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → 1 ≤ A − A − 1 ∧ A − A − 1 < N
24 difltmodne ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ A − 1 ∈ ℤ ∧ 1 ≤ A − A − 1 ∧ A − A − 1 < N → A mod N ≠ A − 1 mod N
25 2 7 23 24 syl3anc ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → A mod N ≠ A − 1 mod N
26 25 necomd ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → A − 1 mod N ≠ A mod N
27 zmodidfzoimp ⊢ A ∈ 0 ..^ N → A mod N = A
28 27 adantl ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → A mod N = A
29 26 28 neeqtrd ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ 0 ..^ N → A − 1 mod N ≠ A