Metamath Proof Explorer

Theorem 2lgslem1a1

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

Ref Expression
Assertion 2lgslem1a1 
|- ( ( P e. NN /\ -. 2 || P ) -> A. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( i x. 2 ) = ( ( i x. 2 ) mod P ) )

Proof

Step Hyp Ref Expression
1 nnrp 
 |-  ( P e. NN -> P e. RR+ )
2 1 adantr 
 |-  ( ( P e. NN /\ -. 2 || P ) -> P e. RR+ )
3 elfzelz 
 |-  ( i e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> i e. ZZ )
4 zre 
 |-  ( i e. ZZ -> i e. RR )
5 2re 
 |-  2 e. RR
6 5 a1i 
 |-  ( i e. ZZ -> 2 e. RR )
7 4 6 remulcld 
 |-  ( i e. ZZ -> ( i x. 2 ) e. RR )
8 3 7 syl 
 |-  ( i e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( i x. 2 ) e. RR )
9 2 8 anim12ci 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( i x. 2 ) e. RR /\ P e. RR+ ) )
10 elfznn 
 |-  ( i e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> i e. NN )
11 nnre 
 |-  ( i e. NN -> i e. RR )
12 nnnn0 
 |-  ( i e. NN -> i e. NN0 )
13 12 nn0ge0d 
 |-  ( i e. NN -> 0 <_ i )
14 0le2 
 |-  0 <_ 2
15 5 14 pm3.2i 
 |-  ( 2 e. RR /\ 0 <_ 2 )
16 15 a1i 
 |-  ( i e. NN -> ( 2 e. RR /\ 0 <_ 2 ) )
17 mulge0 
 |-  ( ( ( i e. RR /\ 0 <_ i ) /\ ( 2 e. RR /\ 0 <_ 2 ) ) -> 0 <_ ( i x. 2 ) )
18 11 13 16 17 syl21anc 
 |-  ( i e. NN -> 0 <_ ( i x. 2 ) )
19 10 18 syl 
 |-  ( i e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> 0 <_ ( i x. 2 ) )
20 19 adantl 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 <_ ( i x. 2 ) )
21 elfz2 
 |-  ( i e. ( 1 ... ( ( P - 1 ) / 2 ) ) <-> ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ ( ( P - 1 ) / 2 ) ) ) )
22 4 3ad2ant3 
 |-  ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) -> i e. RR )
23 zre 
 |-  ( ( ( P - 1 ) / 2 ) e. ZZ -> ( ( P - 1 ) / 2 ) e. RR )
24 23 3ad2ant2 
 |-  ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) -> ( ( P - 1 ) / 2 ) e. RR )
25 2pos 
 |-  0 < 2
26 5 25 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
27 26 a1i 
 |-  ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) -> ( 2 e. RR /\ 0 < 2 ) )
28 lemul1 
 |-  ( ( i e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( i <_ ( ( P - 1 ) / 2 ) <-> ( i x. 2 ) <_ ( ( ( P - 1 ) / 2 ) x. 2 ) ) )
29 22 24 27 28 syl3anc 
 |-  ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) -> ( i <_ ( ( P - 1 ) / 2 ) <-> ( i x. 2 ) <_ ( ( ( P - 1 ) / 2 ) x. 2 ) ) )
30 nncn 
 |-  ( P e. NN -> P e. CC )
31 peano2cnm 
 |-  ( P e. CC -> ( P - 1 ) e. CC )
32 30 31 syl 
 |-  ( P e. NN -> ( P - 1 ) e. CC )
33 2cnd 
 |-  ( P e. NN -> 2 e. CC )
34 2ne0 
 |-  2 =/= 0
35 34 a1i 
 |-  ( P e. NN -> 2 =/= 0 )
36 32 33 35 divcan1d 
 |-  ( P e. NN -> ( ( ( P - 1 ) / 2 ) x. 2 ) = ( P - 1 ) )
37 36 adantr 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( ( ( P - 1 ) / 2 ) x. 2 ) = ( P - 1 ) )
38 37 adantl 
 |-  ( ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) /\ ( P e. NN /\ -. 2 || P ) ) -> ( ( ( P - 1 ) / 2 ) x. 2 ) = ( P - 1 ) )
39 38 breq2d 
 |-  ( ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) /\ ( P e. NN /\ -. 2 || P ) ) -> ( ( i x. 2 ) <_ ( ( ( P - 1 ) / 2 ) x. 2 ) <-> ( i x. 2 ) <_ ( P - 1 ) ) )
40 id 
 |-  ( i e. ZZ -> i e. ZZ )
41 2z 
 |-  2 e. ZZ
42 41 a1i 
 |-  ( i e. ZZ -> 2 e. ZZ )
43 40 42 zmulcld 
 |-  ( i e. ZZ -> ( i x. 2 ) e. ZZ )
44 43 3ad2ant3 
 |-  ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) -> ( i x. 2 ) e. ZZ )
45 nnz 
 |-  ( P e. NN -> P e. ZZ )
46 45 adantr 
 |-  ( ( P e. NN /\ -. 2 || P ) -> P e. ZZ )
47 zltlem1 
 |-  ( ( ( i x. 2 ) e. ZZ /\ P e. ZZ ) -> ( ( i x. 2 ) < P <-> ( i x. 2 ) <_ ( P - 1 ) ) )
48 44 46 47 syl2an 
 |-  ( ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) /\ ( P e. NN /\ -. 2 || P ) ) -> ( ( i x. 2 ) < P <-> ( i x. 2 ) <_ ( P - 1 ) ) )
49 48 biimprd 
 |-  ( ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) /\ ( P e. NN /\ -. 2 || P ) ) -> ( ( i x. 2 ) <_ ( P - 1 ) -> ( i x. 2 ) < P ) )
50 39 49 sylbid 
 |-  ( ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) /\ ( P e. NN /\ -. 2 || P ) ) -> ( ( i x. 2 ) <_ ( ( ( P - 1 ) / 2 ) x. 2 ) -> ( i x. 2 ) < P ) )
51 50 ex 
 |-  ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) -> ( ( P e. NN /\ -. 2 || P ) -> ( ( i x. 2 ) <_ ( ( ( P - 1 ) / 2 ) x. 2 ) -> ( i x. 2 ) < P ) ) )
52 51 com23 
 |-  ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) -> ( ( i x. 2 ) <_ ( ( ( P - 1 ) / 2 ) x. 2 ) -> ( ( P e. NN /\ -. 2 || P ) -> ( i x. 2 ) < P ) ) )
53 29 52 sylbid 
 |-  ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) -> ( i <_ ( ( P - 1 ) / 2 ) -> ( ( P e. NN /\ -. 2 || P ) -> ( i x. 2 ) < P ) ) )
54 53 a1d 
 |-  ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) -> ( 1 <_ i -> ( i <_ ( ( P - 1 ) / 2 ) -> ( ( P e. NN /\ -. 2 || P ) -> ( i x. 2 ) < P ) ) ) )
55 54 imp32 
 |-  ( ( ( 1 e. ZZ /\ ( ( P - 1 ) / 2 ) e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ ( ( P - 1 ) / 2 ) ) ) -> ( ( P e. NN /\ -. 2 || P ) -> ( i x. 2 ) < P ) )
56 21 55 sylbi 
 |-  ( i e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( ( P e. NN /\ -. 2 || P ) -> ( i x. 2 ) < P ) )
57 56 impcom 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( i x. 2 ) < P )
58 modid 
 |-  ( ( ( ( i x. 2 ) e. RR /\ P e. RR+ ) /\ ( 0 <_ ( i x. 2 ) /\ ( i x. 2 ) < P ) ) -> ( ( i x. 2 ) mod P ) = ( i x. 2 ) )
59 9 20 57 58 syl12anc 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( i x. 2 ) mod P ) = ( i x. 2 ) )
60 59 eqcomd 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( i x. 2 ) = ( ( i x. 2 ) mod P ) )
61 60 ralrimiva 
 |-  ( ( P e. NN /\ -. 2 || P ) -> A. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( i x. 2 ) = ( ( i x. 2 ) mod P ) )