Theorem gpg3kgrtriexlem5

Description: Lemma 5 for gpg3kgrtriex . (Contributed by AV, 1-Oct-2025)

	Ref	Expression
Hypothesis	gpg3kgrtriex.n	⊢ 𝑁 = ( 3 · 𝐾 )
Assertion	gpg3kgrtriexlem5	⊢ ( 𝐾 ∈ ℕ → ( 𝐾 mod 𝑁 ) ≠ ( - 𝐾 mod 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		gpg3kgrtriex.n	⊢ 𝑁 = ( 3 · 𝐾 )
2		3nn	⊢ 3 ∈ ℕ
3	2	a1i	⊢ ( 𝐾 ∈ ℕ → 3 ∈ ℕ )
4		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
5		eluzfz2	⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 2 ∈ ( 1 ... 2 ) )
6	4 5	ax-mp	⊢ 2 ∈ ( 1 ... 2 )
7		3m1e2	⊢ ( 3 − 1 ) = 2
8	7	oveq2i	⊢ ( 1 ... ( 3 − 1 ) ) = ( 1 ... 2 )
9	6 8	eleqtrri	⊢ 2 ∈ ( 1 ... ( 3 − 1 ) )
10	9	a1i	⊢ ( 𝐾 ∈ ℕ → 2 ∈ ( 1 ... ( 3 − 1 ) ) )
11		fzm1ndvds	⊢ ( ( 3 ∈ ℕ ∧ 2 ∈ ( 1 ... ( 3 − 1 ) ) ) → ¬ 3 ∥ 2 )
12	3 10 11	syl2anc	⊢ ( 𝐾 ∈ ℕ → ¬ 3 ∥ 2 )
13		3z	⊢ 3 ∈ ℤ
14	13	a1i	⊢ ( 𝐾 ∈ ℕ → 3 ∈ ℤ )
15		2z	⊢ 2 ∈ ℤ
16	15	a1i	⊢ ( 𝐾 ∈ ℕ → 2 ∈ ℤ )
17		nnz	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
18		nnne0	⊢ ( 𝐾 ∈ ℕ → 𝐾 ≠ 0 )
19		dvdsmulcr	⊢ ( ( 3 ∈ ℤ ∧ 2 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 3 · 𝐾 ) ∥ ( 2 · 𝐾 ) ↔ 3 ∥ 2 ) )
20	14 16 17 18 19	syl112anc	⊢ ( 𝐾 ∈ ℕ → ( ( 3 · 𝐾 ) ∥ ( 2 · 𝐾 ) ↔ 3 ∥ 2 ) )
21	12 20	mtbird	⊢ ( 𝐾 ∈ ℕ → ¬ ( 3 · 𝐾 ) ∥ ( 2 · 𝐾 ) )
22	1	breq1i	⊢ ( 𝑁 ∥ ( 2 · 𝐾 ) ↔ ( 3 · 𝐾 ) ∥ ( 2 · 𝐾 ) )
23	21 22	sylnibr	⊢ ( 𝐾 ∈ ℕ → ¬ 𝑁 ∥ ( 2 · 𝐾 ) )
24		id	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ )
25	3 24	nnmulcld	⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ℕ )
26	1 25	eqeltrid	⊢ ( 𝐾 ∈ ℕ → 𝑁 ∈ ℕ )
27		2nn	⊢ 2 ∈ ℕ
28	27	a1i	⊢ ( 𝐾 ∈ ℕ → 2 ∈ ℕ )
29	28 24	nnmulcld	⊢ ( 𝐾 ∈ ℕ → ( 2 · 𝐾 ) ∈ ℕ )
30	29	nnzd	⊢ ( 𝐾 ∈ ℕ → ( 2 · 𝐾 ) ∈ ℤ )
31		dvdsval3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 2 · 𝐾 ) ∈ ℤ ) → ( 𝑁 ∥ ( 2 · 𝐾 ) ↔ ( ( 2 · 𝐾 ) mod 𝑁 ) = 0 ) )
32	26 30 31	syl2anc	⊢ ( 𝐾 ∈ ℕ → ( 𝑁 ∥ ( 2 · 𝐾 ) ↔ ( ( 2 · 𝐾 ) mod 𝑁 ) = 0 ) )
33		nncn	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℂ )
34	33	2timesd	⊢ ( 𝐾 ∈ ℕ → ( 2 · 𝐾 ) = ( 𝐾 + 𝐾 ) )
35	34	oveq1d	⊢ ( 𝐾 ∈ ℕ → ( ( 2 · 𝐾 ) mod 𝑁 ) = ( ( 𝐾 + 𝐾 ) mod 𝑁 ) )
36	35	eqeq1d	⊢ ( 𝐾 ∈ ℕ → ( ( ( 2 · 𝐾 ) mod 𝑁 ) = 0 ↔ ( ( 𝐾 + 𝐾 ) mod 𝑁 ) = 0 ) )
37		summodnegmod	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐾 + 𝐾 ) mod 𝑁 ) = 0 ↔ ( 𝐾 mod 𝑁 ) = ( - 𝐾 mod 𝑁 ) ) )
38	17 17 26 37	syl3anc	⊢ ( 𝐾 ∈ ℕ → ( ( ( 𝐾 + 𝐾 ) mod 𝑁 ) = 0 ↔ ( 𝐾 mod 𝑁 ) = ( - 𝐾 mod 𝑁 ) ) )
39	32 36 38	3bitrd	⊢ ( 𝐾 ∈ ℕ → ( 𝑁 ∥ ( 2 · 𝐾 ) ↔ ( 𝐾 mod 𝑁 ) = ( - 𝐾 mod 𝑁 ) ) )
40	23 39	mtbid	⊢ ( 𝐾 ∈ ℕ → ¬ ( 𝐾 mod 𝑁 ) = ( - 𝐾 mod 𝑁 ) )
41	40	neqned	⊢ ( 𝐾 ∈ ℕ → ( 𝐾 mod 𝑁 ) ≠ ( - 𝐾 mod 𝑁 ) )