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

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
2	1	3ad2ant1	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ )
3		simp2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → 𝐴 ∈ ℤ )
4		elfzoelz	⊢ ( 𝐾 ∈ ( 1 ..^ 𝑁 ) → 𝐾 ∈ ℤ )
5	4	3ad2ant3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → 𝐾 ∈ ℤ )
6	3 5	zaddcld	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐴 + 𝐾 ) ∈ ℤ )
7	3	zcnd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → 𝐴 ∈ ℂ )
8	4	zcnd	⊢ ( 𝐾 ∈ ( 1 ..^ 𝑁 ) → 𝐾 ∈ ℂ )
9	8	3ad2ant3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → 𝐾 ∈ ℂ )
10	7 9	pncan2d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝐴 + 𝐾 ) − 𝐴 ) = 𝐾 )
11		elfzo1	⊢ ( 𝐾 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
12		nnge1	⊢ ( 𝐾 ∈ ℕ → 1 ≤ 𝐾 )
13	12	anim1i	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( 1 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) )
14	13	3adant2	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( 1 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) )
15	11 14	sylbi	⊢ ( 𝐾 ∈ ( 1 ..^ 𝑁 ) → ( 1 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) )
16	15	3ad2ant3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → ( 1 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) )
17	16	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) ∧ ( ( 𝐴 + 𝐾 ) − 𝐴 ) = 𝐾 ) → ( 1 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) )
18		breq2	⊢ ( ( ( 𝐴 + 𝐾 ) − 𝐴 ) = 𝐾 → ( 1 ≤ ( ( 𝐴 + 𝐾 ) − 𝐴 ) ↔ 1 ≤ 𝐾 ) )
19	18	adantl	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) ∧ ( ( 𝐴 + 𝐾 ) − 𝐴 ) = 𝐾 ) → ( 1 ≤ ( ( 𝐴 + 𝐾 ) − 𝐴 ) ↔ 1 ≤ 𝐾 ) )
20		breq1	⊢ ( ( ( 𝐴 + 𝐾 ) − 𝐴 ) = 𝐾 → ( ( ( 𝐴 + 𝐾 ) − 𝐴 ) < 𝑁 ↔ 𝐾 < 𝑁 ) )
21	20	adantl	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) ∧ ( ( 𝐴 + 𝐾 ) − 𝐴 ) = 𝐾 ) → ( ( ( 𝐴 + 𝐾 ) − 𝐴 ) < 𝑁 ↔ 𝐾 < 𝑁 ) )
22	19 21	anbi12d	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) ∧ ( ( 𝐴 + 𝐾 ) − 𝐴 ) = 𝐾 ) → ( ( 1 ≤ ( ( 𝐴 + 𝐾 ) − 𝐴 ) ∧ ( ( 𝐴 + 𝐾 ) − 𝐴 ) < 𝑁 ) ↔ ( 1 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
23	17 22	mpbird	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) ∧ ( ( 𝐴 + 𝐾 ) − 𝐴 ) = 𝐾 ) → ( 1 ≤ ( ( 𝐴 + 𝐾 ) − 𝐴 ) ∧ ( ( 𝐴 + 𝐾 ) − 𝐴 ) < 𝑁 ) )
24	10 23	mpdan	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → ( 1 ≤ ( ( 𝐴 + 𝐾 ) − 𝐴 ) ∧ ( ( 𝐴 + 𝐾 ) − 𝐴 ) < 𝑁 ) )
25		difltmodne	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 + 𝐾 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( 1 ≤ ( ( 𝐴 + 𝐾 ) − 𝐴 ) ∧ ( ( 𝐴 + 𝐾 ) − 𝐴 ) < 𝑁 ) ) → ( ( 𝐴 + 𝐾 ) mod 𝑁 ) ≠ ( 𝐴 mod 𝑁 ) )
26	2 6 3 24 25	syl121anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝐴 + 𝐾 ) mod 𝑁 ) ≠ ( 𝐴 mod 𝑁 ) )