Metamath Proof Explorer

Theorem 2lgslem1a

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

Ref Expression
Assertion 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 ) } )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 1 nnnn0d 
 |-  ( P e. Prime -> P e. NN0 )
3 2 ad2antrr 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> P e. NN0 )
4 4nn 
 |-  4 e. NN
5 3 4 jctir 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> ( P e. NN0 /\ 4 e. NN ) )
6 fldivnn0 
 |-  ( ( P e. NN0 /\ 4 e. NN ) -> ( |_ ` ( P / 4 ) ) e. NN0 )
7 nn0p1nn 
 |-  ( ( |_ ` ( P / 4 ) ) e. NN0 -> ( ( |_ ` ( P / 4 ) ) + 1 ) e. NN )
8 5 6 7 3syl 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> ( ( |_ ` ( P / 4 ) ) + 1 ) e. NN )
9 elnnuz 
 |-  ( ( ( |_ ` ( P / 4 ) ) + 1 ) e. NN <-> ( ( |_ ` ( P / 4 ) ) + 1 ) e. ( ZZ>= ` 1 ) )
10 8 9 sylib 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> ( ( |_ ` ( P / 4 ) ) + 1 ) e. ( ZZ>= ` 1 ) )
11 fzss1 
 |-  ( ( ( |_ ` ( P / 4 ) ) + 1 ) e. ( ZZ>= ` 1 ) -> ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) C_ ( 1 ... ( ( P - 1 ) / 2 ) ) )
12 rexss 
 |-  ( ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) C_ ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) <-> E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) /\ x = ( i x. 2 ) ) ) )
13 10 11 12 3syl 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> ( E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) <-> E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) /\ x = ( i x. 2 ) ) ) )
14 ancom 
 |-  ( ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) /\ x = ( i x. 2 ) ) <-> ( x = ( i x. 2 ) /\ i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) ) )
15 2 4 jctir 
 |-  ( P e. Prime -> ( P e. NN0 /\ 4 e. NN ) )
16 15 6 syl 
 |-  ( P e. Prime -> ( |_ ` ( P / 4 ) ) e. NN0 )
17 16 nn0zd 
 |-  ( P e. Prime -> ( |_ ` ( P / 4 ) ) e. ZZ )
18 17 ad2antrr 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> ( |_ ` ( P / 4 ) ) e. ZZ )
19 elfzelz 
 |-  ( i e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> i e. ZZ )
20 zltp1le 
 |-  ( ( ( |_ ` ( P / 4 ) ) e. ZZ /\ i e. ZZ ) -> ( ( |_ ` ( P / 4 ) ) < i <-> ( ( |_ ` ( P / 4 ) ) + 1 ) <_ i ) )
21 18 19 20 syl2an 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( |_ ` ( P / 4 ) ) < i <-> ( ( |_ ` ( P / 4 ) ) + 1 ) <_ i ) )
22 21 bicomd 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( |_ ` ( P / 4 ) ) + 1 ) <_ i <-> ( |_ ` ( P / 4 ) ) < i ) )
23 22 anbi1d 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( |_ ` ( P / 4 ) ) + 1 ) <_ i /\ i <_ ( ( P - 1 ) / 2 ) ) <-> ( ( |_ ` ( P / 4 ) ) < i /\ i <_ ( ( P - 1 ) / 2 ) ) ) )
24 19 adantl 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> i e. ZZ )
25 17 peano2zd 
 |-  ( P e. Prime -> ( ( |_ ` ( P / 4 ) ) + 1 ) e. ZZ )
26 25 adantr 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( |_ ` ( P / 4 ) ) + 1 ) e. ZZ )
27 26 ad2antrr 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( |_ ` ( P / 4 ) ) + 1 ) e. ZZ )
28 prmz 
 |-  ( P e. Prime -> P e. ZZ )
29 oddm1d2 
 |-  ( P e. ZZ -> ( -. 2 || P <-> ( ( P - 1 ) / 2 ) e. ZZ ) )
30 28 29 syl 
 |-  ( P e. Prime -> ( -. 2 || P <-> ( ( P - 1 ) / 2 ) e. ZZ ) )
31 30 biimpa 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( P - 1 ) / 2 ) e. ZZ )
32 31 ad2antrr 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - 1 ) / 2 ) e. ZZ )
33 elfz 
 |-  ( ( i e. ZZ /\ ( ( |_ ` ( P / 4 ) ) + 1 ) e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ ) -> ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) <-> ( ( ( |_ ` ( P / 4 ) ) + 1 ) <_ i /\ i <_ ( ( P - 1 ) / 2 ) ) ) )
34 24 27 32 33 syl3anc 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) <-> ( ( ( |_ ` ( P / 4 ) ) + 1 ) <_ i /\ i <_ ( ( P - 1 ) / 2 ) ) ) )
35 elfzle2 
 |-  ( i e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> i <_ ( ( P - 1 ) / 2 ) )
36 35 adantl 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> i <_ ( ( P - 1 ) / 2 ) )
37 36 biantrud 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( |_ ` ( P / 4 ) ) < i <-> ( ( |_ ` ( P / 4 ) ) < i /\ i <_ ( ( P - 1 ) / 2 ) ) ) )
38 23 34 37 3bitr4d 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) <-> ( |_ ` ( P / 4 ) ) < i ) )
39 28 ad2antrr 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> P e. ZZ )
40 2lgslem1a2 
 |-  ( ( P e. ZZ /\ i e. ZZ ) -> ( ( |_ ` ( P / 4 ) ) < i <-> ( P / 2 ) < ( i x. 2 ) ) )
41 39 19 40 syl2an 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( |_ ` ( P / 4 ) ) < i <-> ( P / 2 ) < ( i x. 2 ) ) )
42 38 41 bitrd 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) <-> ( P / 2 ) < ( i x. 2 ) ) )
43 2lgslem1a1 
 |-  ( ( P e. NN /\ -. 2 || P ) -> A. k e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( k x. 2 ) = ( ( k x. 2 ) mod P ) )
44 1 43 sylan 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> A. k e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( k x. 2 ) = ( ( k x. 2 ) mod P ) )
45 44 adantr 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> A. k e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( k x. 2 ) = ( ( k x. 2 ) mod P ) )
46 oveq1 
 |-  ( k = i -> ( k x. 2 ) = ( i x. 2 ) )
47 46 oveq1d 
 |-  ( k = i -> ( ( k x. 2 ) mod P ) = ( ( i x. 2 ) mod P ) )
48 46 47 eqeq12d 
 |-  ( k = i -> ( ( k x. 2 ) = ( ( k x. 2 ) mod P ) <-> ( i x. 2 ) = ( ( i x. 2 ) mod P ) ) )
49 48 rspccva 
 |-  ( ( A. k e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( k x. 2 ) = ( ( k x. 2 ) mod P ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( i x. 2 ) = ( ( i x. 2 ) mod P ) )
50 45 49 sylan 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( i x. 2 ) = ( ( i x. 2 ) mod P ) )
51 50 breq2d 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P / 2 ) < ( i x. 2 ) <-> ( P / 2 ) < ( ( i x. 2 ) mod P ) ) )
52 42 51 bitrd 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) <-> ( P / 2 ) < ( ( i x. 2 ) mod P ) ) )
53 oveq1 
 |-  ( x = ( i x. 2 ) -> ( x mod P ) = ( ( i x. 2 ) mod P ) )
54 53 eqcomd 
 |-  ( x = ( i x. 2 ) -> ( ( i x. 2 ) mod P ) = ( x mod P ) )
55 54 breq2d 
 |-  ( x = ( i x. 2 ) -> ( ( P / 2 ) < ( ( i x. 2 ) mod P ) <-> ( P / 2 ) < ( x mod P ) ) )
56 52 55 sylan9bb 
 |-  ( ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ x = ( i x. 2 ) ) -> ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) <-> ( P / 2 ) < ( x mod P ) ) )
57 56 pm5.32da 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( x = ( i x. 2 ) /\ i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) ) <-> ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) ) )
58 14 57 syl5bb 
 |-  ( ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) /\ x = ( i x. 2 ) ) <-> ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) ) )
59 58 rexbidva 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> ( E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) /\ x = ( i x. 2 ) ) <-> E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) ) )
60 13 59 bitrd 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> ( E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) <-> E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) ) )
61 60 bicomd 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ x e. ZZ ) -> ( E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) <-> E. i e. ( ( ( |_ ` ( P / 4 ) ) + 1 ) ... ( ( P - 1 ) / 2 ) ) x = ( i x. 2 ) ) )
62 61 rabbidva 
 |-  ( ( 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 ) } )