MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgseisenlem1 Unicode version

Theorem lgseisenlem1 21086
Description: Lemma for lgseisen 21090. 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.)
Hypotheses
Ref Expression
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
Ref Expression
lgseisenlem1  |-  ( ph  ->  M : ( 1 ... ( ( P  -  1 )  / 
2 ) ) --> ( 1 ... ( ( P  -  1 )  /  2 ) ) )
Distinct variable groups:    x, P    ph, x    x, Q
Allowed substitution hints:    R( x)    M( x)

Proof of Theorem lgseisenlem1
StepHypRef Expression
1 neg1cn 10023 . . . . . . . . . . . . . . 15  |-  -u 1  e.  CC
21a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  -u 1  e.  CC )
3 ax-1cn 9004 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
4 ax-1ne0 9015 . . . . . . . . . . . . . . . 16  |-  1  =/=  0
53, 4negne0i 9331 . . . . . . . . . . . . . . 15  |-  -u 1  =/=  0
65a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  -u 1  =/=  0 )
7 2z 10268 . . . . . . . . . . . . . . 15  |-  2  e.  ZZ
87a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  2  e.  ZZ )
9 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( R  /  2 )  e.  ZZ )
10 expmulz 11381 . . . . . . . . . . . . . 14  |-  ( ( ( -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
) ) )
112, 6, 8, 9, 10syl22anc 1185 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( -u 1 ^ ( 2  x.  ( R  / 
2 ) ) )  =  ( ( -u
1 ^ 2 ) ^ ( R  / 
2 ) ) )
12 lgseisen.4 . . . . . . . . . . . . . . . . . . . 20  |-  R  =  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)
13 lgseisen.2 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
1413adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ( Prime  \  { 2 } ) )
1514eldifad 3292 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  Prime )
16 prmz 13038 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
1715, 16syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ZZ )
18 elfzelz 11015 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  ZZ )
1918adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  ZZ )
20 zmulcl 10280 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  e.  ZZ  /\  x  e.  ZZ )  ->  ( 2  x.  x
)  e.  ZZ )
217, 19, 20sylancr 645 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  ZZ )
2217, 21zmulcld 10337 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  ZZ )
23 lgseisen.1 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
2423adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ( Prime  \  { 2 } ) )
2524eldifad 3292 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  Prime )
26 prmnn 13037 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  Prime  ->  P  e.  NN )
2725, 26syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  NN )
28 zmodfz 11223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( Q  x.  (
2  x.  x ) )  e.  ZZ  /\  P  e.  NN )  ->  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)  e.  ( 0 ... ( P  - 
1 ) ) )
2922, 27, 28syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  e.  ( 0 ... ( P  -  1 ) ) )
3012, 29syl5eqel 2488 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ( 0 ... ( P  -  1 ) ) )
31 elfznn0 11039 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  ( 0 ... ( P  -  1 ) )  ->  R  e.  NN0 )
3230, 31syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN0 )
3332nn0zd 10329 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ZZ )
3433zcnd 10332 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  CC )
3534adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  R  e.  CC )
36 2cn 10026 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
3736a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  2  e.  CC )
38 2ne0 10039 . . . . . . . . . . . . . . . 16  |-  2  =/=  0
3938a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  2  =/=  0 )
4035, 37, 39divcan2d 9748 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
2  x.  ( R  /  2 ) )  =  R )
4140oveq2d 6056 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( -u 1 ^ ( 2  x.  ( R  / 
2 ) ) )  =  ( -u 1 ^ R ) )
42 sqneg 11397 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  CC  ->  ( -u 1 ^ 2 )  =  ( 1 ^ 2 ) )
433, 42ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( -u
1 ^ 2 )  =  ( 1 ^ 2 )
44 sq1 11431 . . . . . . . . . . . . . . . 16  |-  ( 1 ^ 2 )  =  1
4543, 44eqtri 2424 . . . . . . . . . . . . . . 15  |-  ( -u
1 ^ 2 )  =  1
4645oveq1i 6050 . . . . . . . . . . . . . 14  |-  ( (
-u 1 ^ 2 ) ^ ( R  /  2 ) )  =  ( 1 ^ ( R  /  2
) )
47 1exp 11364 . . . . . . . . . . . . . . 15  |-  ( ( R  /  2 )  e.  ZZ  ->  (
1 ^ ( R  /  2 ) )  =  1 )
4847adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
1 ^ ( R  /  2 ) )  =  1 )
4946, 48syl5eq 2448 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( -u 1 ^ 2 ) ^ ( R  /  2 ) )  =  1 )
5011, 41, 493eqtr3d 2444 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( -u 1 ^ R )  =  1 )
5150oveq1d 6055 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( -u 1 ^ R
)  x.  R )  =  ( 1  x.  R ) )
5235mulid2d 9062 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
1  x.  R )  =  R )
5351, 52eqtrd 2436 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( -u 1 ^ R
)  x.  R )  =  R )
5453oveq1d 6055 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  =  ( R  mod  P ) )
5532nn0red 10231 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  RR )
5627nnrpd 10603 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR+ )
5732nn0ge0d 10233 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <_  R )
5822zred 10331 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  RR )
59 modlt 11213 . . . . . . . . . . . . 13  |-  ( ( ( Q  x.  (
2  x.  x ) )  e.  RR  /\  P  e.  RR+ )  -> 
( ( Q  x.  ( 2  x.  x
) )  mod  P
)  <  P )
6058, 56, 59syl2anc 643 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  <  P )
6112, 60syl5eqbr 4205 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  <  P )
62 modid 11225 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  P  e.  RR+ )  /\  ( 0  <_  R  /\  R  <  P ) )  ->  ( R  mod  P )  =  R )
6355, 56, 57, 61, 62syl22anc 1185 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( R  mod  P )  =  R )
6463adantr 452 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( R  mod  P )  =  R )
6554, 64eqtrd 2436 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  =  R )
6665oveq1d 6055 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  =  ( R  /  2 ) )
6766, 9eqeltrd 2478 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  e.  ZZ )
6827nncnd 9972 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  CC )
6968mulid2d 9062 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  P )  =  P )
7069oveq2d 6056 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u R  +  ( 1  x.  P ) )  =  ( -u R  +  P ) )
7155renegcld 9420 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u R  e.  RR )
7271recnd 9070 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u R  e.  CC )
7368, 72addcomd 9224 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  +  -u R )  =  ( -u R  +  P ) )
7468, 34negsubd 9373 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  +  -u R )  =  ( P  -  R ) )
7570, 73, 743eqtr2d 2442 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u R  +  ( 1  x.  P ) )  =  ( P  -  R ) )
7675oveq1d 6055 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u R  +  ( 1  x.  P ) )  mod  P )  =  ( ( P  -  R )  mod 
P ) )
77 1z 10267 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
7877a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  e.  ZZ )
79 modcyc 11231 . . . . . . . . . . . . 13  |-  ( (
-u R  e.  RR  /\  P  e.  RR+  /\  1  e.  ZZ )  ->  (
( -u R  +  ( 1  x.  P ) )  mod  P )  =  ( -u R  mod  P ) )
8071, 56, 78, 79syl3anc 1184 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u R  +  ( 1  x.  P ) )  mod  P )  =  ( -u R  mod  P ) )
8127nnred 9971 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR )
8281, 55resubcld 9421 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  R )  e.  RR )
8355, 81, 61ltled 9177 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  <_  P )
8481, 55subge0d 9572 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
0  <_  ( P  -  R )  <->  R  <_  P ) )
8583, 84mpbird 224 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <_  ( P  -  R
) )
86 2nn 10089 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  NN
87 elfznn 11036 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  NN )
8887adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  NN )
89 nnmulcl 9979 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2  e.  NN  /\  x  e.  NN )  ->  ( 2  x.  x
)  e.  NN )
9086, 88, 89sylancr 645 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  NN )
91 elfzle2 11017 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  <_  ( ( P  - 
1 )  /  2
) )
9291adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  <_  ( ( P  - 
1 )  /  2
) )
9388nnred 9971 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  RR )
94 prmuz2 13052 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
95 uz2m1nn 10506 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  ( ZZ>= `  2
)  ->  ( P  -  1 )  e.  NN )
9625, 94, 953syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  NN )
9796nnred 9971 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  RR )
98 2re 10025 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  2  e.  RR
9998a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  RR )
100 2pos 10038 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <  2
101100a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <  2 )
102 lemuldiv2 9846 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  RR  /\  ( P  -  1
)  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
2  x.  x )  <_  ( P  - 
1 )  <->  x  <_  ( ( P  -  1 )  /  2 ) ) )
10393, 97, 99, 101, 102syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( 2  x.  x
)  <_  ( P  -  1 )  <->  x  <_  ( ( P  -  1 )  /  2 ) ) )
10492, 103mpbird 224 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  <_  ( P  - 
1 ) )
105 prmz 13038 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e.  Prime  ->  P  e.  ZZ )
10625, 105syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
107 peano2zm 10276 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( P  e.  ZZ  ->  ( P  -  1 )  e.  ZZ )
108 fznn 11070 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( P  -  1 )  e.  ZZ  ->  (
( 2  x.  x
)  e.  ( 1 ... ( P  - 
1 ) )  <->  ( (
2  x.  x )  e.  NN  /\  (
2  x.  x )  <_  ( P  - 
1 ) ) ) )
109106, 107, 1083syl 19 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( 2  x.  x
)  e.  ( 1 ... ( P  - 
1 ) )  <->  ( (
2  x.  x )  e.  NN  /\  (
2  x.  x )  <_  ( P  - 
1 ) ) ) )
11090, 104, 109mpbir2and 889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  ( 1 ... ( P  -  1 ) ) )
111 fzm1ndvds 12856 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( P  e.  NN  /\  ( 2  x.  x
)  e.  ( 1 ... ( P  - 
1 ) ) )  ->  -.  P  ||  (
2  x.  x ) )
11227, 110, 111syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  ( 2  x.  x ) )
113 lgseisen.3 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  =/=  Q )
114113adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  =/=  Q )
115 prmrp 13056 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( P  e.  Prime  /\  Q  e.  Prime )  ->  (
( P  gcd  Q
)  =  1  <->  P  =/=  Q ) )
11625, 15, 115syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  gcd  Q
)  =  1  <->  P  =/=  Q ) )
117114, 116mpbird 224 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  gcd  Q )  =  1 )
118 coprmdvds 13057 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 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
) ) )
119106, 17, 21, 118syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  ||  ( Q  x.  ( 2  x.  x ) )  /\  ( P  gcd  Q )  =  1 )  ->  P  ||  (
2  x.  x ) ) )
120117, 119mpan2d 656 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( Q  x.  ( 2  x.  x
) )  ->  P  ||  ( 2  x.  x
) ) )
121112, 120mtod 170 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  ( Q  x.  ( 2  x.  x
) ) )
122 dvdsval3 12811 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P  e.  NN  /\  ( Q  x.  (
2  x.  x ) )  e.  ZZ )  ->  ( P  ||  ( Q  x.  (
2  x.  x ) )  <->  ( ( Q  x.  ( 2  x.  x ) )  mod 
P )  =  0 ) )
12327, 22, 122syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( Q  x.  ( 2  x.  x
) )  <->  ( ( Q  x.  ( 2  x.  x ) )  mod  P )  =  0 ) )
124121, 123mtbid 292 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)  =  0 )
12512eqeq1i 2411 . . . . . . . . . . . . . . . . . . 19  |-  ( R  =  0  <->  ( ( Q  x.  ( 2  x.  x ) )  mod  P )  =  0 )
126124, 125sylnibr 297 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  R  =  0 )
12796nnnn0d 10230 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  NN0 )
128 nn0uz 10476 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  =  ( ZZ>= `  0 )
129127, 128syl6eleq 2494 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  ( ZZ>= `  0
) )
130 elfzp12 11081 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P  -  1 )  e.  ( ZZ>= `  0
)  ->  ( R  e.  ( 0 ... ( P  -  1 ) )  <->  ( R  =  0  \/  R  e.  ( ( 0  +  1 ) ... ( P  -  1 ) ) ) ) )
131129, 130syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( R  e.  ( 0 ... ( P  - 
1 ) )  <->  ( R  =  0  \/  R  e.  ( ( 0  +  1 ) ... ( P  -  1 ) ) ) ) )
13230, 131mpbid 202 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( R  =  0  \/  R  e.  ( (
0  +  1 ) ... ( P  - 
1 ) ) ) )
133132ord 367 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -.  R  =  0  ->  R  e.  ( ( 0  +  1 ) ... ( P  - 
1 ) ) ) )
134126, 133mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ( ( 0  +  1 ) ... ( P  -  1 ) ) )
135 1e0p1 10366 . . . . . . . . . . . . . . . . . 18  |-  1  =  ( 0  +  1 )
136135oveq1i 6050 . . . . . . . . . . . . . . . . 17  |-  ( 1 ... ( P  - 
1 ) )  =  ( ( 0  +  1 ) ... ( P  -  1 ) )
137134, 136syl6eleqr 2495 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ( 1 ... ( P  -  1 ) ) )
138 elfznn 11036 . . . . . . . . . . . . . . . 16  |-  ( R  e.  ( 1 ... ( P  -  1 ) )  ->  R  e.  NN )
139137, 138syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN )
140139nnrpd 10603 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  RR+ )
14181, 140ltsubrpd 10632 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  R )  <  P )
142 modid 11225 . . . . . . . . . . . . 13  |-  ( ( ( ( P  -  R )  e.  RR  /\  P  e.  RR+ )  /\  ( 0  <_  ( P  -  R )  /\  ( P  -  R
)  <  P )
)  ->  ( ( P  -  R )  mod  P )  =  ( P  -  R ) )
14382, 56, 85, 141, 142syl22anc 1185 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  R
)  mod  P )  =  ( P  -  R ) )
14476, 80, 1433eqtr3d 2444 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u R  mod  P )  =  ( P  -  R ) )
145144adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u R  mod  P
)  =  ( P  -  R ) )
1463a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
1  e.  CC )
147139adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  R  e.  NN )
1487a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  ZZ )
14938a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  =/=  0 )
15033peano2zd 10334 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( R  +  1 )  e.  ZZ )
151 dvdsval2 12810 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  ZZ  /\  2  =/=  0  /\  ( R  +  1 )  e.  ZZ )  -> 
( 2  ||  ( R  +  1 )  <-> 
( ( R  + 
1 )  /  2
)  e.  ZZ ) )
152148, 149, 150, 151syl3anc 1184 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  ||  ( R  +  1 )  <->  ( ( R  +  1 )  /  2 )  e.  ZZ ) )
153152biimpar 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
2  ||  ( R  +  1 ) )
15433adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  R  e.  ZZ )
15586a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
2  e.  NN )
156 1lt2 10098 . . . . . . . . . . . . . . . . . 18  |-  1  <  2
157156a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
1  <  2 )
158 ndvdsp1 12884 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  ZZ  /\  2  e.  NN  /\  1  <  2 )  ->  (
2  ||  R  ->  -.  2  ||  ( R  +  1 ) ) )
159154, 155, 157, 158syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( 2  ||  R  ->  -.  2  ||  ( R  +  1 ) ) )
160153, 159mt2d 111 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  -.  2  ||  R )
161 oexpneg 12866 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  R  e.  NN  /\  -.  2  ||  R )  -> 
( -u 1 ^ R
)  =  -u (
1 ^ R ) )
162146, 147, 160, 161syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u 1 ^ R
)  =  -u (
1 ^ R ) )
163 1exp 11364 . . . . . . . . . . . . . . . 16  |-  ( R  e.  ZZ  ->  (
1 ^ R )  =  1 )
164154, 163syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( 1 ^ R
)  =  1 )
165164negeqd 9256 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  -u ( 1 ^ R
)  =  -u 1
)
166162, 165eqtrd 2436 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u 1 ^ R
)  =  -u 1
)
167166oveq1d 6055 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( -u 1 ^ R )  x.  R
)  =  ( -u
1  x.  R ) )
16834adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  R  e.  CC )
169168mulm1d 9441 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u 1  x.  R
)  =  -u R
)
170167, 169eqtrd 2436 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( -u 1 ^ R )  x.  R
)  =  -u R
)
171170oveq1d 6055 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  =  (
-u R  mod  P
) )
17268adantr 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  P  e.  CC )
173172, 168, 146pnpcan2d 9405 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  -  ( R  +  1 ) )  =  ( P  -  R ) )
174145, 171, 1733eqtr4d 2446 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  =  ( ( P  +  1 )  -  ( R  +  1 ) ) )
175174oveq1d 6055 . . . . . . . 8  |-  ( ( ( 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 ) )
176 peano2cn 9194 . . . . . . . . . 10  |-  ( P  e.  CC  ->  ( P  +  1 )  e.  CC )
177172, 176syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( P  +  1 )  e.  CC )
178 peano2cn 9194 . . . . . . . . . 10  |-  ( R  e.  CC  ->  ( R  +  1 )  e.  CC )
179168, 178syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( R  +  1 )  e.  CC )
18036a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
2  e.  CC )
18138a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
2  =/=  0 )
182177, 179, 180, 181divsubdird 9785 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  +  1 )  -  ( R  +  1
) )  /  2
)  =  ( ( ( P  +  1 )  /  2 )  -  ( ( R  +  1 )  / 
2 ) ) )
183175, 182eqtrd 2436 . . . . . . 7  |-  ( ( ( 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 ) ) )
184172, 146, 180subadd23d 9389 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  - 
1 )  +  2 )  =  ( P  +  ( 2  -  1 ) ) )
185 2m1e1 10051 . . . . . . . . . . . . 13  |-  ( 2  -  1 )  =  1
186185oveq2i 6051 . . . . . . . . . . . 12  |-  ( P  +  ( 2  -  1 ) )  =  ( P  +  1 )
187184, 186syl6req 2453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( P  +  1 )  =  ( ( P  -  1 )  +  2 ) )
188187oveq1d 6055 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  /  2
)  =  ( ( ( P  -  1 )  +  2 )  /  2 ) )
18996nncnd 9972 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  CC )
190189adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( P  -  1 )  e.  CC )
191190, 180, 180, 181divdird 9784 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  -  1 )  +  2 )  /  2
)  =  ( ( ( P  -  1 )  /  2 )  +  ( 2  / 
2 ) ) )
19236, 38dividi 9703 . . . . . . . . . . . 12  |-  ( 2  /  2 )  =  1
193192oveq2i 6051 . . . . . . . . . . 11  |-  ( ( ( P  -  1 )  /  2 )  +  ( 2  / 
2 ) )  =  ( ( ( P  -  1 )  / 
2 )  +  1 )
194191, 193syl6eq 2452 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  -  1 )  +  2 )  /  2
)  =  ( ( ( P  -  1 )  /  2 )  +  1 ) )
195188, 194eqtrd 2436 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  /  2
)  =  ( ( ( P  -  1 )  /  2 )  +  1 ) )
196 oddprm 13144 . . . . . . . . . . . . 13  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
19724, 196syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  1 )  /  2 )  e.  NN )
198197nnzd 10330 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  1 )  /  2 )  e.  ZZ )
199198adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  - 
1 )  /  2
)  e.  ZZ )
200199peano2zd 10334 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  -  1 )  / 
2 )  +  1 )  e.  ZZ )
201195, 200eqeltrd 2478 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  /  2
)  e.  ZZ )
202 simpr 448 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( R  + 
1 )  /  2
)  e.  ZZ )
203201, 202zsubcld 10336 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  +  1 )  / 
2 )  -  (
( R  +  1 )  /  2 ) )  e.  ZZ )
204183, 203eqeltrd 2478 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 )  e.  ZZ )
205 zeo 10311 . . . . . . 7  |-  ( R  e.  ZZ  ->  (
( R  /  2
)  e.  ZZ  \/  ( ( R  + 
1 )  /  2
)  e.  ZZ ) )
20633, 205syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( R  /  2
)  e.  ZZ  \/  ( ( R  + 
1 )  /  2
)  e.  ZZ ) )
20767, 204, 206mpjaodan 762 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  e.  ZZ )
208 m1expcl 11359 . . . . . . . . . . 11  |-  ( R  e.  ZZ  ->  ( -u 1 ^ R )  e.  ZZ )
20933, 208syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  ZZ )
210209, 33zmulcld 10337 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  R )  e.  ZZ )
211 zmodfz 11223 . . . . . . . . 9  |-  ( ( ( ( -u 1 ^ R )  x.  R
)  e.  ZZ  /\  P  e.  NN )  ->  ( ( ( -u
1 ^ R )  x.  R )  mod 
P )  e.  ( 0 ... ( P  -  1 ) ) )
212210, 27, 211syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  ( 0 ... ( P  -  1 ) ) )
213 elfznn0 11039 . . . . . . . 8  |-  ( ( ( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  ( 0 ... ( P  -  1 ) )  ->  ( (
( -u 1 ^ R
)  x.  R )  mod  P )  e. 
NN0 )
214212, 213syl 16 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  NN0 )
215214nn0red 10231 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  RR )
216 fzm1ndvds 12856 . . . . . . . . . . . 12  |-  ( ( P  e.  NN  /\  R  e.  ( 1 ... ( P  - 
1 ) ) )  ->  -.  P  ||  R
)
21727, 137, 216syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  R )
218 divneg2 9694 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  =/=  0 )  ->  -u (
1  /  1 )  =  ( 1  /  -u 1 ) )
2193, 3, 4, 218mp3an 1279 . . . . . . . . . . . . . . . . . . 19  |-  -u (
1  /  1 )  =  ( 1  /  -u 1 )
2203, 4dividi 9703 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  1 )  =  1
221220negeqi 9255 . . . . . . . . . . . . . . . . . . 19  |-  -u (
1  /  1 )  =  -u 1
222219, 221eqtr3i 2426 . . . . . . . . . . . . . . . . . 18  |-  ( 1  /  -u 1 )  = 
-u 1
223222oveq1i 6050 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  -u 1
) ^ R )  =  ( -u 1 ^ R )
2241a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  e.  CC )
2255a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  =/=  0 )
226224, 225, 33exprecd 11486 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( 1  /  -u 1
) ^ R )  =  ( 1  / 
( -u 1 ^ R
) ) )
227223, 226syl5eqr 2450 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  =  ( 1  / 
( -u 1 ^ R
) ) )
228227oveq2d 6056 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( -u
1 ^ R ) )  =  ( (
-u 1 ^ R
)  x.  ( 1  /  ( -u 1 ^ R ) ) ) )
229209zcnd 10332 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  CC )
230224, 225, 33expne0d 11484 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  =/=  0 )
231229, 230recidd 9741 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( 1  /  ( -u 1 ^ R ) ) )  =  1 )
232228, 231eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( -u
1 ^ R ) )  =  1 )
233232oveq1d 6055 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  ( -u 1 ^ R ) )  x.  R )  =  ( 1  x.  R ) )
234229, 229, 34mulassd 9067 . . . . . . . . . . . . 13  |-  ( (
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 ) ) )
23534mulid2d 9062 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  R )  =  R )
236233, 234, 2353eqtr3d 2444 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( (
-u 1 ^ R
)  x.  R ) )  =  R )
237236breq2d 4184 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( ( -u
1 ^ R )  x.  ( ( -u
1 ^ R )  x.  R ) )  <-> 
P  ||  R )
)
238217, 237mtbird 293 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  ( ( -u
1 ^ R )  x.  ( ( -u
1 ^ R )  x.  R ) ) )
239 dvdsmultr2 12840 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
240106, 209, 210, 239syl3anc 1184 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( ( -u
1 ^ R )  x.  R )  ->  P  ||  ( ( -u
1 ^ R )  x.  ( ( -u
1 ^ R )  x.  R ) ) ) )
241238, 240mtod 170 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  ( ( -u
1 ^ R )  x.  R ) )
242 dvdsval3 12811 . . . . . . . . . 10  |-  ( ( P  e.  NN  /\  ( ( -u 1 ^ R )  x.  R
)  e.  ZZ )  ->  ( P  ||  ( ( -u 1 ^ R )  x.  R
)  <->  ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  =  0 ) )
24327, 210, 242syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( ( -u
1 ^ R )  x.  R )  <->  ( (
( -u 1 ^ R
)  x.  R )  mod  P )  =  0 ) )
244241, 243mtbid 292 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  ( ( ( -u
1 ^ R )  x.  R )  mod 
P )  =  0 )
245 elnn0 10179 . . . . . . . . . 10  |-  ( ( ( ( -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 ) )
246214, 245sylib 189 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  e.  NN  \/  ( ( ( -u
1 ^ R )  x.  R )  mod 
P )  =  0 ) )
247246ord 367 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -.  ( ( ( -u
1 ^ R )  x.  R )  mod 
P )  e.  NN  ->  ( ( ( -u
1 ^ R )  x.  R )  mod 
P )  =  0 ) )
248244, 247mt3d 119 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  NN )
249248nngt0d 9999 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <  ( ( ( -u
1 ^ R )  x.  R )  mod 
P ) )
250215, 99, 249, 101divgt0d 9902 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
251 elnnz 10248 . . . . 5  |-  ( ( ( ( ( -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 ) ) )
252207, 250, 251sylanbrc 646 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  e.  NN )
253252nnge1d 9998 . . 3  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  <_  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
254 elfzle2 11017 . . . . 5  |-  ( ( ( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  ( 0 ... ( P  -  1 ) )  ->  ( (
( -u 1 ^ R
)  x.  R )  mod  P )  <_ 
( P  -  1 ) )
255212, 254syl 16 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  <_  ( P  -  1 ) )
256 lediv1 9831 . . . . 5  |-  ( ( ( ( ( -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
) ) )
257215, 97, 99, 101, 256syl112anc 1188 . . . 4  |-  ( (
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 ) ) )
258255, 257mpbid 202 . . 3  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  <_  ( ( P  -  1 )  /  2 ) )
259 elfz 11005 . . . 4  |-  ( ( ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 )  e.  ZZ  /\  1  e.  ZZ  /\  ( ( P  - 
1 )  /  2
)  e.  ZZ )  ->  ( ( ( ( ( -u 1 ^ R )  x.  R
)  mod  P )  /  2 )  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  <->  ( 1  <_ 
( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 )  /\  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  <_  ( ( P  -  1 )  /  2 ) ) ) )
260207, 78, 198, 259syl3anc 1184 . . 3  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 )  e.  ( 1 ... ( ( P  -  1 )  /  2 ) )  <-> 
( 1  <_  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  /\  ( (
( ( -u 1 ^ R )  x.  R
)  mod  P )  /  2 )  <_ 
( ( P  - 
1 )  /  2
) ) ) )
261253, 258, 260mpbir2and 889 . 2  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  e.  ( 1 ... ( ( P  -  1 )  / 
2 ) ) )
262 lgseisen.5 . 2  |-  M  =  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
263261, 262fmptd 5852 1  |-  ( ph  ->  M : ( 1 ... ( ( P  -  1 )  / 
2 ) ) --> ( 1 ... ( ( P  -  1 )  /  2 ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1721    =/= wne 2567    \ cdif 3277   {csn 3774   class class class wbr 4172    e. cmpt 4226   -->wf 5409   ` cfv 5413  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947    + caddc 8949    x. cmul 8951    < clt 9076    <_ cle 9077    - cmin 9247   -ucneg 9248    / cdiv 9633   NNcn 9956   2c2 10005   NN0cn0 10177   ZZcz 10238   ZZ>=cuz 10444   RR+crp 10568   ...cfz 10999    mod cmo 11205   ^cexp 11337    || cdivides 12807    gcd cgcd 12961   Primecprime 13034
This theorem is referenced by:  lgseisenlem2  21087  lgseisenlem3  21088
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fz 11000  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-dvds 12808  df-gcd 12962  df-prm 13035
  Copyright terms: Public domain W3C validator