ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lgsval2lem Unicode version

Theorem lgsval2lem 13670
Description: Lemma for lgsval2 13676. (Contributed by Mario Carneiro, 4-Feb-2015.)
Hypothesis
Ref Expression
lgsval.1  |-  F  =  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( if ( n  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( n  -  1 )  /  2 ) )  +  1 )  mod  n )  -  1 ) ) ^ (
n  pCnt  N )
) ,  1 ) )
Assertion
Ref Expression
lgsval2lem  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( A  /L
N )  =  if ( N  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( N  -  1 )  /  2 ) )  +  1 )  mod  N )  - 
1 ) ) )
Distinct variable groups:    A, n    n, N
Allowed substitution hint:    F( n)

Proof of Theorem lgsval2lem
Dummy variables  x  y  k  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prmz 12058 . . 3  |-  ( N  e.  Prime  ->  N  e.  ZZ )
2 lgsval.1 . . . 4  |-  F  =  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( if ( n  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( n  -  1 )  /  2 ) )  +  1 )  mod  n )  -  1 ) ) ^ (
n  pCnt  N )
) ,  1 ) )
32lgsval 13664 . . 3  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( A  /L
N )  =  if ( N  =  0 ,  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) ,  ( if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  x.  (  seq 1 (  x.  ,  F ) `  ( abs `  N ) ) ) ) )
41, 3sylan2 284 . 2  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( A  /L
N )  =  if ( N  =  0 ,  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) ,  ( if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  x.  (  seq 1 (  x.  ,  F ) `  ( abs `  N ) ) ) ) )
5 prmnn 12057 . . . . . 6  |-  ( N  e.  Prime  ->  N  e.  NN )
65adantl 275 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  NN )
76nnne0d 8916 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  =/=  0 )
87neneqd 2361 . . 3  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  -.  N  =  0
)
98iffalsed 3535 . 2  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  if ( N  =  0 ,  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) ,  ( if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  x.  (  seq 1 (  x.  ,  F ) `  ( abs `  N ) ) ) )  =  ( if ( ( N  <  0  /\  A  <  0 ) ,  -u
1 ,  1 )  x.  (  seq 1
(  x.  ,  F
) `  ( abs `  N ) ) ) )
106nnnn0d 9181 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  NN0 )
1110nn0ge0d 9184 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
0  <_  N )
12 0re 7913 . . . . . . . 8  |-  0  e.  RR
136nnred 8884 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  RR )
14 lenlt 7988 . . . . . . . 8  |-  ( ( 0  e.  RR  /\  N  e.  RR )  ->  ( 0  <_  N  <->  -.  N  <  0 ) )
1512, 13, 14sylancr 412 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( 0  <_  N  <->  -.  N  <  0 ) )
1611, 15mpbid 146 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  -.  N  <  0
)
1716intnanrd 927 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  -.  ( N  <  0  /\  A  <  0
) )
1817iffalsed 3535 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  if ( ( N  <  0  /\  A  <  0 ) ,  -u
1 ,  1 )  =  1 )
1913, 11absidd 11124 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( abs `  N
)  =  N )
2019fveq2d 5498 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  ( abs `  N ) )  =  (  seq 1 (  x.  ,  F ) `  N
) )
21 1zzd 9232 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
1  e.  ZZ )
22 prmuz2 12078 . . . . . . . . 9  |-  ( N  e.  Prime  ->  N  e.  ( ZZ>= `  2 )
)
2322adantl 275 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  ( ZZ>= ` 
2 ) )
24 df-2 8930 . . . . . . . . 9  |-  2  =  ( 1  +  1 )
2524fveq2i 5497 . . . . . . . 8  |-  ( ZZ>= ` 
2 )  =  (
ZZ>= `  ( 1  +  1 ) )
2623, 25eleqtrdi 2263 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  ( ZZ>= `  ( 1  +  1 ) ) )
27 simpll 524 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  k  e.  ( ZZ>=
`  1 ) )  ->  A  e.  ZZ )
281ad2antlr 486 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  k  e.  ( ZZ>=
`  1 ) )  ->  N  e.  ZZ )
297adantr 274 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  k  e.  ( ZZ>=
`  1 ) )  ->  N  =/=  0
)
302lgsfcl 13668 . . . . . . . . 9  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  F : NN --> ZZ )
3127, 28, 29, 30syl3anc 1233 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  k  e.  ( ZZ>=
`  1 ) )  ->  F : NN --> ZZ )
32 elnnuz 9516 . . . . . . . . . 10  |-  ( k  e.  NN  <->  k  e.  ( ZZ>= `  1 )
)
3332biimpri 132 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  1
)  ->  k  e.  NN )
3433adantl 275 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  k  e.  ( ZZ>=
`  1 ) )  ->  k  e.  NN )
3531, 34ffvelrnd 5630 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  k  e.  ( ZZ>=
`  1 ) )  ->  ( F `  k )  e.  ZZ )
36 zmulcl 9258 . . . . . . . 8  |-  ( ( k  e.  ZZ  /\  v  e.  ZZ )  ->  ( k  x.  v
)  e.  ZZ )
3736adantl 275 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  ( k  e.  ZZ  /\  v  e.  ZZ ) )  ->  ( k  x.  v )  e.  ZZ )
3821, 26, 35, 37seq3m1 10417 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  N )  =  ( (  seq 1 (  x.  ,  F ) `
 ( N  - 
1 ) )  x.  ( F `  N
) ) )
39 1t1e1 9023 . . . . . . . . 9  |-  ( 1  x.  1 )  =  1
4039a1i 9 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( 1  x.  1 )  =  1 )
41 uz2m1nn 9557 . . . . . . . . . 10  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( N  -  1 )  e.  NN )
4223, 41syl 14 . . . . . . . . 9  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( N  -  1 )  e.  NN )
43 nnuz 9515 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
4442, 43eleqtrdi 2263 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( N  -  1 )  e.  ( ZZ>= ` 
1 ) )
45 simpll 524 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  (
1 ... ( N  - 
1 ) ) )  ->  A  e.  ZZ )
466adantr 274 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  (
1 ... ( N  - 
1 ) ) )  ->  N  e.  NN )
47 elfznn 10003 . . . . . . . . . . 11  |-  ( x  e.  ( 1 ... ( N  -  1 ) )  ->  x  e.  NN )
4847adantl 275 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  (
1 ... ( N  - 
1 ) ) )  ->  x  e.  NN )
492lgsfvalg 13665 . . . . . . . . . 10  |-  ( ( A  e.  ZZ  /\  N  e.  NN  /\  x  e.  NN )  ->  ( F `  x )  =  if ( x  e. 
Prime ,  ( if ( x  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  -  1 ) ) ^ (
x  pCnt  N )
) ,  1 ) )
5045, 46, 48, 49syl3anc 1233 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  (
1 ... ( N  - 
1 ) ) )  ->  ( F `  x )  =  if ( x  e.  Prime ,  ( if ( x  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  -  1 ) ) ^ (
x  pCnt  N )
) ,  1 ) )
51 elfzelz 9974 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  N  e.  ZZ )
5251zred 9327 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  N  e.  RR )
5352ltm1d 8841 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  ( N  -  1 )  <  N )
54 peano2rem 8179 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  RR  ->  ( N  -  1 )  e.  RR )
5552, 54syl 14 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  ( N  -  1 )  e.  RR )
56 elfzle2 9977 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  N  <_  ( N  -  1 ) )
5752, 55, 56lensymd 8034 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  -.  ( N  -  1
)  <  N )
5853, 57pm2.65i 634 . . . . . . . . . . . . . . . . 17  |-  -.  N  e.  ( 1 ... ( N  -  1 ) )
59 eleq1 2233 . . . . . . . . . . . . . . . . 17  |-  ( x  =  N  ->  (
x  e.  ( 1 ... ( N  - 
1 ) )  <->  N  e.  ( 1 ... ( N  -  1 ) ) ) )
6058, 59mtbiri 670 . . . . . . . . . . . . . . . 16  |-  ( x  =  N  ->  -.  x  e.  ( 1 ... ( N  - 
1 ) ) )
6160con2i 622 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 ... ( N  -  1 ) )  ->  -.  x  =  N )
6261ad2antlr 486 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  -.  x  =  N )
63 prmuz2 12078 . . . . . . . . . . . . . . 15  |-  ( x  e.  Prime  ->  x  e.  ( ZZ>= `  2 )
)
64 simpllr 529 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  N  e.  Prime )
65 dvdsprm 12084 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  N  e.  Prime )  ->  (
x  ||  N  <->  x  =  N ) )
6663, 64, 65syl2an2 589 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  (
x  ||  N  <->  x  =  N ) )
6762, 66mtbird 668 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  -.  x  ||  N )
68 simpr 109 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  x  e.  Prime )
696ad2antrr 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  N  e.  NN )
70 pceq0 12268 . . . . . . . . . . . . . 14  |-  ( ( x  e.  Prime  /\  N  e.  NN )  ->  (
( x  pCnt  N
)  =  0  <->  -.  x  ||  N ) )
7168, 69, 70syl2anc 409 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  (
( x  pCnt  N
)  =  0  <->  -.  x  ||  N ) )
7267, 71mpbird 166 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  (
x  pCnt  N )  =  0 )
7372oveq2d 5867 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  ( if ( x  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( x  -  1 )  /  2 ) )  +  1 )  mod  x )  - 
1 ) ) ^
( x  pCnt  N
) )  =  ( if ( x  =  2 ,  if ( 2  ||  A , 
0 ,  if ( ( A  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
) ) ,  ( ( ( ( A ^ ( ( x  -  1 )  / 
2 ) )  +  1 )  mod  x
)  -  1 ) ) ^ 0 ) )
74 0zd 9217 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ZZ  ->  0  e.  ZZ )
75 1zzd 9232 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  ZZ  ->  1  e.  ZZ )
76 neg1z 9237 . . . . . . . . . . . . . . . . . . 19  |-  -u 1  e.  ZZ
7776a1i 9 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  ZZ  ->  -u 1  e.  ZZ )
78 id 19 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A  e.  ZZ  ->  A  e.  ZZ )
79 8nn 9038 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  8  e.  NN
8079a1i 9 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A  e.  ZZ  ->  8  e.  NN )
8178, 80zmodcld 10294 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A  e.  ZZ  ->  ( A  mod  8 )  e. 
NN0 )
8281nn0zd 9325 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A  e.  ZZ  ->  ( A  mod  8 )  e.  ZZ )
83 zdceq 9280 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  mod  8
)  e.  ZZ  /\  1  e.  ZZ )  -> DECID  ( A  mod  8 )  =  1 )
8482, 75, 83syl2anc 409 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  ZZ  -> DECID  ( A  mod  8
)  =  1 )
85 7nn 9037 . . . . . . . . . . . . . . . . . . . . . 22  |-  7  e.  NN
8685nnzi 9226 . . . . . . . . . . . . . . . . . . . . 21  |-  7  e.  ZZ
87 zdceq 9280 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  mod  8
)  e.  ZZ  /\  7  e.  ZZ )  -> DECID  ( A  mod  8 )  =  7 )
8882, 86, 87sylancl 411 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  ZZ  -> DECID  ( A  mod  8
)  =  7 )
89 dcor 930 . . . . . . . . . . . . . . . . . . . 20  |-  (DECID  ( A  mod  8 )  =  1  ->  (DECID  ( A  mod  8 )  =  7  -> DECID 
( ( A  mod  8 )  =  1  \/  ( A  mod  8 )  =  7 ) ) )
9084, 88, 89sylc 62 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  ZZ  -> DECID  ( ( A  mod  8 )  =  1  \/  ( A  mod  8 )  =  7 ) )
91 elprg 3601 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  mod  8 )  e.  NN0  ->  ( ( A  mod  8 )  e.  { 1 ,  7 }  <->  ( ( A  mod  8 )  =  1  \/  ( A  mod  8 )  =  7 ) ) )
9281, 91syl 14 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  ZZ  ->  (
( A  mod  8
)  e.  { 1 ,  7 }  <->  ( ( A  mod  8 )  =  1  \/  ( A  mod  8 )  =  7 ) ) )
9392dcbid 833 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  ZZ  ->  (DECID  ( A  mod  8 )  e. 
{ 1 ,  7 }  <-> DECID  ( ( A  mod  8 )  =  1  \/  ( A  mod  8 )  =  7 ) ) )
9490, 93mpbird 166 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  ZZ  -> DECID  ( A  mod  8
)  e.  { 1 ,  7 } )
9575, 77, 94ifcldcd 3560 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ZZ  ->  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 )  e.  ZZ )
96 2nn 9032 . . . . . . . . . . . . . . . . . 18  |-  2  e.  NN
97 dvdsdc 11753 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  NN  /\  A  e.  ZZ )  -> DECID  2 
||  A )
9896, 97mpan 422 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ZZ  -> DECID  2  ||  A )
9974, 95, 98ifcldcd 3560 . . . . . . . . . . . . . . . 16  |-  ( A  e.  ZZ  ->  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) )  e.  ZZ )
10099ad3antrrr 489 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  x  =  2 )  ->  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) )  e.  ZZ )
101 simpl 108 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  A  e.  ZZ )
102101ad2antrr 485 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  A  e.  ZZ )
103 simplr 525 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  x  e.  Prime )
104 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  -.  x  = 
2 )
105104neqned 2347 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  x  =/=  2
)
106 eldifsn 3708 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( Prime  \  {
2 } )  <->  ( x  e.  Prime  /\  x  =/=  2 ) )
107103, 105, 106sylanbrc 415 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  x  e.  ( Prime  \  { 2 } ) )
108 oddprm 12206 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( Prime  \  {
2 } )  -> 
( ( x  - 
1 )  /  2
)  e.  NN )
109107, 108syl 14 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( x  -  1 )  / 
2 )  e.  NN )
110109nnnn0d 9181 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( x  -  1 )  / 
2 )  e.  NN0 )
111 zexpcl 10484 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  ZZ  /\  ( ( x  - 
1 )  /  2
)  e.  NN0 )  ->  ( A ^ (
( x  -  1 )  /  2 ) )  e.  ZZ )
112102, 110, 111syl2anc 409 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( A ^
( ( x  - 
1 )  /  2
) )  e.  ZZ )
113112peano2zd 9330 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( A ^ ( ( x  -  1 )  / 
2 ) )  +  1 )  e.  ZZ )
114 prmnn 12057 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  Prime  ->  x  e.  NN )
115114ad2antlr 486 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  x  e.  NN )
116113, 115zmodcld 10294 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  e.  NN0 )
117116nn0zd 9325 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  e.  ZZ )
118 peano2zm 9243 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A ^
( ( x  - 
1 )  /  2
) )  +  1 )  mod  x )  e.  ZZ  ->  (
( ( ( A ^ ( ( x  -  1 )  / 
2 ) )  +  1 )  mod  x
)  -  1 )  e.  ZZ )
119117, 118syl 14 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( ( ( A ^ (
( x  -  1 )  /  2 ) )  +  1 )  mod  x )  - 
1 )  e.  ZZ )
120 prmz 12058 . . . . . . . . . . . . . . . 16  |-  ( x  e.  Prime  ->  x  e.  ZZ )
121 2z 9233 . . . . . . . . . . . . . . . . 17  |-  2  e.  ZZ
122121a1i 9 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  Prime )  ->  2  e.  ZZ )
123 zdceq 9280 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ZZ  /\  2  e.  ZZ )  -> DECID  x  =  2 )
124120, 122, 123syl2an2 589 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  Prime )  -> DECID 
x  =  2 )
125100, 119, 124ifcldadc 3554 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  Prime )  ->  if ( x  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  -  1 ) )  e.  ZZ )
126125zcnd 9328 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  Prime )  ->  if ( x  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  -  1 ) )  e.  CC )
127126adantlr 474 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  if ( x  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  -  1 ) )  e.  CC )
128127exp0d 10596 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  ( if ( x  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( x  -  1 )  /  2 ) )  +  1 )  mod  x )  - 
1 ) ) ^
0 )  =  1 )
12973, 128eqtrd 2203 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  ( if ( x  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( x  -  1 )  /  2 ) )  +  1 )  mod  x )  - 
1 ) ) ^
( x  pCnt  N
) )  =  1 )
130 prmdc 12077 . . . . . . . . . . 11  |-  ( x  e.  NN  -> DECID  x  e.  Prime )
13148, 130syl 14 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  (
1 ... ( N  - 
1 ) ) )  -> DECID 
x  e.  Prime )
132129, 131ifeq1dadc 3555 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  (
1 ... ( N  - 
1 ) ) )  ->  if ( x  e.  Prime ,  ( if ( x  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( x  -  1 )  /  2 ) )  +  1 )  mod  x )  - 
1 ) ) ^
( x  pCnt  N
) ) ,  1 )  =  if ( x  e.  Prime ,  1 ,  1 ) )
133 ifiddc 3558 . . . . . . . . . 10  |-  (DECID  x  e. 
Prime  ->  if ( x  e.  Prime ,  1 ,  1 )  =  1 )
134131, 133syl 14 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  (
1 ... ( N  - 
1 ) ) )  ->  if ( x  e.  Prime ,  1 ,  1 )  =  1 )
13550, 132, 1343eqtrd 2207 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  (
1 ... ( N  - 
1 ) ) )  ->  ( F `  x )  =  1 )
136 simpll 524 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  ( ZZ>=
`  1 ) )  ->  A  e.  ZZ )
1371ad2antlr 486 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  ( ZZ>=
`  1 ) )  ->  N  e.  ZZ )
1387adantr 274 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  ( ZZ>=
`  1 ) )  ->  N  =/=  0
)
139136, 137, 138, 30syl3anc 1233 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  ( ZZ>=
`  1 ) )  ->  F : NN --> ZZ )
140 elnnuz 9516 . . . . . . . . . . 11  |-  ( x  e.  NN  <->  x  e.  ( ZZ>= `  1 )
)
141140biimpri 132 . . . . . . . . . 10  |-  ( x  e.  ( ZZ>= `  1
)  ->  x  e.  NN )
142141adantl 275 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  ( ZZ>=
`  1 ) )  ->  x  e.  NN )
143139, 142ffvelrnd 5630 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  ( ZZ>=
`  1 ) )  ->  ( F `  x )  e.  ZZ )
144 zmulcl 9258 . . . . . . . . 9  |-  ( ( x  e.  ZZ  /\  y  e.  ZZ )  ->  ( x  x.  y
)  e.  ZZ )
145144adantl 275 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  ( x  e.  ZZ  /\  y  e.  ZZ ) )  ->  ( x  x.  y )  e.  ZZ )
14640, 44, 135, 21, 143, 145seq3id3 10456 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  ( N  -  1
) )  =  1 )
147146oveq1d 5866 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( (  seq 1
(  x.  ,  F
) `  ( N  -  1 ) )  x.  ( F `  N ) )  =  ( 1  x.  ( F `  N )
) )
1481adantl 275 . . . . . . . . . 10  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  ZZ )
149101, 148, 7, 30syl3anc 1233 . . . . . . . . 9  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  F : NN --> ZZ )
150149, 6ffvelrnd 5630 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( F `  N
)  e.  ZZ )
151150zcnd 9328 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( F `  N
)  e.  CC )
152151mulid2d 7931 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( 1  x.  ( F `  N )
)  =  ( F `
 N ) )
15338, 147, 1523eqtrd 2207 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  N )  =  ( F `  N ) )
15420, 153eqtrd 2203 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  ( abs `  N ) )  =  ( F `
 N ) )
15518, 154oveq12d 5869 . . 3  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  x.  (  seq 1 (  x.  ,  F ) `  ( abs `  N ) ) )  =  ( 1  x.  ( F `  N ) ) )
1562lgsfvalg 13665 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  NN  /\  N  e.  NN )  ->  ( F `  N )  =  if ( N  e. 
Prime ,  ( if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) ^ ( N  pCnt  N ) ) ,  1 ) )
157101, 6, 6, 156syl3anc 1233 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( F `  N
)  =  if ( N  e.  Prime ,  ( if ( N  =  2 ,  if ( 2  ||  A , 
0 ,  if ( ( A  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  / 
2 ) )  +  1 )  mod  N
)  -  1 ) ) ^ ( N 
pCnt  N ) ) ,  1 ) )
158 iftrue 3530 . . . . 5  |-  ( N  e.  Prime  ->  if ( N  e.  Prime ,  ( if ( N  =  2 ,  if ( 2  ||  A , 
0 ,  if ( ( A  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  / 
2 ) )  +  1 )  mod  N
)  -  1 ) ) ^ ( N 
pCnt  N ) ) ,  1 )  =  ( if ( N  =  2 ,  if ( 2  ||  A , 
0 ,  if ( ( A  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  / 
2 ) )  +  1 )  mod  N
)  -  1 ) ) ^ ( N 
pCnt  N ) ) )
159158adantl 275 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  if ( N  e.  Prime ,  ( if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) ^ ( N  pCnt  N ) ) ,  1 )  =  ( if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) ^ ( N  pCnt  N ) ) )
1606nncnd 8885 . . . . . . . . 9  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  CC )
161160exp1d 10597 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( N ^ 1 )  =  N )
162161oveq2d 5867 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( N  pCnt  ( N ^ 1 ) )  =  ( N  pCnt  N ) )
163 simpr 109 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  Prime )
164 1z 9231 . . . . . . . 8  |-  1  e.  ZZ
165 pcid 12270 . . . . . . . 8  |-  ( ( N  e.  Prime  /\  1  e.  ZZ )  ->  ( N  pCnt  ( N ^
1 ) )  =  1 )
166163, 164, 165sylancl 411 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( N  pCnt  ( N ^ 1 ) )  =  1 )
167162, 166eqtr3d 2205 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( N  pCnt  N
)  =  1 )
168167oveq2d 5867 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) ^ ( N  pCnt  N ) )  =  ( if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) ^ 1 ) )
169 eqeq1 2177 . . . . . . . . 9  |-  ( x  =  N  ->  (
x  =  2  <->  N  =  2 ) )
170 oveq1 5858 . . . . . . . . . . . . . 14  |-  ( x  =  N  ->  (
x  -  1 )  =  ( N  - 
1 ) )
171170oveq1d 5866 . . . . . . . . . . . . 13  |-  ( x  =  N  ->  (
( x  -  1 )  /  2 )  =  ( ( N  -  1 )  / 
2 ) )
172171oveq2d 5867 . . . . . . . . . . . 12  |-  ( x  =  N  ->  ( A ^ ( ( x  -  1 )  / 
2 ) )  =  ( A ^ (
( N  -  1 )  /  2 ) ) )
173172oveq1d 5866 . . . . . . . . . . 11  |-  ( x  =  N  ->  (
( A ^ (
( x  -  1 )  /  2 ) )  +  1 )  =  ( ( A ^ ( ( N  -  1 )  / 
2 ) )  +  1 ) )
174 id 19 . . . . . . . . . . 11  |-  ( x  =  N  ->  x  =  N )
175173, 174oveq12d 5869 . . . . . . . . . 10  |-  ( x  =  N  ->  (
( ( A ^
( ( x  - 
1 )  /  2
) )  +  1 )  mod  x )  =  ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N ) )
176175oveq1d 5866 . . . . . . . . 9  |-  ( x  =  N  ->  (
( ( ( A ^ ( ( x  -  1 )  / 
2 ) )  +  1 )  mod  x
)  -  1 )  =  ( ( ( ( A ^ (
( N  -  1 )  /  2 ) )  +  1 )  mod  N )  - 
1 ) )
177169, 176ifbieq2d 3549 . . . . . . . 8  |-  ( x  =  N  ->  if ( x  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  -  1 ) )  =  if ( N  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( N  -  1 )  /  2 ) )  +  1 )  mod  N )  - 
1 ) ) )
178177eleq1d 2239 . . . . . . 7  |-  ( x  =  N  ->  ( if ( x  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( x  -  1 )  /  2 ) )  +  1 )  mod  x )  - 
1 ) )  e.  CC  <->  if ( N  =  2 ,  if ( 2  ||  A , 
0 ,  if ( ( A  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  / 
2 ) )  +  1 )  mod  N
)  -  1 ) )  e.  CC ) )
179126ralrimiva 2543 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  A. x  e.  Prime  if ( x  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( x  -  1 )  /  2 ) )  +  1 )  mod  x )  - 
1 ) )  e.  CC )
180178, 179, 163rspcdva 2839 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  if ( N  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( N  -  1 )  /  2 ) )  +  1 )  mod  N )  - 
1 ) )  e.  CC )
181180exp1d 10597 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) ^ 1 )  =  if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) )
182168, 181eqtrd 2203 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) ^ ( N  pCnt  N ) )  =  if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) )
183157, 159, 1823eqtrd 2207 . . 3  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( F `  N
)  =  if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) )
184155, 152, 1833eqtrd 2207 . 2  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  x.  (  seq 1 (  x.  ,  F ) `  ( abs `  N ) ) )  =  if ( N  =  2 ,  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N )  -  1 ) ) )
1854, 9, 1843eqtrd 2207 1  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( A  /L
N )  =  if ( N  =  2 ,  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) ,  ( ( ( ( A ^ (
( N  -  1 )  /  2 ) )  +  1 )  mod  N )  - 
1 ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 703  DECID wdc 829    = wceq 1348    e. wcel 2141    =/= wne 2340    \ cdif 3118   ifcif 3525   {csn 3581   {cpr 3582   class class class wbr 3987    |-> cmpt 4048   -->wf 5192   ` cfv 5196  (class class class)co 5851   CCcc 7765   RRcr 7766   0cc0 7767   1c1 7768    + caddc 7770    x. cmul 7772    < clt 7947    <_ cle 7948    - cmin 8083   -ucneg 8084    / cdiv 8582   NNcn 8871   2c2 8922   7c7 8927   8c8 8928   NN0cn0 9128   ZZcz 9205   ZZ>=cuz 9480   ...cfz 9958    mod cmo 10271    seqcseq 10394   ^cexp 10468   abscabs 10954    || cdvds 11742   Primecprime 12054    pCnt cpc 12231    /Lclgs 13657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570  ax-cnex 7858  ax-resscn 7859  ax-1cn 7860  ax-1re 7861  ax-icn 7862  ax-addcl 7863  ax-addrcl 7864  ax-mulcl 7865  ax-mulrcl 7866  ax-addcom 7867  ax-mulcom 7868  ax-addass 7869  ax-mulass 7870  ax-distr 7871  ax-i2m1 7872  ax-0lt1 7873  ax-1rid 7874  ax-0id 7875  ax-rnegex 7876  ax-precex 7877  ax-cnre 7878  ax-pre-ltirr 7879  ax-pre-ltwlin 7880  ax-pre-lttrn 7881  ax-pre-apti 7882  ax-pre-ltadd 7883  ax-pre-mulgt0 7884  ax-pre-mulext 7885  ax-arch 7886  ax-caucvg 7887
This theorem depends on definitions:  df-bi 116  df-stab 826  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-xor 1371  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-po 4279  df-iso 4280  df-iord 4349  df-on 4351  df-ilim 4352  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-isom 5205  df-riota 5807  df-ov 5854  df-oprab 5855  df-mpo 5856  df-1st 6117  df-2nd 6118  df-recs 6282  df-irdg 6347  df-frec 6368  df-1o 6393  df-2o 6394  df-oadd 6397  df-er 6511  df-en 6717  df-dom 6718  df-fin 6719  df-sup 6959  df-inf 6960  df-pnf 7949  df-mnf 7950  df-xr 7951  df-ltxr 7952  df-le 7953  df-sub 8085  df-neg 8086  df-reap 8487  df-ap 8494  df-div 8583  df-inn 8872  df-2 8930  df-3 8931  df-4 8932  df-5 8933  df-6 8934  df-7 8935  df-8 8936  df-n0 9129  df-z 9206  df-uz 9481  df-q 9572  df-rp 9604  df-fz 9959  df-fzo 10092  df-fl 10219  df-mod 10272  df-seqfrec 10395  df-exp 10469  df-ihash 10703  df-cj 10799  df-re 10800  df-im 10801  df-rsqrt 10955  df-abs 10956  df-clim 11235  df-proddc 11507  df-dvds 11743  df-gcd 11891  df-prm 12055  df-phi 12158  df-pc 12232  df-lgs 13658
This theorem is referenced by:  lgsval4lem  13671  lgsval2  13676
  Copyright terms: Public domain W3C validator