zplusmodne

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

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

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
2	1	3ad2ant1	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to N \in ℕ$
3		simp2	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to A \in ℤ$
4		elfzoelz	$⊢ K \in (1 ..^N) \to K \in ℤ$
5	4	3ad2ant3	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to K \in ℤ$
6	3 5	zaddcld	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to A + K \in ℤ$
7	3	zcnd	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to A \in ℂ$
8	4	zcnd	$⊢ K \in (1 ..^N) \to K \in ℂ$
9	8	3ad2ant3	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to K \in ℂ$
10	7 9	pncan2d	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to A + K - A = K$
11		elfzo1	$⊢ K \in (1 ..^N) \leftrightarrow (K \in ℕ \land N \in ℕ \land K < N)$
12		nnge1	$⊢ K \in ℕ \to 1 \leq K$
13	12	anim1i	$⊢ (K \in ℕ \land K < N) \to (1 \leq K \land K < N)$
14	13	3adant2	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to (1 \leq K \land K < N)$
15	11 14	sylbi	$⊢ K \in (1 ..^N) \to (1 \leq K \land K < N)$
16	15	3ad2ant3	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to (1 \leq K \land K < N)$
17	16	adantr	$⊢ ((N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \land A + K - A = K) \to (1 \leq K \land K < N)$
18		breq2	$⊢ A + K - A = K \to (1 \leq A + K - A \leftrightarrow 1 \leq K)$
19	18	adantl	$⊢ ((N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \land A + K - A = K) \to (1 \leq A + K - A \leftrightarrow 1 \leq K)$
20		breq1	$⊢ A + K - A = K \to (A + K - A < N \leftrightarrow K < N)$
21	20	adantl	$⊢ ((N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \land A + K - A = K) \to (A + K - A < N \leftrightarrow K < N)$
22	19 21	anbi12d	$⊢ ((N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \land A + K - A = K) \to ((1 \leq A + K - A \land A + K - A < N) \leftrightarrow (1 \leq K \land K < N))$
23	17 22	mpbird	$⊢ ((N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \land A + K - A = K) \to (1 \leq A + K - A \land A + K - A < N)$
24	10 23	mpdan	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to (1 \leq A + K - A \land A + K - A < N)$
25		difltmodne	$⊢ (N \in ℕ \land (A + K \in ℤ \land A \in ℤ) \land (1 \leq A + K - A \land A + K - A < N)) \to (A + K) \mod N \neq A \mod N$
26	2 6 3 24 25	syl121anc	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ \land K \in (1 ..^N)) \to (A + K) \mod N \neq A \mod N$

Metamath Proof Explorer

Theorem zplusmodne

Proof