Metamath Proof Explorer

Theorem gpg3nbgrvtxlem

Description: Lemma for gpg3nbgrvtx0ALT and gpg3nbgrvtx1 . For this theorem, it is essential that 2 < N and K < ( N / 2 ) ! (Contributed by AV, 3-Sep-2025) (Proof shortened by AV, 9-Sep-2025)

Ref Expression
Assertion gpg3nbgrvtxlem 
|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) /\ A e. ( 0 ..^ N ) ) -> ( ( A + K ) mod N ) =/= ( ( A - K ) mod N ) )

Proof

Step Hyp Ref Expression
1 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
2 1 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) /\ A e. ( 0 ..^ N ) ) -> N e. NN )
3 elfzoelz 
 |-  ( A e. ( 0 ..^ N ) -> A e. ZZ )
4 3 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) /\ A e. ( 0 ..^ N ) ) -> A e. ZZ )
5 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
6 5 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) /\ A e. ( 0 ..^ N ) ) -> K e. ZZ )
7 5 zcnd 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. CC )
8 2times 
 |-  ( K e. CC -> ( 2 x. K ) = ( K + K ) )
9 8 eqcomd 
 |-  ( K e. CC -> ( K + K ) = ( 2 x. K ) )
10 7 9 syl 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> ( K + K ) = ( 2 x. K ) )
11 10 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( K + K ) = ( 2 x. K ) )
12 1red 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> 1 e. RR )
13 5 zred 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. RR )
14 2z 
 |-  2 e. ZZ
15 14 a1i 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> 2 e. ZZ )
16 15 5 zmulcld 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> ( 2 x. K ) e. ZZ )
17 16 zred 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> ( 2 x. K ) e. RR )
18 elfzole1 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> 1 <_ K )
19 elfzo1 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) )
20 19 simp1bi 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. NN )
21 20 nnnn0d 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. NN0 )
22 nn0le2x 
 |-  ( K e. NN0 -> K <_ ( 2 x. K ) )
23 21 22 syl 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K <_ ( 2 x. K ) )
24 12 13 17 18 23 letrd 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> 1 <_ ( 2 x. K ) )
25 24 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> 1 <_ ( 2 x. K ) )
26 2tceilhalfelfzo1 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( 2 x. K ) < N )
27 25 26 jca 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( 1 <_ ( 2 x. K ) /\ ( 2 x. K ) < N ) )
28 breq2 
 |-  ( ( K + K ) = ( 2 x. K ) -> ( 1 <_ ( K + K ) <-> 1 <_ ( 2 x. K ) ) )
29 breq1 
 |-  ( ( K + K ) = ( 2 x. K ) -> ( ( K + K ) < N <-> ( 2 x. K ) < N ) )
30 28 29 anbi12d 
 |-  ( ( K + K ) = ( 2 x. K ) -> ( ( 1 <_ ( K + K ) /\ ( K + K ) < N ) <-> ( 1 <_ ( 2 x. K ) /\ ( 2 x. K ) < N ) ) )
31 27 30 syl5ibrcom 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( ( K + K ) = ( 2 x. K ) -> ( 1 <_ ( K + K ) /\ ( K + K ) < N ) ) )
32 11 31 mpd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( 1 <_ ( K + K ) /\ ( K + K ) < N ) )
33 32 3adant3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) /\ A e. ( 0 ..^ N ) ) -> ( 1 <_ ( K + K ) /\ ( K + K ) < N ) )
34 submodneaddmod 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ K e. ZZ /\ K e. ZZ ) /\ ( 1 <_ ( K + K ) /\ ( K + K ) < N ) ) -> ( ( A + K ) mod N ) =/= ( ( A - K ) mod N ) )
35 2 4 6 6 33 34 syl131anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) /\ A e. ( 0 ..^ N ) ) -> ( ( A + K ) mod N ) =/= ( ( A - K ) mod N ) )