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

Theorem lgsval2lem 13790
Description: Lemma for lgsval2 13796. (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 12069 . . 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 13784 . . 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 12068 . . . . . 6  |-  ( N  e.  Prime  ->  N  e.  NN )
65adantl 275 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  NN )
76nnne0d 8927 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  =/=  0 )
87neneqd 2362 . . 3  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  -.  N  =  0
)
98iffalsed 3537 . 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 9192 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  NN0 )
1110nn0ge0d 9195 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
0  <_  N )
12 0re 7924 . . . . . . . 8  |-  0  e.  RR
136nnred 8895 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  RR )
14 lenlt 7999 . . . . . . . 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 928 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  -.  ( N  <  0  /\  A  <  0
) )
1817iffalsed 3537 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  if ( ( N  <  0  /\  A  <  0 ) ,  -u
1 ,  1 )  =  1 )
1913, 11absidd 11135 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( abs `  N
)  =  N )
2019fveq2d 5503 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  ( abs `  N ) )  =  (  seq 1 (  x.  ,  F ) `  N
) )
21 1zzd 9243 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
1  e.  ZZ )
22 prmuz2 12089 . . . . . . . . 9  |-  ( N  e.  Prime  ->  N  e.  ( ZZ>= `  2 )
)
2322adantl 275 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  ( ZZ>= ` 
2 ) )
24 df-2 8941 . . . . . . . . 9  |-  2  =  ( 1  +  1 )
2524fveq2i 5502 . . . . . . . 8  |-  ( ZZ>= ` 
2 )  =  (
ZZ>= `  ( 1  +  1 ) )
2623, 25eleqtrdi 2264 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  ( ZZ>= `  ( 1  +  1 ) ) )
27 simpll 525 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  k  e.  ( ZZ>=
`  1 ) )  ->  A  e.  ZZ )
281ad2antlr 487 . . . . . . . . 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 13788 . . . . . . . . 9  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  F : NN --> ZZ )
3127, 28, 29, 30syl3anc 1234 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  k  e.  ( ZZ>=
`  1 ) )  ->  F : NN --> ZZ )
32 elnnuz 9527 . . . . . . . . . 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 5636 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  k  e.  ( ZZ>=
`  1 ) )  ->  ( F `  k )  e.  ZZ )
36 zmulcl 9269 . . . . . . . 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 10428 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  N )  =  ( (  seq 1 (  x.  ,  F ) `
 ( N  - 
1 ) )  x.  ( F `  N
) ) )
39 1t1e1 9034 . . . . . . . . 9  |-  ( 1  x.  1 )  =  1
4039a1i 9 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( 1  x.  1 )  =  1 )
41 uz2m1nn 9568 . . . . . . . . . 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 9526 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
4442, 43eleqtrdi 2264 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( N  -  1 )  e.  ( ZZ>= ` 
1 ) )
45 simpll 525 . . . . . . . . . 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 10014 . . . . . . . . . . 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 13785 . . . . . . . . . 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 1234 . . . . . . . . 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 9985 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  N  e.  ZZ )
5251zred 9338 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  N  e.  RR )
5352ltm1d 8852 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  ( N  -  1 )  <  N )
54 peano2rem 8190 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  RR  ->  ( N  -  1 )  e.  RR )
5552, 54syl 14 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  ( N  -  1 )  e.  RR )
56 elfzle2 9988 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  N  <_  ( N  -  1 ) )
5752, 55, 56lensymd 8045 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  -.  ( N  -  1
)  <  N )
5853, 57pm2.65i 635 . . . . . . . . . . . . . . . . 17  |-  -.  N  e.  ( 1 ... ( N  -  1 ) )
59 eleq1 2234 . . . . . . . . . . . . . . . . 17  |-  ( x  =  N  ->  (
x  e.  ( 1 ... ( N  - 
1 ) )  <->  N  e.  ( 1 ... ( N  -  1 ) ) ) )
6058, 59mtbiri 671 . . . . . . . . . . . . . . . 16  |-  ( x  =  N  ->  -.  x  e.  ( 1 ... ( N  - 
1 ) ) )
6160con2i 623 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 ... ( N  -  1 ) )  ->  -.  x  =  N )
6261ad2antlr 487 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  -.  x  =  N )
63 prmuz2 12089 . . . . . . . . . . . . . . 15  |-  ( x  e.  Prime  ->  x  e.  ( ZZ>= `  2 )
)
64 simpllr 530 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  N  e.  Prime )
65 dvdsprm 12095 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( ZZ>= ` 
2 )  /\  N  e.  Prime )  ->  (
x  ||  N  <->  x  =  N ) )
6663, 64, 65syl2an2 590 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  (
x  ||  N  <->  x  =  N ) )
6762, 66mtbird 669 . . . . . . . . . . . . 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 486 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  ( 1 ... ( N  -  1 ) ) )  /\  x  e.  Prime )  ->  N  e.  NN )
70 pceq0 12279 . . . . . . . . . . . . . 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 5873 . . . . . . . . . . 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 9228 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ZZ  ->  0  e.  ZZ )
75 1zzd 9243 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  ZZ  ->  1  e.  ZZ )
76 neg1z 9248 . . . . . . . . . . . . . . . . . . 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 9049 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  8  e.  NN
8079a1i 9 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A  e.  ZZ  ->  8  e.  NN )
8178, 80zmodcld 10305 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A  e.  ZZ  ->  ( A  mod  8 )  e. 
NN0 )
8281nn0zd 9336 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A  e.  ZZ  ->  ( A  mod  8 )  e.  ZZ )
83 zdceq 9291 . . . . . . . . . . . . . . . . . . . . 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 9048 . . . . . . . . . . . . . . . . . . . . . 22  |-  7  e.  NN
8685nnzi 9237 . . . . . . . . . . . . . . . . . . . . 21  |-  7  e.  ZZ
87 zdceq 9291 . . . . . . . . . . . . . . . . . . . . 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 931 . . . . . . . . . . . . . . . . . . . 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 3604 . . . . . . . . . . . . . . . . . . . . 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 834 . . . . . . . . . . . . . . . . . . 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 3562 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ZZ  ->  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 )  e.  ZZ )
96 2nn 9043 . . . . . . . . . . . . . . . . . 18  |-  2  e.  NN
97 dvdsdc 11764 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  NN  /\  A  e.  ZZ )  -> DECID  2 
||  A )
9896, 97mpan 422 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ZZ  -> DECID  2  ||  A )
9974, 95, 98ifcldcd 3562 . . . . . . . . . . . . . . . 16  |-  ( A  e.  ZZ  ->  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) )  e.  ZZ )
10099ad3antrrr 490 . . . . . . . . . . . . . . 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 486 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  A  e.  ZZ )
103 simplr 526 . . . . . . . . . . . . . . . . . . . . . . 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 2348 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  x  =/=  2
)
106 eldifsn 3711 . . . . . . . . . . . . . . . . . . . . . . 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 12217 . . . . . . . . . . . . . . . . . . . . . 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 9192 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( x  -  1 )  / 
2 )  e.  NN0 )
111 zexpcl 10495 . . . . . . . . . . . . . . . . . . . 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 9341 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( A ^ ( ( x  -  1 )  / 
2 ) )  +  1 )  e.  ZZ )
114 prmnn 12068 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  Prime  ->  x  e.  NN )
115114ad2antlr 487 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  x  e.  NN )
116113, 115zmodcld 10305 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  e.  NN0 )
117116nn0zd 9336 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e. 
Prime )  /\  x  e.  Prime )  /\  -.  x  =  2 )  ->  ( ( ( A ^ ( ( x  -  1 )  /  2 ) )  +  1 )  mod  x )  e.  ZZ )
118 peano2zm 9254 . . . . . . . . . . . . . . . 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 12069 . . . . . . . . . . . . . . . 16  |-  ( x  e.  Prime  ->  x  e.  ZZ )
121 2z 9244 . . . . . . . . . . . . . . . . 17  |-  2  e.  ZZ
122121a1i 9 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  Prime )  ->  2  e.  ZZ )
123 zdceq 9291 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ZZ  /\  2  e.  ZZ )  -> DECID  x  =  2 )
124120, 122, 123syl2an2 590 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  Prime )  -> DECID 
x  =  2 )
125100, 119, 124ifcldadc 3556 . . . . . . . . . . . . . 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 9339 . . . . . . . . . . . . 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 475 . . . . . . . . . . . 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 10607 . . . . . . . . . . 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 2204 . . . . . . . . . 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 12088 . . . . . . . . . . 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 3557 . . . . . . . . 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 3560 . . . . . . . . . 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 2208 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  (
1 ... ( N  - 
1 ) ) )  ->  ( F `  x )  =  1 )
136 simpll 525 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  ( ZZ>=
`  1 ) )  ->  A  e.  ZZ )
1371ad2antlr 487 . . . . . . . . . 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 1234 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  ( ZZ>=
`  1 ) )  ->  F : NN --> ZZ )
140 elnnuz 9527 . . . . . . . . . . 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 5636 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  Prime )  /\  x  e.  ( ZZ>=
`  1 ) )  ->  ( F `  x )  e.  ZZ )
144 zmulcl 9269 . . . . . . . . 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 10467 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  ( N  -  1
) )  =  1 )
147146oveq1d 5872 . . . . . 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 1234 . . . . . . . . 9  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  F : NN --> ZZ )
150149, 6ffvelrnd 5636 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( F `  N
)  e.  ZZ )
151150zcnd 9339 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( F `  N
)  e.  CC )
152151mulid2d 7942 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( 1  x.  ( F `  N )
)  =  ( F `
 N ) )
15338, 147, 1523eqtrd 2208 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  N )  =  ( F `  N ) )
15420, 153eqtrd 2204 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
(  seq 1 (  x.  ,  F ) `  ( abs `  N ) )  =  ( F `
 N ) )
15518, 154oveq12d 5875 . . 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 13785 . . . . 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 1234 . . . 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 3532 . . . . 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 8896 . . . . . . . . 9  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  ->  N  e.  CC )
161160exp1d 10608 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( N ^ 1 )  =  N )
162161oveq2d 5873 . . . . . . 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 9242 . . . . . . . 8  |-  1  e.  ZZ
165 pcid 12281 . . . . . . . 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 2206 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  Prime )  -> 
( N  pCnt  N
)  =  1 )
168167oveq2d 5873 . . . . 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 2178 . . . . . . . . 9  |-  ( x  =  N  ->  (
x  =  2  <->  N  =  2 ) )
170 oveq1 5864 . . . . . . . . . . . . . 14  |-  ( x  =  N  ->  (
x  -  1 )  =  ( N  - 
1 ) )
171170oveq1d 5872 . . . . . . . . . . . . 13  |-  ( x  =  N  ->  (
( x  -  1 )  /  2 )  =  ( ( N  -  1 )  / 
2 ) )
172171oveq2d 5873 . . . . . . . . . . . 12  |-  ( x  =  N  ->  ( A ^ ( ( x  -  1 )  / 
2 ) )  =  ( A ^ (
( N  -  1 )  /  2 ) ) )
173172oveq1d 5872 . . . . . . . . . . 11  |-  ( x  =  N  ->  (
( A ^ (
( x  -  1 )  /  2 ) )  +  1 )  =  ( ( A ^ ( ( N  -  1 )  / 
2 ) )  +  1 ) )
174 id 19 . . . . . . . . . . 11  |-  ( x  =  N  ->  x  =  N )
175173, 174oveq12d 5875 . . . . . . . . . 10  |-  ( x  =  N  ->  (
( ( A ^
( ( x  - 
1 )  /  2
) )  +  1 )  mod  x )  =  ( ( ( A ^ ( ( N  -  1 )  /  2 ) )  +  1 )  mod 
N ) )
176175oveq1d 5872 . . . . . . . . 9  |-  ( x  =  N  ->  (
( ( ( A ^ ( ( x  -  1 )  / 
2 ) )  +  1 )  mod  x
)  -  1 )  =  ( ( ( ( A ^ (
( N  -  1 )  /  2 ) )  +  1 )  mod  N )  - 
1 ) )
177169, 176ifbieq2d 3551 . . . . . . . 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 2240 . . . . . . 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 2544 . . . . . . 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 2840 . . . . . 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 10608 . . . . 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 2204 . . . 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 2208 . . 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 2208 . 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 2208 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 704  DECID wdc 830    = wceq 1349    e. wcel 2142    =/= wne 2341    \ cdif 3119   ifcif 3527   {csn 3584   {cpr 3585   class class class wbr 3990    |-> cmpt 4051   -->wf 5196   ` cfv 5200  (class class class)co 5857   CCcc 7776   RRcr 7777   0cc0 7778   1c1 7779    + caddc 7781    x. cmul 7783    < clt 7958    <_ cle 7959    - cmin 8094   -ucneg 8095    / cdiv 8593   NNcn 8882   2c2 8933   7c7 8938   8c8 8939   NN0cn0 9139   ZZcz 9216   ZZ>=cuz 9491   ...cfz 9969    mod cmo 10282    seqcseq 10405   ^cexp 10479   abscabs 10965    || cdvds 11753   Primecprime 12065    pCnt cpc 12242    /Lclgs 13777
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 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-coll 4105  ax-sep 4108  ax-nul 4116  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-setind 4522  ax-iinf 4573  ax-cnex 7869  ax-resscn 7870  ax-1cn 7871  ax-1re 7872  ax-icn 7873  ax-addcl 7874  ax-addrcl 7875  ax-mulcl 7876  ax-mulrcl 7877  ax-addcom 7878  ax-mulcom 7879  ax-addass 7880  ax-mulass 7881  ax-distr 7882  ax-i2m1 7883  ax-0lt1 7884  ax-1rid 7885  ax-0id 7886  ax-rnegex 7887  ax-precex 7888  ax-cnre 7889  ax-pre-ltirr 7890  ax-pre-ltwlin 7891  ax-pre-lttrn 7892  ax-pre-apti 7893  ax-pre-ltadd 7894  ax-pre-mulgt0 7895  ax-pre-mulext 7896  ax-arch 7897  ax-caucvg 7898
This theorem depends on definitions:  df-bi 116  df-stab 827  df-dc 831  df-3or 975  df-3an 976  df-tru 1352  df-fal 1355  df-xor 1372  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ne 2342  df-nel 2437  df-ral 2454  df-rex 2455  df-reu 2456  df-rmo 2457  df-rab 2458  df-v 2733  df-sbc 2957  df-csb 3051  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-nul 3416  df-if 3528  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-iun 3876  df-br 3991  df-opab 4052  df-mpt 4053  df-tr 4089  df-id 4279  df-po 4282  df-iso 4283  df-iord 4352  df-on 4354  df-ilim 4355  df-suc 4357  df-iom 4576  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-f1 5205  df-fo 5206  df-f1o 5207  df-fv 5208  df-isom 5209  df-riota 5813  df-ov 5860  df-oprab 5861  df-mpo 5862  df-1st 6123  df-2nd 6124  df-recs 6288  df-irdg 6353  df-frec 6374  df-1o 6399  df-2o 6400  df-oadd 6403  df-er 6517  df-en 6723  df-dom 6724  df-fin 6725  df-sup 6965  df-inf 6966  df-pnf 7960  df-mnf 7961  df-xr 7962  df-ltxr 7963  df-le 7964  df-sub 8096  df-neg 8097  df-reap 8498  df-ap 8505  df-div 8594  df-inn 8883  df-2 8941  df-3 8942  df-4 8943  df-5 8944  df-6 8945  df-7 8946  df-8 8947  df-n0 9140  df-z 9217  df-uz 9492  df-q 9583  df-rp 9615  df-fz 9970  df-fzo 10103  df-fl 10230  df-mod 10283  df-seqfrec 10406  df-exp 10480  df-ihash 10714  df-cj 10810  df-re 10811  df-im 10812  df-rsqrt 10966  df-abs 10967  df-clim 11246  df-proddc 11518  df-dvds 11754  df-gcd 11902  df-prm 12066  df-phi 12169  df-pc 12243  df-lgs 13778
This theorem is referenced by:  lgsval4lem  13791  lgsval2  13796
  Copyright terms: Public domain W3C validator