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 ) )