Metamath Proof Explorer

Theorem zp1modne

Description: An integer is not itself plus 1 modulo an integer greater than 1. (Contributed by AV, 6-Sep-2025)

Ref Expression
Assertion zp1modne ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ ℤ → A + 1 mod N ≠ A mod N

Proof

Step Hyp Ref Expression
1 fzo1lb ⊢ 1 ∈ 1 ..^ N ↔ N ∈ ℤ ≥ 2
2 1 biranri ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ ℤ → 1 ∈ 1 ..^ N
3 zplusmodne ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ ℤ ∧ 1 ∈ 1 ..^ N → A + 1 mod N ≠ A mod N
4 2 3 mpd3an3 ⊢ N ∈ ℤ ≥ 2 ∧ A ∈ ℤ → A + 1 mod N ≠ A mod N