Metamath Proof Explorer

Theorem gpg3kgrtriexlem5

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

Ref Expression
Hypothesis gpg3kgrtriex.n ⊢ N = 3 ⁢ K
Assertion gpg3kgrtriexlem5 ⊢ K ∈ ℕ → K mod N ≠ − K mod N

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n ⊢ N = 3 ⁢ K
2 3nn ⊢ 3 ∈ ℕ
3 2 a1i ⊢ K ∈ ℕ → 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 ⊢ K ∈ ℕ → 2 ∈ 1 … 3 − 1
11 fzm1ndvds ⊢ 3 ∈ ℕ ∧ 2 ∈ 1 … 3 − 1 → ¬ 3 ∥ 2
12 3 10 11 syl2anc ⊢ K ∈ ℕ → ¬ 3 ∥ 2
13 3z ⊢ 3 ∈ ℤ
14 13 a1i ⊢ K ∈ ℕ → 3 ∈ ℤ
15 2z ⊢ 2 ∈ ℤ
16 15 a1i ⊢ K ∈ ℕ → 2 ∈ ℤ
17 nnz ⊢ K ∈ ℕ → K ∈ ℤ
18 nnne0 ⊢ K ∈ ℕ → K ≠ 0
19 dvdsmulcr ⊢ 3 ∈ ℤ ∧ 2 ∈ ℤ ∧ K ∈ ℤ ∧ K ≠ 0 → 3 ⁢ K ∥ 2 ⁢ K ↔ 3 ∥ 2
20 14 16 17 18 19 syl112anc ⊢ K ∈ ℕ → 3 ⁢ K ∥ 2 ⁢ K ↔ 3 ∥ 2
21 12 20 mtbird ⊢ K ∈ ℕ → ¬ 3 ⁢ K ∥ 2 ⁢ K
22 1 breq1i ⊢ N ∥ 2 ⁢ K ↔ 3 ⁢ K ∥ 2 ⁢ K
23 21 22 sylnibr ⊢ K ∈ ℕ → ¬ N ∥ 2 ⁢ K
24 id ⊢ K ∈ ℕ → K ∈ ℕ
25 3 24 nnmulcld ⊢ K ∈ ℕ → 3 ⁢ K ∈ ℕ
26 1 25 eqeltrid ⊢ K ∈ ℕ → N ∈ ℕ
27 2nn ⊢ 2 ∈ ℕ
28 27 a1i ⊢ K ∈ ℕ → 2 ∈ ℕ
29 28 24 nnmulcld ⊢ K ∈ ℕ → 2 ⁢ K ∈ ℕ
30 29 nnzd ⊢ K ∈ ℕ → 2 ⁢ K ∈ ℤ
31 dvdsval3 ⊢ N ∈ ℕ ∧ 2 ⁢ K ∈ ℤ → N ∥ 2 ⁢ K ↔ 2 ⁢ K mod N = 0
32 26 30 31 syl2anc ⊢ K ∈ ℕ → N ∥ 2 ⁢ K ↔ 2 ⁢ K mod N = 0
33 nncn ⊢ K ∈ ℕ → K ∈ ℂ
34 33 2timesd ⊢ K ∈ ℕ → 2 ⁢ K = K + K
35 34 oveq1d ⊢ K ∈ ℕ → 2 ⁢ K mod N = K + K mod N
36 35 eqeq1d ⊢ K ∈ ℕ → 2 ⁢ K mod N = 0 ↔ K + K mod N = 0
37 summodnegmod ⊢ K ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℕ → K + K mod N = 0 ↔ K mod N = − K mod N
38 17 17 26 37 syl3anc ⊢ K ∈ ℕ → K + K mod N = 0 ↔ K mod N = − K mod N
39 32 36 38 3bitrd ⊢ K ∈ ℕ → N ∥ 2 ⁢ K ↔ K mod N = − K mod N
40 23 39 mtbid ⊢ K ∈ ℕ → ¬ K mod N = − K mod N
41 40 neqned ⊢ K ∈ ℕ → K mod N ≠ − K mod N