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

Theorem lgseisenlem1 20515
Description: Lemma for lgseisen 20519. 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 9746 . . . . . . . . . . . . . . 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 8728 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
4 ax-1ne0 8739 . . . . . . . . . . . . . . . 16  |-  1  =/=  0
53, 4negne0i 9054 . . . . . . . . . . . . . . 15  |-  -u 1  =/=  0
65a1i 12 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  -u 1  =/=  0 )
7 2z 9986 . . . . . . . . . . . . . . 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 11079 . . . . . . . . . . . . . 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 3240 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( Q  e.  ( Prime  \  {
2 } )  ->  Q  e.  Prime )
1614, 15syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  Prime )
17 prmz 12688 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
1816, 17syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ZZ )
19 elfzelz 10729 . . . . . . . . . . . . . . . . . . . . . . . 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 9998 . . . . . . . . . . . . . . . . . . . . . . 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 10055 . . . . . . . . . . . . . . . . . . . . 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 3240 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  e.  Prime )
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  Prime )
28 prmnn 12689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  Prime  ->  P  e.  NN )
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  NN )
30 zmodfz 10922 . . . . . . . . . . . . . . . . . . . . 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 2340 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ( 0 ... ( P  -  1 ) ) )
33 elfznn0 10753 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  ( 0 ... ( P  -  1 ) )  ->  R  e.  NN0 )
3432, 33syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN0 )
3534nn0zd 10047 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ZZ )
3635zcnd 10050 . . . . . . . . . . . . . . . 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 9749 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
3938a1i 12 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  2  e.  CC )
40 2ne0 9762 . . . . . . . . . . . . . . . 16  |-  2  =/=  0
4140a1i 12 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  2  =/=  0 )
4237, 39, 41divcan2d 9471 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
2  x.  ( R  /  2 ) )  =  R )
4342oveq2d 5773 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( -u 1 ^ ( 2  x.  ( R  / 
2 ) ) )  =  ( -u 1 ^ R ) )
44 sqneg 11095 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  CC  ->  ( -u 1 ^ 2 )  =  ( 1 ^ 2 ) )
453, 44ax-mp 10 . . . . . . . . . . . . . . . 16  |-  ( -u
1 ^ 2 )  =  ( 1 ^ 2 )
46 sq1 11129 . . . . . . . . . . . . . . . 16  |-  ( 1 ^ 2 )  =  1
4745, 46eqtri 2276 . . . . . . . . . . . . . . 15  |-  ( -u
1 ^ 2 )  =  1
4847oveq1i 5767 . . . . . . . . . . . . . 14  |-  ( (
-u 1 ^ 2 ) ^ ( R  /  2 ) )  =  ( 1 ^ ( R  /  2
) )
49 1exp 11062 . . . . . . . . . . . . . . 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 2300 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( -u 1 ^ 2 ) ^ ( R  /  2 ) )  =  1 )
5211, 43, 513eqtr3d 2296 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  ( -u 1 ^ R )  =  1 )
5352oveq1d 5772 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( -u 1 ^ R
)  x.  R )  =  ( 1  x.  R ) )
5437mulid2d 8786 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
1  x.  R )  =  R )
5553, 54eqtrd 2288 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( -u 1 ^ R
)  x.  R )  =  R )
5655oveq1d 5772 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  =  ( R  mod  P ) )
5734nn0red 9951 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  RR )
5829nnrpd 10321 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR+ )
5934nn0ge0d 9953 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <_  R )
6023zred 10049 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  RR )
61 modlt 10912 . . . . . . . . . . . . 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 3996 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  <  P )
64 modid 10924 . . . . . . . . . . 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 2288 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  =  R )
6867oveq1d 5772 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  =  ( R  /  2 ) )
6968, 9eqeltrd 2330 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  ( R  /  2 )  e.  ZZ )  ->  (
( ( ( -u
1 ^ R )  x.  R )  mod 
P )  /  2
)  e.  ZZ )
7029nncnd 9695 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  CC )
7170mulid2d 8786 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  P )  =  P )
7271oveq2d 5773 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u R  +  ( 1  x.  P ) )  =  ( -u R  +  P ) )
7357renegcld 9143 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u R  e.  RR )
7473recnd 8794 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u R  e.  CC )
7570, 74addcomd 8947 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  +  -u R )  =  ( -u R  +  P ) )
7670, 36negsubd 9096 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  +  -u R )  =  ( P  -  R ) )
7772, 75, 763eqtr2d 2294 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u R  +  ( 1  x.  P ) )  =  ( P  -  R ) )
7877oveq1d 5772 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u R  +  ( 1  x.  P ) )  mod  P )  =  ( ( P  -  R )  mod 
P ) )
79 1z 9985 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
8079a1i 12 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  e.  ZZ )
81 modcyc 10930 . . . . . . . . . . . . 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 9694 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR )
8483, 57resubcld 9144 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  R )  e.  RR )
8557, 83, 63ltled 8900 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  <_  P )
8683, 57subge0d 9295 . . . . . . . . . . . . . 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 9809 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  NN
89 elfznn 10750 . . . . . . . . . . . . . . . . . . . . . . . . 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 9702 . . . . . . . . . . . . . . . . . . . . . . . 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 10731 . . . . . . . . . . . . . . . . . . . . . . . . 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 9694 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  RR )
96 prmuz2 12703 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
97 uz2m1nn 10224 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9694 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  RR )
100 2re 9748 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  2  e.  RR
101100a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  RR )
102 2pos 9761 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <  2
103102a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <  2 )
104 lemuldiv2 9569 . . . . . . . . . . . . . . . . . . . . . . . . 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 12688 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( P  e.  Prime  ->  P  e.  ZZ )
10827, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
109 peano2zm 9994 . . . . . . . . . . . . . . . . . . . . . . . . 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 10783 . . . . . . . . . . . . . . . . . . . . . . . 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 12507 . . . . . . . . . . . . . . . . . . . . . 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 12707 . . . . . . . . . . . . . . . . . . . . . . . 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 12708 . . . . . . . . . . . . . . . . . . . . . . 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 12462 . . . . . . . . . . . . . . . . . . . . 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 2263 . . . . . . . . . . . . . . . . . . 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 9950 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  NN0 )
131 nn0uz 10194 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  =  ( ZZ>= `  0 )
132130, 131syl6eleq 2346 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  1 )  e.  ( ZZ>= `  0
) )
133 elfzp12 10792 . . . . . . . . . . . . . . . . . . . . 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 10084 . . . . . . . . . . . . . . . . . 18  |-  1  =  ( 0  +  1 )
139138oveq1i 5767 . . . . . . . . . . . . . . . . 17  |-  ( 1 ... ( P  - 
1 ) )  =  ( ( 0  +  1 ) ... ( P  -  1 ) )
140137, 139syl6eleqr 2347 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ( 1 ... ( P  -  1 ) ) )
141 elfznn 10750 . . . . . . . . . . . . . . . 16  |-  ( R  e.  ( 1 ... ( P  -  1 ) )  ->  R  e.  NN )
142140, 141syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN )
143142nnrpd 10321 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  RR+ )
14483, 143ltsubrpd 10350 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  -  R )  <  P )
145 modid 10924 . . . . . . . . . . . . 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 2296 . . . . . . . . . . 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 10052 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( R  +  1 )  e.  ZZ )
154 divides2 12461 . . . . . . . . . . . . . . . . . 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 9818 . . . . . . . . . . . . . . . . . 18  |-  1  <  2
160159a1i 12 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
1  <  2 )
161 ndvdsp1 12535 . . . . . . . . . . . . . . . . 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 12517 . . . . . . . . . . . . . . 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 11062 . . . . . . . . . . . . . . . 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 8979 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  ->  -u ( 1 ^ R
)  =  -u 1
)
169165, 168eqtrd 2288 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u 1 ^ R
)  =  -u 1
)
170169oveq1d 5772 . . . . . . . . . . . 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 9164 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( -u 1  x.  R
)  =  -u R
)
173170, 172eqtrd 2288 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( -u 1 ^ R )  x.  R
)  =  -u R
)
174173oveq1d 5772 . . . . . . . . . 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 9128 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  -  ( R  +  1 ) )  =  ( P  -  R ) )
177148, 174, 1763eqtr4d 2298 . . . . . . . . 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 5772 . . . . . . . 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 8917 . . . . . . . . . 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 8917 . . . . . . . . . 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 9508 . . . . . . . 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 2288 . . . . . . 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 9112 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  - 
1 )  +  2 )  =  ( P  +  ( 2  -  1 ) ) )
188 1p1e2 9773 . . . . . . . . . . . . . 14  |-  ( 1  +  1 )  =  2
18938, 3, 3, 188subaddrii 9068 . . . . . . . . . . . . 13  |-  ( 2  -  1 )  =  1
190189oveq2i 5768 . . . . . . . . . . . 12  |-  ( P  +  ( 2  -  1 ) )  =  ( P  +  1 )
191187, 190syl6req 2305 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( P  +  1 )  =  ( ( P  -  1 )  +  2 ) )
192191oveq1d 5772 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  /  2
)  =  ( ( ( P  -  1 )  +  2 )  /  2 ) )
19398nncnd 9695 . . . . . . . . . . . . 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 9507 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  -  1 )  +  2 )  /  2
)  =  ( ( ( P  -  1 )  /  2 )  +  ( 2  / 
2 ) ) )
19638, 40dividi 9426 . . . . . . . . . . . 12  |-  ( 2  /  2 )  =  1
197196oveq2i 5768 . . . . . . . . . . 11  |-  ( ( ( P  -  1 )  /  2 )  +  ( 2  / 
2 ) )  =  ( ( ( P  -  1 )  / 
2 )  +  1 )
198195, 197syl6eq 2304 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  -  1 )  +  2 )  /  2
)  =  ( ( ( P  -  1 )  /  2 )  +  1 ) )
199192, 198eqtrd 2288 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( P  + 
1 )  /  2
)  =  ( ( ( P  -  1 )  /  2 )  +  1 ) )
200 oddprm 12795 . . . . . . . . . . . . 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 10048 . . . . . . . . . . 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 10052 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  -  1 )  / 
2 )  +  1 )  e.  ZZ )
205199, 204eqeltrd 2330 . . . . . . . 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 10054 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  /\  (
( R  +  1 )  /  2 )  e.  ZZ )  -> 
( ( ( P  +  1 )  / 
2 )  -  (
( R  +  1 )  /  2 ) )  e.  ZZ )
208186, 207eqeltrd 2330 . . . . . 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 10029 . . . . . . 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 11057 . . . . . . . . . . 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 10055 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  R )  e.  ZZ )
215 zmodfz 10922 . . . . . . . . 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 10753 . . . . . . . 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 9951 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  R
)  mod  P )  e.  RR )
220 fzm1ndvds 12507 . . . . . . . . . . . 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 9417 . . . . . . . . . . . . . . . . . . . 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 9426 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  1 )  =  1
225224negeqi 8978 . . . . . . . . . . . . . . . . . . 19  |-  -u (
1  /  1 )  =  -u 1
226223, 225eqtr3i 2278 . . . . . . . . . . . . . . . . . 18  |-  ( 1  /  -u 1 )  = 
-u 1
227226oveq1i 5767 . . . . . . . . . . . . . . . . 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 11184 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( 1  /  -u 1
) ^ R )  =  ( 1  / 
( -u 1 ^ R
) ) )
231227, 230syl5eqr 2302 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  =  ( 1  / 
( -u 1 ^ R
) ) )
232231oveq2d 5773 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( -u
1 ^ R ) )  =  ( (
-u 1 ^ R
)  x.  ( 1  /  ( -u 1 ^ R ) ) ) )
233213zcnd 10050 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  CC )
234228, 229, 35expne0d 11182 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  =/=  0 )
235233, 234recidd 9464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( 1  /  ( -u 1 ^ R ) ) )  =  1 )
236232, 235eqtrd 2288 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( -u
1 ^ R ) )  =  1 )
237236oveq1d 5772 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ R )  x.  ( -u 1 ^ R ) )  x.  R )  =  ( 1  x.  R ) )
238233, 233, 36mulassd 8791 . . . . . . . . . . . . 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 8786 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  R )  =  R )
240237, 238, 2393eqtr3d 2296 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  ( (
-u 1 ^ R
)  x.  R ) )  =  R )
241240breq2d 3975 . . . . . . . . . . 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 12491 . . . . . . . . . . 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 12462 . . . . . . . . . 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 9899 . . . . . . . . . 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 9722 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <  ( ( ( -u
1 ^ R )  x.  R )  mod 
P ) )
254219, 101, 253, 103divgt0d 9625 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  0  <  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
255 elnnz 9966 . . . . 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 9721 . . 3  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  <_  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
258 elfzle2 10731 . . . . 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 9554 . . . . 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 10719 . . . 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 5583 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 2419    \ cdif 3091   {csn 3581   class class class wbr 3963    e. cmpt 4017   -->wf 4634   ` cfv 4638  (class class class)co 5757   CCcc 8668   RRcr 8669   0cc0 8670   1c1 8671    + caddc 8673    x. cmul 8675    < clt 8800    <_ cle 8801    - cmin 8970   -ucneg 8971    / cdiv 9356   NNcn 9679   2c2 9728   NN0cn0 9897   ZZcz 9956   ZZ>=cuz 10162   RR+crp 10286   ...cfz 10713    mod cmo 10904   ^cexp 11035    || cdivides 12458    gcd cgcd 12612   Primecprime 12685
This theorem is referenced by:  lgseisenlem2  20516  lgseisenlem3  20517
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 2237  ax-sep 4081  ax-nul 4089  ax-pow 4126  ax-pr 4152  ax-un 4449  ax-cnex 8726  ax-resscn 8727  ax-1cn 8728  ax-icn 8729  ax-addcl 8730  ax-addrcl 8731  ax-mulcl 8732  ax-mulrcl 8733  ax-mulcom 8734  ax-addass 8735  ax-mulass 8736  ax-distr 8737  ax-i2m1 8738  ax-1ne0 8739  ax-1rid 8740  ax-rnegex 8741  ax-rrecex 8742  ax-cnre 8743  ax-pre-lttri 8744  ax-pre-lttrn 8745  ax-pre-ltadd 8746  ax-pre-mulgt0 8747  ax-pre-sup 8748
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 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-nel 2422  df-ral 2520  df-rex 2521  df-reu 2522  df-rab 2523  df-v 2742  df-sbc 2936  df-csb 3024  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-pss 3110  df-nul 3398  df-if 3507  df-pw 3568  df-sn 3587  df-pr 3588  df-tp 3589  df-op 3590  df-uni 3769  df-int 3804  df-iun 3848  df-br 3964  df-opab 4018  df-mpt 4019  df-tr 4054  df-eprel 4242  df-id 4246  df-po 4251  df-so 4252  df-fr 4289  df-we 4291  df-ord 4332  df-on 4333  df-lim 4334  df-suc 4335  df-om 4594  df-xp 4640  df-rel 4641  df-cnv 4642  df-co 4643  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fun 4648  df-fn 4649  df-f 4650  df-f1 4651  df-fo 4652  df-f1o 4653  df-fv 4654  df-ov 5760  df-oprab 5761  df-mpt2 5762  df-1st 6021  df-2nd 6022  df-iota 6190  df-riota 6237  df-recs 6321  df-rdg 6356  df-1o 6412  df-2o 6413  df-oadd 6416  df-er 6593  df-en 6797  df-dom 6798  df-sdom 6799  df-fin 6800  df-sup 7127  df-pnf 8802  df-mnf 8803  df-xr 8804  df-ltxr 8805  df-le 8806  df-sub 8972  df-neg 8973  df-div 9357  df-n 9680  df-2 9737  df-3 9738  df-n0 9898  df-z 9957  df-uz 10163  df-rp 10287  df-fz 10714  df-fl 10856  df-mod 10905  df-seq 10978  df-exp 11036  df-cj 11514  df-re 11515  df-im 11516  df-sqr 11650  df-abs 11651  df-divides 12459  df-gcd 12613  df-prime 12686
  Copyright terms: Public domain W3C validator