Metamath Proof Explorer

Theorem gpg3kgrtriexlem5

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

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

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n 
 |-  N = ( 3 x. K )
2 3nn 
 |-  3 e. NN
3 2 a1i 
 |-  ( K e. NN -> 3 e. NN )
4 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
5 eluzfz2 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> 2 e. ( 1 ... 2 ) )
6 4 5 ax-mp 
 |-  2 e. ( 1 ... 2 )
7 3m1e2 
 |-  ( 3 - 1 ) = 2
8 7 oveq2i 
 |-  ( 1 ... ( 3 - 1 ) ) = ( 1 ... 2 )
9 6 8 eleqtrri 
 |-  2 e. ( 1 ... ( 3 - 1 ) )
10 9 a1i 
 |-  ( K e. NN -> 2 e. ( 1 ... ( 3 - 1 ) ) )
11 fzm1ndvds 
 |-  ( ( 3 e. NN /\ 2 e. ( 1 ... ( 3 - 1 ) ) ) -> -. 3 || 2 )
12 3 10 11 syl2anc 
 |-  ( K e. NN -> -. 3 || 2 )
13 3z 
 |-  3 e. ZZ
14 13 a1i 
 |-  ( K e. NN -> 3 e. ZZ )
15 2z 
 |-  2 e. ZZ
16 15 a1i 
 |-  ( K e. NN -> 2 e. ZZ )
17 nnz 
 |-  ( K e. NN -> K e. ZZ )
18 nnne0 
 |-  ( K e. NN -> K =/= 0 )
19 dvdsmulcr 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( 3 x. K ) || ( 2 x. K ) <-> 3 || 2 ) )
20 14 16 17 18 19 syl112anc 
 |-  ( K e. NN -> ( ( 3 x. K ) || ( 2 x. K ) <-> 3 || 2 ) )
21 12 20 mtbird 
 |-  ( K e. NN -> -. ( 3 x. K ) || ( 2 x. K ) )
22 1 breq1i 
 |-  ( N || ( 2 x. K ) <-> ( 3 x. K ) || ( 2 x. K ) )
23 21 22 sylnibr 
 |-  ( K e. NN -> -. N || ( 2 x. K ) )
24 id 
 |-  ( K e. NN -> K e. NN )
25 3 24 nnmulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. NN )
26 1 25 eqeltrid 
 |-  ( K e. NN -> N e. NN )
27 2nn 
 |-  2 e. NN
28 27 a1i 
 |-  ( K e. NN -> 2 e. NN )
29 28 24 nnmulcld 
 |-  ( K e. NN -> ( 2 x. K ) e. NN )
30 29 nnzd 
 |-  ( K e. NN -> ( 2 x. K ) e. ZZ )
31 dvdsval3 
 |-  ( ( N e. NN /\ ( 2 x. K ) e. ZZ ) -> ( N || ( 2 x. K ) <-> ( ( 2 x. K ) mod N ) = 0 ) )
32 26 30 31 syl2anc 
 |-  ( K e. NN -> ( N || ( 2 x. K ) <-> ( ( 2 x. K ) mod N ) = 0 ) )
33 nncn 
 |-  ( K e. NN -> K e. CC )
34 33 2timesd 
 |-  ( K e. NN -> ( 2 x. K ) = ( K + K ) )
35 34 oveq1d 
 |-  ( K e. NN -> ( ( 2 x. K ) mod N ) = ( ( K + K ) mod N ) )
36 35 eqeq1d 
 |-  ( K e. NN -> ( ( ( 2 x. K ) mod N ) = 0 <-> ( ( K + K ) mod N ) = 0 ) )
37 summodnegmod 
 |-  ( ( K e. ZZ /\ K e. ZZ /\ N e. NN ) -> ( ( ( K + K ) mod N ) = 0 <-> ( K mod N ) = ( -u K mod N ) ) )
38 17 17 26 37 syl3anc 
 |-  ( K e. NN -> ( ( ( K + K ) mod N ) = 0 <-> ( K mod N ) = ( -u K mod N ) ) )
39 32 36 38 3bitrd 
 |-  ( K e. NN -> ( N || ( 2 x. K ) <-> ( K mod N ) = ( -u K mod N ) ) )
40 23 39 mtbid 
 |-  ( K e. NN -> -. ( K mod N ) = ( -u K mod N ) )
41 40 neqned 
 |-  ( K e. NN -> ( K mod N ) =/= ( -u K mod N ) )