Metamath Proof Explorer

Theorem gpg3kgrtriexlem2

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

Ref Expression
Hypothesis gpg3kgrtriex.n 
|- N = ( 3 x. K )
Assertion gpg3kgrtriexlem2 
|- ( K e. NN -> ( -u K mod N ) = ( ( ( K mod N ) + K ) mod N ) )

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n 
 |-  N = ( 3 x. K )
2 nnre 
 |-  ( K e. NN -> K e. RR )
3 3rp 
 |-  3 e. RR+
4 3 a1i 
 |-  ( K e. NN -> 3 e. RR+ )
5 nnrp 
 |-  ( K e. NN -> K e. RR+ )
6 4 5 rpmulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. RR+ )
7 1 6 eqeltrid 
 |-  ( K e. NN -> N e. RR+ )
8 modaddmod 
 |-  ( ( K e. RR /\ K e. RR /\ N e. RR+ ) -> ( ( ( K mod N ) + K ) mod N ) = ( ( K + K ) mod N ) )
9 2 2 7 8 syl3anc 
 |-  ( K e. NN -> ( ( ( K mod N ) + K ) mod N ) = ( ( K + K ) mod N ) )
10 nncn 
 |-  ( K e. NN -> K e. CC )
11 10 2timesd 
 |-  ( K e. NN -> ( 2 x. K ) = ( K + K ) )
12 11 eqcomd 
 |-  ( K e. NN -> ( K + K ) = ( 2 x. K ) )
13 12 oveq1d 
 |-  ( K e. NN -> ( ( K + K ) mod N ) = ( ( 2 x. K ) mod N ) )
14 2cnd 
 |-  ( K e. NN -> 2 e. CC )
15 14 10 adddirp1d 
 |-  ( K e. NN -> ( ( 2 + 1 ) x. K ) = ( ( 2 x. K ) + K ) )
16 2p1e3 
 |-  ( 2 + 1 ) = 3
17 16 oveq1i 
 |-  ( ( 2 + 1 ) x. K ) = ( 3 x. K )
18 15 17 eqtr3di 
 |-  ( K e. NN -> ( ( 2 x. K ) + K ) = ( 3 x. K ) )
19 18 oveq1d 
 |-  ( K e. NN -> ( ( ( 2 x. K ) + K ) mod N ) = ( ( 3 x. K ) mod N ) )
20 1 a1i 
 |-  ( K e. NN -> N = ( 3 x. K ) )
21 20 oveq2d 
 |-  ( K e. NN -> ( ( 3 x. K ) mod N ) = ( ( 3 x. K ) mod ( 3 x. K ) ) )
22 modid0 
 |-  ( ( 3 x. K ) e. RR+ -> ( ( 3 x. K ) mod ( 3 x. K ) ) = 0 )
23 6 22 syl 
 |-  ( K e. NN -> ( ( 3 x. K ) mod ( 3 x. K ) ) = 0 )
24 19 21 23 3eqtrd 
 |-  ( K e. NN -> ( ( ( 2 x. K ) + K ) mod N ) = 0 )
25 2nn 
 |-  2 e. NN
26 25 a1i 
 |-  ( K e. NN -> 2 e. NN )
27 id 
 |-  ( K e. NN -> K e. NN )
28 26 27 nnmulcld 
 |-  ( K e. NN -> ( 2 x. K ) e. NN )
29 28 nnzd 
 |-  ( K e. NN -> ( 2 x. K ) e. ZZ )
30 nnz 
 |-  ( K e. NN -> K e. ZZ )
31 3nn 
 |-  3 e. NN
32 31 a1i 
 |-  ( K e. NN -> 3 e. NN )
33 32 27 nnmulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. NN )
34 1 33 eqeltrid 
 |-  ( K e. NN -> N e. NN )
35 summodnegmod 
 |-  ( ( ( 2 x. K ) e. ZZ /\ K e. ZZ /\ N e. NN ) -> ( ( ( ( 2 x. K ) + K ) mod N ) = 0 <-> ( ( 2 x. K ) mod N ) = ( -u K mod N ) ) )
36 29 30 34 35 syl3anc 
 |-  ( K e. NN -> ( ( ( ( 2 x. K ) + K ) mod N ) = 0 <-> ( ( 2 x. K ) mod N ) = ( -u K mod N ) ) )
37 24 36 mpbid 
 |-  ( K e. NN -> ( ( 2 x. K ) mod N ) = ( -u K mod N ) )
38 9 13 37 3eqtrrd 
 |-  ( K e. NN -> ( -u K mod N ) = ( ( ( K mod N ) + K ) mod N ) )