Metamath Proof Explorer

Theorem 2lgslem1

Description: Lemma 1 for 2lgs . (Contributed by AV, 19-Jun-2021)

Ref Expression
Assertion 2lgslem1 
|- ( ( P e. Prime /\ -. 2 || P ) -> ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) )

Proof

Step Hyp Ref Expression
1 2lgslem1a 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } = { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } )
2 1 fveq2d 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) = ( # ` { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } ) )
3 ovex 
 |-  ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) e. _V
4 3 mptex 
 |-  ( y e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) |-> ( y x. 2 ) ) e. _V
5 f1oeq1 
 |-  ( f = ( y e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) |-> ( y x. 2 ) ) -> ( f : ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } <-> ( y e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) |-> ( y x. 2 ) ) : ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } ) )
6 eqid 
 |-  ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) = ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) )
7 eqid 
 |-  ( y e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) |-> ( y x. 2 ) ) = ( y e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) |-> ( y x. 2 ) )
8 6 7 2lgslem1b 
 |-  ( y e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) |-> ( y x. 2 ) ) : ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) }
9 4 5 8 ceqsexv2d 
 |-  E. f f : ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) }
10 9 a1i 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> E. f f : ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } )
11 hasheqf1oi 
 |-  ( ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) e. _V -> ( E. f f : ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } -> ( # ` ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) ) = ( # ` { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } ) ) )
12 3 10 11 mpsyl 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( # ` ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) ) = ( # ` { x e. ZZ | E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) } ) )
13 prmz 
 |-  ( P e. Prime -> P e. ZZ )
14 13 zred 
 |-  ( P e. Prime -> P e. RR )
15 4re 
 |-  4 e. RR
16 15 a1i 
 |-  ( P e. Prime -> 4 e. RR )
17 4ne0 
 |-  4 =/= 0
18 17 a1i 
 |-  ( P e. Prime -> 4 =/= 0 )
19 14 16 18 redivcld 
 |-  ( P e. Prime -> ( P / 4 ) e. RR )
20 19 flcld 
 |-  ( P e. Prime -> ( |_ ` ( P / 4 ) ) e. ZZ )
21 20 adantr 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( |_ ` ( P / 4 ) ) e. ZZ )
22 oddm1d2 
 |-  ( P e. ZZ -> ( -. 2 || P <-> ( ( P - 1 ) / 2 ) e. ZZ ) )
23 13 22 syl 
 |-  ( P e. Prime -> ( -. 2 || P <-> ( ( P - 1 ) / 2 ) e. ZZ ) )
24 23 biimpa 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( P - 1 ) / 2 ) e. ZZ )
25 2lgslem1c 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )
26 eluz2 
 |-  ( ( ( P - 1 ) / 2 ) e. ( ZZ>= ` ( |_ ` ( P / 4 ) ) ) <-> ( ( |_ ` ( P / 4 ) ) e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
27 21 24 25 26 syl3anbrc 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( P - 1 ) / 2 ) e. ( ZZ>= ` ( |_ ` ( P / 4 ) ) ) )
28 hashfzp1 
 |-  ( ( ( P - 1 ) / 2 ) e. ( ZZ>= ` ( |_ ` ( P / 4 ) ) ) -> ( # ` ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) ) = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) )
29 27 28 syl 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( # ` ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) ) = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) )
30 2 12 29 3eqtr2d 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) )