Metamath Proof Explorer

Theorem gpg3kgrtriexlem2

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

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

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n ⊢ N = 3 ⁢ K
2 nnre ⊢ K ∈ ℕ → K ∈ ℝ
3 3rp ⊢ 3 ∈ ℝ +
4 3 a1i ⊢ K ∈ ℕ → 3 ∈ ℝ +
5 nnrp ⊢ K ∈ ℕ → K ∈ ℝ +
6 4 5 rpmulcld ⊢ K ∈ ℕ → 3 ⁢ K ∈ ℝ +
7 1 6 eqeltrid ⊢ K ∈ ℕ → N ∈ ℝ +
8 modaddmod ⊢ K ∈ ℝ ∧ K ∈ ℝ ∧ N ∈ ℝ + → K mod N + K mod N = K + K mod N
9 2 2 7 8 syl3anc ⊢ K ∈ ℕ → K mod N + K mod N = K + K mod N
10 nncn ⊢ K ∈ ℕ → K ∈ ℂ
11 10 2timesd ⊢ K ∈ ℕ → 2 ⁢ K = K + K
12 11 eqcomd ⊢ K ∈ ℕ → K + K = 2 ⁢ K
13 12 oveq1d ⊢ K ∈ ℕ → K + K mod N = 2 ⁢ K mod N
14 2cnd ⊢ K ∈ ℕ → 2 ∈ ℂ
15 14 10 adddirp1d ⊢ K ∈ ℕ → 2 + 1 ⁢ K = 2 ⁢ K + K
16 2p1e3 ⊢ 2 + 1 = 3
17 16 oveq1i ⊢ 2 + 1 ⁢ K = 3 ⁢ K
18 15 17 eqtr3di ⊢ K ∈ ℕ → 2 ⁢ K + K = 3 ⁢ K
19 18 oveq1d ⊢ K ∈ ℕ → 2 ⁢ K + K mod N = 3 ⁢ K mod N
20 1 a1i ⊢ K ∈ ℕ → N = 3 ⁢ K
21 20 oveq2d ⊢ K ∈ ℕ → 3 ⁢ K mod N = 3 ⁢ K mod 3 ⁢ K
22 modid0 ⊢ 3 ⁢ K ∈ ℝ + → 3 ⁢ K mod 3 ⁢ K = 0
23 6 22 syl ⊢ K ∈ ℕ → 3 ⁢ K mod 3 ⁢ K = 0
24 19 21 23 3eqtrd ⊢ K ∈ ℕ → 2 ⁢ K + K mod N = 0
25 2nn ⊢ 2 ∈ ℕ
26 25 a1i ⊢ K ∈ ℕ → 2 ∈ ℕ
27 id ⊢ K ∈ ℕ → K ∈ ℕ
28 26 27 nnmulcld ⊢ K ∈ ℕ → 2 ⁢ K ∈ ℕ
29 28 nnzd ⊢ K ∈ ℕ → 2 ⁢ K ∈ ℤ
30 nnz ⊢ K ∈ ℕ → K ∈ ℤ
31 3nn ⊢ 3 ∈ ℕ
32 31 a1i ⊢ K ∈ ℕ → 3 ∈ ℕ
33 32 27 nnmulcld ⊢ K ∈ ℕ → 3 ⁢ K ∈ ℕ
34 1 33 eqeltrid ⊢ K ∈ ℕ → N ∈ ℕ
35 summodnegmod ⊢ 2 ⁢ K ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℕ → 2 ⁢ K + K mod N = 0 ↔ 2 ⁢ K mod N = − K mod N
36 29 30 34 35 syl3anc ⊢ K ∈ ℕ → 2 ⁢ K + K mod N = 0 ↔ 2 ⁢ K mod N = − K mod N
37 24 36 mpbid ⊢ K ∈ ℕ → 2 ⁢ K mod N = − K mod N
38 9 13 37 3eqtrrd ⊢ K ∈ ℕ → − K mod N = K mod N + K mod N