Metamath Proof Explorer

Theorem p1modne

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

		Ref	Expression
	Assertion	p1modne	$⊢ (N \in ℤ_{\geq 2} \land A \in (0 ..^N)) \to (A + 1) \mod N \neq A$

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	$⊢ A \in (0 ..^N) \to A \in ℤ$
2		zp1modne	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to (A + 1) \mod N \neq A \mod N$
3	1 2	sylan2	$⊢ (N \in ℤ_{\geq 2} \land A \in (0 ..^N)) \to (A + 1) \mod N \neq A \mod N$
4		zmodidfzoimp	$⊢ A \in (0 ..^N) \to A \mod N = A$
5	4	adantl	$⊢ (N \in ℤ_{\geq 2} \land A \in (0 ..^N)) \to A \mod N = A$
6	3 5	neeqtrd	$⊢ (N \in ℤ_{\geq 2} \land A \in (0 ..^N)) \to (A + 1) \mod N \neq A$