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

Theorem lgseisenlem1 20551
Description: Lemma for lgseisen 20555. 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 9781 . . . . . . . . . . . . . . 15  |-  -u 1  e.  CC
21a1i 12 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  -u 1  e.  CC )
3 ax-1cn 8763 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
4 ax-1ne0 8774 . . . . . . . . . . . . . . . 16  |-  1  =/=  0
53, 4negne0i 9089 . . . . . . . . . . . . . . 15  |-  -u 1  =/=  0
65a1i 12 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  -u 1  =/=  0 )
7 2z 10022 . . . . . . . . . . . . . . 15  |-  2  e.  ZZ
87a1i 12 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  2  e.  ZZ )
9 simpr 449 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( R  /  2 )  e.  ZZ )
10 expmulz 11115 . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ( Prime  \  { 2 } ) )
15 eldifi 3273 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( Q  e.  ( Prime  \  {
2 } )  ->  Q  e.  Prime )
1614, 15syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  Prime )
17 prmz 12724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
1816, 17syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ZZ )
19 elfzelz 10765 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  ZZ )
2019adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  ZZ )
21 zmulcl 10034 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  e.  ZZ  /\  x  e.  ZZ )  ->  ( 2  x.  x
)  e.  ZZ )
227, 20, 21sylancr 647 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  ZZ )
2318, 22zmulcld 10091 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  ZZ )
24 lgseisen.1 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
2524adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ( Prime  \  { 2 } ) )
26 eldifi 3273 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  e.  Prime )
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  Prime )
28 prmnn 12725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  Prime  ->  P  e.  NN )
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  NN )
30 zmodfz 10958 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( Q  x.  (
2  x.  x ) )  e.  ZZ  /\  P  e.  NN )  ->  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)  e.  ( 0 ... ( P  - 
1 ) ) )
3123, 29, 30syl2anc 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  e.  ( 0 ... ( P  -  1 ) ) )
3212, 31syl5eqel 2342 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ( 0 ... ( P  -  1 ) ) )
33 elfznn0 10789 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  ( 0 ... ( P  -  1 ) )  ->  R  e.  NN0 )
3432, 33syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN0 )
3534nn0zd 10083 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ZZ )
3635zcnd 10086 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  CC )
3736adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  R  e.  CC )
38 2cn 9784 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
3938a1i 12 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  2  e.  CC )
40 2ne0 9797 . . . . . . . . . . . . . . . 16  |-  2  =/=  0
4140a1i 12 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  2  =/=  0 )
4237, 39, 41divcan2d 9506 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
2  x.  ( R  /  2 ) )  =  R )
4342oveq2d 5808 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( -u 1 ^ ( 2  x.  ( R  / 
2 ) ) )  =  ( -u 1 ^ R ) )
44 sqneg 11131 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  CC  ->  ( -u 1 ^ 2 )  =  ( 1 ^ 2 ) )
453, 44ax-mp 10 . . . . . . . . . . . . . . . 16  |-  ( -u
1 ^ 2 )  =  ( 1 ^ 2 )
46 sq1 11165 . . . . . . . . . . . . . . . 16  |-  ( 1 ^ 2 )  =  1
4745, 46eqtri 2278 . . . . . . . . . . . . . . 15  |-  ( -u
1 ^ 2 )  =  1
4847oveq1i 5802 . . . . . . . . . . . . . 14  |-  ( (
-u 1 ^ 2 ) ^ ( R  /  2 ) )  =  ( 1 ^ ( R  /  2
) )
49 1exp 11098 . . . . . . . . . . . . . . 15  |-  ( ( R  /  2 )  e.  ZZ  ->  (
1 ^ ( R  /  2 ) )  =  1 )
5049adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
1 ^ ( R  /  2 ) )  =  1 )
5148, 50syl5eq 2302 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( -u 1 ^ 2 ) ^ ( R  /  2 ) )  =  1 )
5211, 43, 513eqtr3d 2298 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( -u 1 ^ R )  =  1 )
5352oveq1d 5807 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( -u 1 ^ R
)  x.  R )  =  ( 1  x.  R ) )
5437mulid2d 8821 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
1  x.  R )  =  R )
5553, 54eqtrd 2290 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( -u 1 ^ R
)  x.  R )  =  R )
5655oveq1d 5807 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  =  ( R  mod  P ) )
5734nn0red 9987 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  RR )
5829nnrpd 10357 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR+ )
5934nn0ge0d 9989 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <_  R )
6023zred 10085 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  RR )
61 modlt 10948 . . . . . . . . . . . . 13  |-  ( ( ( Q  x.  (
2  x.  x ) )  e.  RR  /\  P  e.  RR+ )  -> 
( ( Q  x.  ( 2  x.  x
) )  mod  P
)  <  P )
6260, 58, 61syl2anc 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  <  P )
6312, 62syl5eqbr 4030 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  <  P )
64 modid 10960 . . . . . . . . . . 11  |-  ( ( ( R  e.  RR  /\  P  e.  RR+ )  /\  ( 0  <_  R  /\  R  <  P ) )  ->  ( R  mod  P )  =  R )
6557, 58, 59, 63, 64syl22anc 1188 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( R  mod  P )  =  R )
6665adantr 453 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( R  mod  P )  =  R )
6756, 66eqtrd 2290 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  =  R )
6867oveq1d 5807 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  =  ( R  /  2 ) )
6968, 9eqeltrd 2332 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  e.  ZZ )
7029nncnd 9730 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  CC )
7170mulid2d 8821 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  P )  =  P )
7271oveq2d 5808 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u R  +  ( 1  x.  P ) )  =  ( -u R  +  P ) )
7357renegcld 9178 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u R  e.  RR )
7473recnd 8829 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u R  e.  CC )
7570, 74addcomd 8982 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  +  -u R )  =  ( -u R  +  P ) )
7670, 36negsubd 9131 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  +  -u R )  =  ( P  -  R ) )
7772, 75, 763eqtr2d 2296 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u R  +  ( 1  x.  P ) )  =  ( P  -  R ) )
7877oveq1d 5807 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u R  +  ( 1  x.  P ) )  mod  P )  =  ( ( P  -  R )  mod 
P ) )
79 1z 10021 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
8079a1i 12 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  e.  ZZ )
81 modcyc 10966 . . . . . . . . . . . . 13  |-  ( (
-u R  e.  RR  /\  P  e.  RR+  /\  1  e.  ZZ )  ->  (
( -u R  +  ( 1  x.  P ) )  mod  P )  =  ( -u R  mod  P ) )
8273, 58, 80, 81syl3anc 1187 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u R  +  ( 1  x.  P ) )  mod  P )  =  ( -u R  mod  P ) )
8329nnred 9729 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR )
8483, 57resubcld 9179 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  R )  e.  RR )
8557, 83, 63ltled 8935 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  <_  P )
8683, 57subge0d 9330 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
0  <_  ( P  -  R )  <->  R  <_  P ) )
8785, 86mpbird 225 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <_  ( P  -  R
) )
88 2nn 9845 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  NN
89 elfznn 10786 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  NN )
9089adantl 454 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  NN )
91 nnmulcl 9737 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2  e.  NN  /\  x  e.  NN )  ->  ( 2  x.  x
)  e.  NN )
9288, 90, 91sylancr 647 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  NN )
93 elfzle2 10767 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  <_  ( ( P  - 
1 )  /  2
) )
9493adantl 454 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  <_  ( ( P  - 
1 )  /  2
) )
9590nnred 9729 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  RR )
96 prmuz2 12739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
97 uz2m1nn 10260 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  ( ZZ>= `  2
)  ->  ( P  -  1 )  e.  NN )
9827, 96, 973syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  NN )
9998nnred 9729 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  RR )
100 2re 9783 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  2  e.  RR
101100a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  RR )
102 2pos 9796 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <  2
103102a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <  2 )
104 lemuldiv2 9604 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  RR  /\  ( P  -  1
)  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
2  x.  x )  <_  ( P  - 
1 )  <->  x  <_  ( ( P  -  1 )  /  2 ) ) )
10595, 99, 101, 103, 104syl112anc 1191 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( 2  x.  x
)  <_  ( P  -  1 )  <->  x  <_  ( ( P  -  1 )  /  2 ) ) )
10694, 105mpbird 225 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  <_  ( P  - 
1 ) )
107 prmz 12724 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( P  e.  Prime  ->  P  e.  ZZ )
10827, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
109 peano2zm 10030 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e.  ZZ  ->  ( P  -  1 )  e.  ZZ )
110108, 109syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  ZZ )
111 fznn 10819 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( P  -  1 )  e.  ZZ  ->  (
( 2  x.  x
)  e.  ( 1 ... ( P  - 
1 ) )  <->  ( (
2  x.  x )  e.  NN  /\  (
2  x.  x )  <_  ( P  - 
1 ) ) ) )
112110, 111syl 17 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
11392, 106, 112mpbir2and 893 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  ( 1 ... ( P  -  1 ) ) )
114 fzm1ndvds 12543 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( P  e.  NN  /\  ( 2  x.  x
)  e.  ( 1 ... ( P  - 
1 ) ) )  ->  -.  P  ||  (
2  x.  x ) )
11529, 113, 114syl2anc 645 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  ( 2  x.  x ) )
116 lgseisen.3 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  =/=  Q )
117116adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  =/=  Q )
118 prmrp 12743 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( P  e.  Prime  /\  Q  e.  Prime )  ->  (
( P  gcd  Q
)  =  1  <->  P  =/=  Q ) )
11927, 16, 118syl2anc 645 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  gcd  Q
)  =  1  <->  P  =/=  Q ) )
120117, 119mpbird 225 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  gcd  Q )  =  1 )
121 coprmdvds 12744 . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
122108, 18, 22, 121syl3anc 1187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  ||  ( Q  x.  ( 2  x.  x ) )  /\  ( P  gcd  Q )  =  1 )  ->  P  ||  (
2  x.  x ) ) )
123120, 122mpan2d 658 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( Q  x.  ( 2  x.  x
) )  ->  P  ||  ( 2  x.  x
) ) )
124115, 123mtod 170 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  ( Q  x.  ( 2  x.  x
) ) )
125 divides3 12498 . . . . . . . . . . . . . . . . . . . . 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 ) )
12629, 23, 125syl2anc 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( Q  x.  ( 2  x.  x
) )  <->  ( ( Q  x.  ( 2  x.  x ) )  mod  P )  =  0 ) )
127124, 126mtbid 293 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)  =  0 )
12812eqeq1i 2265 . . . . . . . . . . . . . . . . . . 19  |-  ( R  =  0  <->  ( ( Q  x.  ( 2  x.  x ) )  mod  P )  =  0 )
129127, 128sylnibr 298 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  R  =  0 )
13098nnnn0d 9986 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  NN0 )
131 nn0uz 10230 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  =  ( ZZ>= `  0 )
132130, 131syl6eleq 2348 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  ( ZZ>= `  0
) )
133 elfzp12 10828 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P  -  1 )  e.  ( ZZ>= `  0
)  ->  ( R  e.  ( 0 ... ( P  -  1 ) )  <->  ( R  =  0  \/  R  e.  ( ( 0  +  1 ) ... ( P  -  1 ) ) ) ) )
134132, 133syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( R  e.  ( 0 ... ( P  - 
1 ) )  <->  ( R  =  0  \/  R  e.  ( ( 0  +  1 ) ... ( P  -  1 ) ) ) ) )
13532, 134mpbid 203 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( R  =  0  \/  R  e.  ( (
0  +  1 ) ... ( P  - 
1 ) ) ) )
136135ord 368 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -.  R  =  0  ->  R  e.  ( ( 0  +  1 ) ... ( P  - 
1 ) ) ) )
137129, 136mpd 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ( ( 0  +  1 ) ... ( P  -  1 ) ) )
138 1e0p1 10120 . . . . . . . . . . . . . . . . . 18  |-  1  =  ( 0  +  1 )
139138oveq1i 5802 . . . . . . . . . . . . . . . . 17  |-  ( 1 ... ( P  - 
1 ) )  =  ( ( 0  +  1 ) ... ( P  -  1 ) )
140137, 139syl6eleqr 2349 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ( 1 ... ( P  -  1 ) ) )
141 elfznn 10786 . . . . . . . . . . . . . . . 16  |-  ( R  e.  ( 1 ... ( P  -  1 ) )  ->  R  e.  NN )
142140, 141syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN )
143142nnrpd 10357 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  RR+ )
14483, 143ltsubrpd 10386 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  R )  <  P )
145 modid 10960 . . . . . . . . . . . . 13  |-  ( ( ( ( P  -  R )  e.  RR  /\  P  e.  RR+ )  /\  ( 0  <_  ( P  -  R )  /\  ( P  -  R
)  <  P )
)  ->  ( ( P  -  R )  mod  P )  =  ( P  -  R ) )
14684, 58, 87, 144, 145syl22anc 1188 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  R
)  mod  P )  =  ( P  -  R ) )
14778, 82, 1463eqtr3d 2298 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u R  mod  P )  =  ( P  -  R ) )
148147adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u R  mod  P
)  =  ( P  -  R ) )
1493a1i 12 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
1  e.  CC )
150142adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  R  e.  NN )
1517a1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  ZZ )
15240a1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  =/=  0 )
15335peano2zd 10088 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( R  +  1 )  e.  ZZ )
154 divides2 12497 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  ZZ  /\  2  =/=  0  /\  ( R  +  1 )  e.  ZZ )  -> 
( 2  ||  ( R  +  1 )  <-> 
( ( R  + 
1 )  /  2
)  e.  ZZ ) )
155151, 152, 153, 154syl3anc 1187 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  ||  ( R  +  1 )  <->  ( ( R  +  1 )  /  2 )  e.  ZZ ) )
156155biimpar 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
2  ||  ( R  +  1 ) )
15735adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  R  e.  ZZ )
15888a1i 12 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
2  e.  NN )
159 1lt2 9854 . . . . . . . . . . . . . . . . . 18  |-  1  <  2
160159a1i 12 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
1  <  2 )
161 ndvdsp1 12571 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  ZZ  /\  2  e.  NN  /\  1  <  2 )  ->  (
2  ||  R  ->  -.  2  ||  ( R  +  1 ) ) )
162157, 158, 160, 161syl3anc 1187 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( 2  ||  R  ->  -.  2  ||  ( R  +  1 ) ) )
163156, 162mt2d 111 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  -.  2  ||  R )
164 oexpneg 12553 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  R  e.  NN  /\  -.  2  ||  R )  -> 
( -u 1 ^ R
)  =  -u (
1 ^ R ) )
165149, 150, 163, 164syl3anc 1187 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u 1 ^ R
)  =  -u (
1 ^ R ) )
166 1exp 11098 . . . . . . . . . . . . . . . 16  |-  ( R  e.  ZZ  ->  (
1 ^ R )  =  1 )
167157, 166syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( 1 ^ R
)  =  1 )
168167negeqd 9014 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  -u ( 1 ^ R
)  =  -u 1
)
169165, 168eqtrd 2290 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u 1 ^ R
)  =  -u 1
)
170169oveq1d 5807 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( -u 1 ^ R )  x.  R
)  =  ( -u
1  x.  R ) )
17136adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  R  e.  CC )
172171mulm1d 9199 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u 1  x.  R
)  =  -u R
)
173170, 172eqtrd 2290 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( -u 1 ^ R )  x.  R
)  =  -u R
)
174173oveq1d 5807 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  =  (
-u R  mod  P
) )
17570adantr 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  P  e.  CC )
176175, 171, 149pnpcan2d 9163 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  -  ( R  +  1 ) )  =  ( P  -  R ) )
177148, 174, 1763eqtr4d 2300 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  =  ( ( P  +  1 )  -  ( R  +  1 ) ) )
178177oveq1d 5807 . . . . . . . 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 ) )
179 peano2cn 8952 . . . . . . . . . 10  |-  ( P  e.  CC  ->  ( P  +  1 )  e.  CC )
180175, 179syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( P  +  1 )  e.  CC )
181 peano2cn 8952 . . . . . . . . . 10  |-  ( R  e.  CC  ->  ( R  +  1 )  e.  CC )
182171, 181syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( R  +  1 )  e.  CC )
18338a1i 12 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
2  e.  CC )
18440a1i 12 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
2  =/=  0 )
185180, 182, 183, 184divsubdird 9543 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  +  1 )  -  ( R  +  1
) )  /  2
)  =  ( ( ( P  +  1 )  /  2 )  -  ( ( R  +  1 )  / 
2 ) ) )
186178, 185eqtrd 2290 . . . . . . 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 ) ) )
187175, 149, 183subadd23d 9147 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  - 
1 )  +  2 )  =  ( P  +  ( 2  -  1 ) ) )
188 1p1e2 9808 . . . . . . . . . . . . . 14  |-  ( 1  +  1 )  =  2
18938, 3, 3, 188subaddrii 9103 . . . . . . . . . . . . 13  |-  ( 2  -  1 )  =  1
190189oveq2i 5803 . . . . . . . . . . . 12  |-  ( P  +  ( 2  -  1 ) )  =  ( P  +  1 )
191187, 190syl6req 2307 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( P  +  1 )  =  ( ( P  -  1 )  +  2 ) )
192191oveq1d 5807 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  /  2
)  =  ( ( ( P  -  1 )  +  2 )  /  2 ) )
19398nncnd 9730 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  CC )
194193adantr 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( P  -  1 )  e.  CC )
195194, 183, 183, 184divdird 9542 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  -  1 )  +  2 )  /  2
)  =  ( ( ( P  -  1 )  /  2 )  +  ( 2  / 
2 ) ) )
19638, 40dividi 9461 . . . . . . . . . . . 12  |-  ( 2  /  2 )  =  1
197196oveq2i 5803 . . . . . . . . . . 11  |-  ( ( ( P  -  1 )  /  2 )  +  ( 2  / 
2 ) )  =  ( ( ( P  -  1 )  / 
2 )  +  1 )
198195, 197syl6eq 2306 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  -  1 )  +  2 )  /  2
)  =  ( ( ( P  -  1 )  /  2 )  +  1 ) )
199192, 198eqtrd 2290 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  /  2
)  =  ( ( ( P  -  1 )  /  2 )  +  1 ) )
200 oddprm 12831 . . . . . . . . . . . . 13  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
20125, 200syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  1 )  /  2 )  e.  NN )
202201nnzd 10084 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  1 )  /  2 )  e.  ZZ )
203202adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  - 
1 )  /  2
)  e.  ZZ )
204203peano2zd 10088 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  -  1 )  / 
2 )  +  1 )  e.  ZZ )
205199, 204eqeltrd 2332 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  /  2
)  e.  ZZ )
206 simpr 449 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( R  + 
1 )  /  2
)  e.  ZZ )
207205, 206zsubcld 10090 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  +  1 )  / 
2 )  -  (
( R  +  1 )  /  2 ) )  e.  ZZ )
208186, 207eqeltrd 2332 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 )  e.  ZZ )
209 zeo 10065 . . . . . . 7  |-  ( R  e.  ZZ  ->  (
( R  /  2
)  e.  ZZ  \/  ( ( R  + 
1 )  /  2
)  e.  ZZ ) )
21035, 209syl 17 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( R  /  2
)  e.  ZZ  \/  ( ( R  + 
1 )  /  2
)  e.  ZZ ) )
21169, 208, 210mpjaodan 764 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  e.  ZZ )
212 m1expcl 11093 . . . . . . . . . . 11  |-  ( R  e.  ZZ  ->  ( -u 1 ^ R )  e.  ZZ )
21335, 212syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  ZZ )
214213, 35zmulcld 10091 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  R )  e.  ZZ )
215 zmodfz 10958 . . . . . . . . 9  |-  ( ( ( ( -u 1 ^ R )  x.  R
)  e.  ZZ  /\  P  e.  NN )  ->  ( ( ( -u
1 ^ R )  x.  R )  mod 
P )  e.  ( 0 ... ( P  -  1 ) ) )
216214, 29, 215syl2anc 645 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  ( 0 ... ( P  -  1 ) ) )
217 elfznn0 10789 . . . . . . . 8  |-  ( ( ( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  ( 0 ... ( P  -  1 ) )  ->  ( (
( -u 1 ^ R
)  x.  R )  mod  P )  e. 
NN0 )
218216, 217syl 17 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  NN0 )
219218nn0red 9987 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  RR )
220 fzm1ndvds 12543 . . . . . . . . . . . 12  |-  ( ( P  e.  NN  /\  R  e.  ( 1 ... ( P  - 
1 ) ) )  ->  -.  P  ||  R
)
22129, 140, 220syl2anc 645 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  R )
222 divneg2 9452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  =/=  0 )  ->  -u (
1  /  1 )  =  ( 1  /  -u 1 ) )
2233, 3, 4, 222mp3an 1282 . . . . . . . . . . . . . . . . . . 19  |-  -u (
1  /  1 )  =  ( 1  /  -u 1 )
2243, 4dividi 9461 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  1 )  =  1
225224negeqi 9013 . . . . . . . . . . . . . . . . . . 19  |-  -u (
1  /  1 )  =  -u 1
226223, 225eqtr3i 2280 . . . . . . . . . . . . . . . . . 18  |-  ( 1  /  -u 1 )  = 
-u 1
227226oveq1i 5802 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  -u 1
) ^ R )  =  ( -u 1 ^ R )
2281a1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  e.  CC )
2295a1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  =/=  0 )
230228, 229, 35exprecd 11220 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( 1  /  -u 1
) ^ R )  =  ( 1  / 
( -u 1 ^ R
) ) )
231227, 230syl5eqr 2304 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  =  ( 1  / 
( -u 1 ^ R
) ) )
232231oveq2d 5808 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( -u
1 ^ R ) )  =  ( (
-u 1 ^ R
)  x.  ( 1  /  ( -u 1 ^ R ) ) ) )
233213zcnd 10086 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  CC )
234228, 229, 35expne0d 11218 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  =/=  0 )
235233, 234recidd 9499 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( 1  /  ( -u 1 ^ R ) ) )  =  1 )
236232, 235eqtrd 2290 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( -u
1 ^ R ) )  =  1 )
237236oveq1d 5807 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  ( -u 1 ^ R ) )  x.  R )  =  ( 1  x.  R ) )
238233, 233, 36mulassd 8826 . . . . . . . . . . . . 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 ) ) )
23936mulid2d 8821 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  R )  =  R )
240237, 238, 2393eqtr3d 2298 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( (
-u 1 ^ R
)  x.  R ) )  =  R )
241240breq2d 4009 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( ( -u
1 ^ R )  x.  ( ( -u
1 ^ R )  x.  R ) )  <-> 
P  ||  R )
)
242221, 241mtbird 294 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  ( ( -u
1 ^ R )  x.  ( ( -u
1 ^ R )  x.  R ) ) )
243 dvdsmultr2 12527 . . . . . . . . . . 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 ) ) ) )
244108, 213, 214, 243syl3anc 1187 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( ( -u
1 ^ R )  x.  R )  ->  P  ||  ( ( -u
1 ^ R )  x.  ( ( -u
1 ^ R )  x.  R ) ) ) )
245242, 244mtod 170 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  ( ( -u
1 ^ R )  x.  R ) )
246 divides3 12498 . . . . . . . . . 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 ) )
24729, 214, 246syl2anc 645 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  ( ( -u
1 ^ R )  x.  R )  <->  ( (
( -u 1 ^ R
)  x.  R )  mod  P )  =  0 ) )
248245, 247mtbid 293 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  ( ( ( -u
1 ^ R )  x.  R )  mod 
P )  =  0 )
249 elnn0 9935 . . . . . . . . . 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 ) )
250218, 249sylib 190 . . . . . . . . 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 ) )
251250ord 368 . . . . . . . 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 ) )
252248, 251mt3d 119 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  NN )
253252nngt0d 9757 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <  ( ( ( -u
1 ^ R )  x.  R )  mod 
P ) )
254219, 101, 253, 103divgt0d 9660 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
255 elnnz 10002 . . . . 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 ) ) )
256211, 254, 255sylanbrc 648 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  e.  NN )
257256nnge1d 9756 . . 3  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  <_  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
258 elfzle2 10767 . . . . 5  |-  ( ( ( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  ( 0 ... ( P  -  1 ) )  ->  ( (
( -u 1 ^ R
)  x.  R )  mod  P )  <_ 
( P  -  1 ) )
259216, 258syl 17 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  <_  ( P  -  1 ) )
260 lediv1 9589 . . . . 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
) ) )
261219, 99, 101, 103, 260syl112anc 1191 . . . 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 ) ) )
262259, 261mpbid 203 . . 3  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  <_  ( ( P  -  1 )  /  2 ) )
263 elfz 10755 . . . 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 ) ) ) )
264211, 80, 202, 263syl3anc 1187 . . 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
) ) ) )
265257, 262, 264mpbir2and 893 . 2  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  e.  ( 1 ... ( ( P  -  1 )  / 
2 ) ) )
266 lgseisen.5 . 2  |-  M  =  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
267265, 266fmptd 5618 1  |-  ( ph  ->  M : ( 1 ... ( ( P  -  1 )  / 
2 ) ) --> ( 1 ... ( ( P  -  1 )  /  2 ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    \/ wo 359    /\ wa 360    = wceq 1619    e. wcel 1621    =/= wne 2421    \ cdif 3124   {csn 3614   class class class wbr 3997    e. cmpt 4051   -->wf 4669   ` cfv 4673  (class class class)co 5792   CCcc 8703   RRcr 8704   0cc0 8705   1c1 8706    + caddc 8708    x. cmul 8710    < clt 8835    <_ cle 8836    - cmin 9005   -ucneg 9006    / cdiv 9391   NNcn 9714   2c2 9763   NN0cn0 9933   ZZcz 9992   ZZ>=cuz 10198   RR+crp 10322   ...cfz 10749    mod cmo 10940   ^cexp 11071    || cdivides 12494    gcd cgcd 12648   Primecprime 12721
This theorem is referenced by:  lgseisenlem2  20552  lgseisenlem3  20553
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484  ax-cnex 8761  ax-resscn 8762  ax-1cn 8763  ax-icn 8764  ax-addcl 8765  ax-addrcl 8766  ax-mulcl 8767  ax-mulrcl 8768  ax-mulcom 8769  ax-addass 8770  ax-mulass 8771  ax-distr 8772  ax-i2m1 8773  ax-1ne0 8774  ax-1rid 8775  ax-rnegex 8776  ax-rrecex 8777  ax-cnre 8778  ax-pre-lttri 8779  ax-pre-lttrn 8780  ax-pre-ltadd 8781  ax-pre-mulgt0 8782  ax-pre-sup 8783
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-nel 2424  df-ral 2523  df-rex 2524  df-reu 2525  df-rmo 2526  df-rab 2527  df-v 2765  df-sbc 2967  df-csb 3057  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-pss 3143  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-tp 3622  df-op 3623  df-uni 3802  df-int 3837  df-iun 3881  df-br 3998  df-opab 4052  df-mpt 4053  df-tr 4088  df-eprel 4277  df-id 4281  df-po 4286  df-so 4287  df-fr 4324  df-we 4326  df-ord 4367  df-on 4368  df-lim 4369  df-suc 4370  df-om 4629  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fn 4684  df-f 4685  df-f1 4686  df-fo 4687  df-f1o 4688  df-fv 4689  df-ov 5795  df-oprab 5796  df-mpt2 5797  df-1st 6056  df-2nd 6057  df-iota 6225  df-riota 6272  df-recs 6356  df-rdg 6391  df-1o 6447  df-2o 6448  df-oadd 6451  df-er 6628  df-en 6832  df-dom 6833  df-sdom 6834  df-fin 6835  df-sup 7162  df-pnf 8837  df-mnf 8838  df-xr 8839  df-ltxr 8840  df-le 8841  df-sub 9007  df-neg 9008  df-div 9392  df-n 9715  df-2 9772  df-3 9773  df-n0 9934  df-z 9993  df-uz 10199  df-rp 10323  df-fz 10750  df-fl 10892  df-mod 10941  df-seq 11014  df-exp 11072  df-cj 11550  df-re 11551  df-im 11552  df-sqr 11686  df-abs 11687  df-divides 12495  df-gcd 12649  df-prime 12722
  Copyright terms: Public domain W3C validator