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