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 ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 − 1 ) mod 𝑁 ) ≠ 𝐴 )

Proof

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