Metamath Proof Explorer

Theorem lgseisenlem1

Description: Lemma for lgseisen . If R ( u ) = ( Q x. u ) mod P and M ( u ) = ( -u 1 ^ R ( u ) ) x. R ( u ) , then for any even 1 <_ u <_ P - 1 , M ( u ) is also an even integer 1 <_ M ( u ) <_ P - 1 . To simplify these statements, we divide all the even numbers by 2 , so that it becomes the statement that M ( x / 2 ) = ( -u 1 ^ R ( x / 2 ) ) x. R ( x / 2 ) / 2 is an integer between 1 and ( P - 1 ) / 2 . (Contributed by Mario Carneiro, 17-Jun-2015)

Ref Expression
Hypotheses lgseisen.1 
|- ( ph -> P e. ( Prime \ { 2 } ) )
lgseisen.2 
|- ( ph -> Q e. ( Prime \ { 2 } ) )
lgseisen.3 
|- ( ph -> P =/= Q )
lgseisen.4 
|- R = ( ( Q x. ( 2 x. x ) ) mod P )
lgseisen.5 
|- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
Assertion lgseisenlem1 
|- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 lgseisen.1 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 lgseisen.2 
 |-  ( ph -> Q e. ( Prime \ { 2 } ) )
3 lgseisen.3 
 |-  ( ph -> P =/= Q )
4 lgseisen.4 
 |-  R = ( ( Q x. ( 2 x. x ) ) mod P )
5 lgseisen.5 
 |-  M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
6 1zzd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 1 e. ZZ )
7 1 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. ( Prime \ { 2 } ) )
8 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
9 7 8 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - 1 ) / 2 ) e. NN )
10 9 nnzd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - 1 ) / 2 ) e. ZZ )
11 neg1cn 
 |-  -u 1 e. CC
12 11 a1i 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> -u 1 e. CC )
13 neg1ne0 
 |-  -u 1 =/= 0
14 13 a1i 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> -u 1 =/= 0 )
15 2z 
 |-  2 e. ZZ
16 15 a1i 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> 2 e. ZZ )
17 simpr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( R / 2 ) e. ZZ )
18 expmulz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( 2 e. ZZ /\ ( R / 2 ) e. ZZ ) ) -> ( -u 1 ^ ( 2 x. ( R / 2 ) ) ) = ( ( -u 1 ^ 2 ) ^ ( R / 2 ) ) )
19 12 14 16 17 18 syl22anc 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( -u 1 ^ ( 2 x. ( R / 2 ) ) ) = ( ( -u 1 ^ 2 ) ^ ( R / 2 ) ) )
20 2 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. ( Prime \ { 2 } ) )
21 20 eldifad 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. Prime )
22 prmz 
 |-  ( Q e. Prime -> Q e. ZZ )
23 21 22 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. ZZ )
24 elfzelz 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. ZZ )
25 24 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. ZZ )
26 zmulcl 
 |-  ( ( 2 e. ZZ /\ x e. ZZ ) -> ( 2 x. x ) e. ZZ )
27 15 25 26 sylancr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. ZZ )
28 23 27 zmulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. ZZ )
29 7 eldifad 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. Prime )
30 prmnn 
 |-  ( P e. Prime -> P e. NN )
31 29 30 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. NN )
32 zmodfz 
 |-  ( ( ( Q x. ( 2 x. x ) ) e. ZZ /\ P e. NN ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. ( 0 ... ( P - 1 ) ) )
33 28 31 32 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. ( 0 ... ( P - 1 ) ) )
34 4 33 eqeltrid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ( 0 ... ( P - 1 ) ) )
35 elfznn0 
 |-  ( R e. ( 0 ... ( P - 1 ) ) -> R e. NN0 )
36 34 35 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. NN0 )
37 36 nn0zd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ZZ )
38 37 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. CC )
39 38 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> R e. CC )
40 2cnd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> 2 e. CC )
41 2ne0 
 |-  2 =/= 0
42 41 a1i 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> 2 =/= 0 )
43 39 40 42 divcan2d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( 2 x. ( R / 2 ) ) = R )
44 43 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( -u 1 ^ ( 2 x. ( R / 2 ) ) ) = ( -u 1 ^ R ) )
45 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
46 45 oveq1i 
 |-  ( ( -u 1 ^ 2 ) ^ ( R / 2 ) ) = ( 1 ^ ( R / 2 ) )
47 1exp 
 |-  ( ( R / 2 ) e. ZZ -> ( 1 ^ ( R / 2 ) ) = 1 )
48 47 adantl 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( 1 ^ ( R / 2 ) ) = 1 )
49 46 48 syl5eq 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( -u 1 ^ 2 ) ^ ( R / 2 ) ) = 1 )
50 19 44 49 3eqtr3d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( -u 1 ^ R ) = 1 )
51 50 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( -u 1 ^ R ) x. R ) = ( 1 x. R ) )
52 39 mulid2d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( 1 x. R ) = R )
53 51 52 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( -u 1 ^ R ) x. R ) = R )
54 53 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( R mod P ) )
55 36 nn0red 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. RR )
56 31 nnrpd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. RR+ )
57 36 nn0ge0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 <_ R )
58 28 zred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. RR )
59 modlt 
 |-  ( ( ( Q x. ( 2 x. x ) ) e. RR /\ P e. RR+ ) -> ( ( Q x. ( 2 x. x ) ) mod P ) < P )
60 58 56 59 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) < P )
61 4 60 eqbrtrid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R < P )
62 modid 
 |-  ( ( ( R e. RR /\ P e. RR+ ) /\ ( 0 <_ R /\ R < P ) ) -> ( R mod P ) = R )
63 55 56 57 61 62 syl22anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( R mod P ) = R )
64 63 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( R mod P ) = R )
65 54 64 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = R )
66 65 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) = ( R / 2 ) )
67 66 17 eqeltrd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ZZ )
68 31 nncnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. CC )
69 68 mulid2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 x. P ) = P )
70 69 oveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u R + ( 1 x. P ) ) = ( -u R + P ) )
71 55 renegcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u R e. RR )
72 71 recnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u R e. CC )
73 68 72 addcomd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P + -u R ) = ( -u R + P ) )
74 68 38 negsubd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P + -u R ) = ( P - R ) )
75 70 73 74 3eqtr2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u R + ( 1 x. P ) ) = ( P - R ) )
76 75 oveq1d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u R + ( 1 x. P ) ) mod P ) = ( ( P - R ) mod P ) )
77 modcyc 
 |-  ( ( -u R e. RR /\ P e. RR+ /\ 1 e. ZZ ) -> ( ( -u R + ( 1 x. P ) ) mod P ) = ( -u R mod P ) )
78 71 56 6 77 syl3anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u R + ( 1 x. P ) ) mod P ) = ( -u R mod P ) )
79 31 nnred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. RR )
80 79 55 resubcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - R ) e. RR )
81 55 79 61 ltled 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R <_ P )
82 79 55 subge0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 0 <_ ( P - R ) <-> R <_ P ) )
83 81 82 mpbird 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 <_ ( P - R ) )
84 2nn 
 |-  2 e. NN
85 elfznn 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN )
86 85 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. NN )
87 nnmulcl 
 |-  ( ( 2 e. NN /\ x e. NN ) -> ( 2 x. x ) e. NN )
88 84 86 87 sylancr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. NN )
89 elfzle2 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x <_ ( ( P - 1 ) / 2 ) )
90 89 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x <_ ( ( P - 1 ) / 2 ) )
91 86 nnred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. RR )
92 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
93 uz2m1nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P - 1 ) e. NN )
94 29 92 93 3syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. NN )
95 94 nnred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. RR )
96 2re 
 |-  2 e. RR
97 96 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 e. RR )
98 2pos 
 |-  0 < 2
99 98 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 < 2 )
100 lemuldiv2 
 |-  ( ( x e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
101 91 95 97 99 100 syl112anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
102 90 101 mpbird 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) <_ ( P - 1 ) )
103 prmz 
 |-  ( P e. Prime -> P e. ZZ )
104 29 103 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. ZZ )
105 peano2zm 
 |-  ( P e. ZZ -> ( P - 1 ) e. ZZ )
106 fznn 
 |-  ( ( P - 1 ) e. ZZ -> ( ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) <-> ( ( 2 x. x ) e. NN /\ ( 2 x. x ) <_ ( P - 1 ) ) ) )
107 104 105 106 3syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) <-> ( ( 2 x. x ) e. NN /\ ( 2 x. x ) <_ ( P - 1 ) ) ) )
108 88 102 107 mpbir2and 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) )
109 fzm1ndvds 
 |-  ( ( P e. NN /\ ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( 2 x. x ) )
110 31 108 109 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || ( 2 x. x ) )
111 3 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P =/= Q )
112 prmrp 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
113 29 21 112 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
114 111 113 mpbird 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P gcd Q ) = 1 )
115 coprmdvds 
 |-  ( ( P e. ZZ /\ Q e. ZZ /\ ( 2 x. x ) e. ZZ ) -> ( ( P || ( Q x. ( 2 x. x ) ) /\ ( P gcd Q ) = 1 ) -> P || ( 2 x. x ) ) )
116 104 23 27 115 syl3anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P || ( Q x. ( 2 x. x ) ) /\ ( P gcd Q ) = 1 ) -> P || ( 2 x. x ) ) )
117 114 116 mpan2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( Q x. ( 2 x. x ) ) -> P || ( 2 x. x ) ) )
118 110 117 mtod 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || ( Q x. ( 2 x. x ) ) )
119 dvdsval3 
 |-  ( ( P e. NN /\ ( Q x. ( 2 x. x ) ) e. ZZ ) -> ( P || ( Q x. ( 2 x. x ) ) <-> ( ( Q x. ( 2 x. x ) ) mod P ) = 0 ) )
120 31 28 119 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( Q x. ( 2 x. x ) ) <-> ( ( Q x. ( 2 x. x ) ) mod P ) = 0 ) )
121 118 120 mtbid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. ( ( Q x. ( 2 x. x ) ) mod P ) = 0 )
122 4 eqeq1i 
 |-  ( R = 0 <-> ( ( Q x. ( 2 x. x ) ) mod P ) = 0 )
123 121 122 sylnibr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. R = 0 )
124 94 nnnn0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. NN0 )
125 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
126 124 125 eleqtrdi 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. ( ZZ>= ` 0 ) )
127 elfzp12 
 |-  ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> ( R e. ( 0 ... ( P - 1 ) ) <-> ( R = 0 \/ R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) ) )
128 126 127 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( R e. ( 0 ... ( P - 1 ) ) <-> ( R = 0 \/ R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) ) )
129 34 128 mpbid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( R = 0 \/ R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) )
130 129 ord 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -. R = 0 -> R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) )
131 123 130 mpd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ( ( 0 + 1 ) ... ( P - 1 ) ) )
132 1e0p1 
 |-  1 = ( 0 + 1 )
133 132 oveq1i 
 |-  ( 1 ... ( P - 1 ) ) = ( ( 0 + 1 ) ... ( P - 1 ) )
134 131 133 eleqtrrdi 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ( 1 ... ( P - 1 ) ) )
135 elfznn 
 |-  ( R e. ( 1 ... ( P - 1 ) ) -> R e. NN )
136 134 135 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. NN )
137 136 nnrpd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. RR+ )
138 79 137 ltsubrpd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - R ) < P )
139 modid 
 |-  ( ( ( ( P - R ) e. RR /\ P e. RR+ ) /\ ( 0 <_ ( P - R ) /\ ( P - R ) < P ) ) -> ( ( P - R ) mod P ) = ( P - R ) )
140 80 56 83 138 139 syl22anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - R ) mod P ) = ( P - R ) )
141 76 78 140 3eqtr3d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u R mod P ) = ( P - R ) )
142 141 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( -u R mod P ) = ( P - R ) )
143 ax-1cn 
 |-  1 e. CC
144 143 a1i 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 1 e. CC )
145 136 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> R e. NN )
146 37 peano2zd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( R + 1 ) e. ZZ )
147 dvdsval2 
 |-  ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( R + 1 ) e. ZZ ) -> ( 2 || ( R + 1 ) <-> ( ( R + 1 ) / 2 ) e. ZZ ) )
148 15 41 146 147 mp3an12i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 || ( R + 1 ) <-> ( ( R + 1 ) / 2 ) e. ZZ ) )
149 148 biimpar 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 2 || ( R + 1 ) )
150 37 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> R e. ZZ )
151 84 a1i 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 2 e. NN )
152 1lt2 
 |-  1 < 2
153 152 a1i 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 1 < 2 )
154 ndvdsp1 
 |-  ( ( R e. ZZ /\ 2 e. NN /\ 1 < 2 ) -> ( 2 || R -> -. 2 || ( R + 1 ) ) )
155 150 151 153 154 syl3anc 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( 2 || R -> -. 2 || ( R + 1 ) ) )
156 149 155 mt2d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> -. 2 || R )
157 oexpneg 
 |-  ( ( 1 e. CC /\ R e. NN /\ -. 2 || R ) -> ( -u 1 ^ R ) = -u ( 1 ^ R ) )
158 144 145 156 157 syl3anc 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( -u 1 ^ R ) = -u ( 1 ^ R ) )
159 1exp 
 |-  ( R e. ZZ -> ( 1 ^ R ) = 1 )
160 150 159 syl 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( 1 ^ R ) = 1 )
161 160 negeqd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> -u ( 1 ^ R ) = -u 1 )
162 158 161 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( -u 1 ^ R ) = -u 1 )
163 162 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( -u 1 ^ R ) x. R ) = ( -u 1 x. R ) )
164 38 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> R e. CC )
165 164 mulm1d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( -u 1 x. R ) = -u R )
166 163 165 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( -u 1 ^ R ) x. R ) = -u R )
167 166 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( -u R mod P ) )
168 68 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> P e. CC )
169 168 164 144 pnpcan2d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P + 1 ) - ( R + 1 ) ) = ( P - R ) )
170 142 167 169 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( ( P + 1 ) - ( R + 1 ) ) )
171 170 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) = ( ( ( P + 1 ) - ( R + 1 ) ) / 2 ) )
172 peano2cn 
 |-  ( P e. CC -> ( P + 1 ) e. CC )
173 168 172 syl 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( P + 1 ) e. CC )
174 peano2cn 
 |-  ( R e. CC -> ( R + 1 ) e. CC )
175 164 174 syl 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( R + 1 ) e. CC )
176 2cnd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 2 e. CC )
177 41 a1i 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 2 =/= 0 )
178 173 175 176 177 divsubdird 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P + 1 ) - ( R + 1 ) ) / 2 ) = ( ( ( P + 1 ) / 2 ) - ( ( R + 1 ) / 2 ) ) )
179 171 178 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) = ( ( ( P + 1 ) / 2 ) - ( ( R + 1 ) / 2 ) ) )
180 168 144 176 subadd23d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P - 1 ) + 2 ) = ( P + ( 2 - 1 ) ) )
181 2m1e1 
 |-  ( 2 - 1 ) = 1
182 181 oveq2i 
 |-  ( P + ( 2 - 1 ) ) = ( P + 1 )
183 180 182 eqtr2di 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( P + 1 ) = ( ( P - 1 ) + 2 ) )
184 183 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P + 1 ) / 2 ) = ( ( ( P - 1 ) + 2 ) / 2 ) )
185 94 nncnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. CC )
186 185 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( P - 1 ) e. CC )
187 186 176 176 177 divdird 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P - 1 ) + 2 ) / 2 ) = ( ( ( P - 1 ) / 2 ) + ( 2 / 2 ) ) )
188 2div2e1 
 |-  ( 2 / 2 ) = 1
189 188 oveq2i 
 |-  ( ( ( P - 1 ) / 2 ) + ( 2 / 2 ) ) = ( ( ( P - 1 ) / 2 ) + 1 )
190 187 189 eqtrdi 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P - 1 ) + 2 ) / 2 ) = ( ( ( P - 1 ) / 2 ) + 1 ) )
191 184 190 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P + 1 ) / 2 ) = ( ( ( P - 1 ) / 2 ) + 1 ) )
192 10 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P - 1 ) / 2 ) e. ZZ )
193 192 peano2zd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P - 1 ) / 2 ) + 1 ) e. ZZ )
194 191 193 eqeltrd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P + 1 ) / 2 ) e. ZZ )
195 simpr 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( R + 1 ) / 2 ) e. ZZ )
196 194 195 zsubcld 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P + 1 ) / 2 ) - ( ( R + 1 ) / 2 ) ) e. ZZ )
197 179 196 eqeltrd 
 |-  ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ZZ )
198 zeo 
 |-  ( R e. ZZ -> ( ( R / 2 ) e. ZZ \/ ( ( R + 1 ) / 2 ) e. ZZ ) )
199 37 198 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( R / 2 ) e. ZZ \/ ( ( R + 1 ) / 2 ) e. ZZ ) )
200 67 197 199 mpjaodan 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ZZ )
201 m1expcl 
 |-  ( R e. ZZ -> ( -u 1 ^ R ) e. ZZ )
202 37 201 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. ZZ )
203 202 37 zmulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. R ) e. ZZ )
204 203 31 zmodcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN0 )
205 204 nn0red 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. RR )
206 fzm1ndvds 
 |-  ( ( P e. NN /\ R e. ( 1 ... ( P - 1 ) ) ) -> -. P || R )
207 31 134 206 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || R )
208 ax-1ne0 
 |-  1 =/= 0
209 divneg2 
 |-  ( ( 1 e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
210 143 143 208 209 mp3an 
 |-  -u ( 1 / 1 ) = ( 1 / -u 1 )
211 1div1e1 
 |-  ( 1 / 1 ) = 1
212 211 negeqi 
 |-  -u ( 1 / 1 ) = -u 1
213 210 212 eqtr3i 
 |-  ( 1 / -u 1 ) = -u 1
214 213 oveq1i 
 |-  ( ( 1 / -u 1 ) ^ R ) = ( -u 1 ^ R )
215 11 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u 1 e. CC )
216 13 a1i 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u 1 =/= 0 )
217 215 216 37 exprecd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( 1 / -u 1 ) ^ R ) = ( 1 / ( -u 1 ^ R ) ) )
218 214 217 eqtr3id 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) = ( 1 / ( -u 1 ^ R ) ) )
219 218 oveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) = ( ( -u 1 ^ R ) x. ( 1 / ( -u 1 ^ R ) ) ) )
220 202 zcnd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. CC )
221 215 216 37 expne0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) =/= 0 )
222 220 221 recidd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. ( 1 / ( -u 1 ^ R ) ) ) = 1 )
223 219 222 eqtrd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) = 1 )
224 223 oveq1d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) x. R ) = ( 1 x. R ) )
225 220 220 38 mulassd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) x. R ) = ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) )
226 38 mulid2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 x. R ) = R )
227 224 225 226 3eqtr3d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) = R )
228 227 breq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) <-> P || R ) )
229 207 228 mtbird 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) )
230 dvdsmultr2 
 |-  ( ( P e. ZZ /\ ( -u 1 ^ R ) e. ZZ /\ ( ( -u 1 ^ R ) x. R ) e. ZZ ) -> ( P || ( ( -u 1 ^ R ) x. R ) -> P || ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) ) )
231 104 202 203 230 syl3anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( ( -u 1 ^ R ) x. R ) -> P || ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) ) )
232 229 231 mtod 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || ( ( -u 1 ^ R ) x. R ) )
233 dvdsval3 
 |-  ( ( P e. NN /\ ( ( -u 1 ^ R ) x. R ) e. ZZ ) -> ( P || ( ( -u 1 ^ R ) x. R ) <-> ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 ) )
234 31 203 233 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( ( -u 1 ^ R ) x. R ) <-> ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 ) )
235 232 234 mtbid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 )
236 elnn0 
 |-  ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN0 <-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN \/ ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 ) )
237 204 236 sylib 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN \/ ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 ) )
238 237 ord 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -. ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 ) )
239 235 238 mt3d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN )
240 239 nngt0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 < ( ( ( -u 1 ^ R ) x. R ) mod P ) )
241 205 97 240 99 divgt0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 < ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
242 elnnz 
 |-  ( ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. NN <-> ( ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ZZ /\ 0 < ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) )
243 200 241 242 sylanbrc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. NN )
244 243 nnge1d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 1 <_ ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
245 zmodfz 
 |-  ( ( ( ( -u 1 ^ R ) x. R ) e. ZZ /\ P e. NN ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ( 0 ... ( P - 1 ) ) )
246 203 31 245 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ( 0 ... ( P - 1 ) ) )
247 elfzle2 
 |-  ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ( 0 ... ( P - 1 ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) <_ ( P - 1 ) )
248 246 247 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) <_ ( P - 1 ) )
249 lediv1 
 |-  ( ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) <_ ( P - 1 ) <-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) <_ ( ( P - 1 ) / 2 ) ) )
250 205 95 97 99 249 syl112anc 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) <_ ( P - 1 ) <-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) <_ ( ( P - 1 ) / 2 ) ) )
251 248 250 mpbid 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) <_ ( ( P - 1 ) / 2 ) )
252 6 10 200 244 251 elfzd 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) )
253 252 5 fmptd 
 |-  ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )