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

Theorem lgsne0 23480
Description: The Legendre symbol is nonzero (and hence equal to  1 or  -u 1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.)
Assertion
Ref Expression
lgsne0  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( A  /L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )

Proof of Theorem lgsne0
Dummy variables  k  n  x  y  p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iffalse 3935 . . . . . 6  |-  ( -.  ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =  0 )
21necon1ai 2674 . . . . 5  |-  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  -> 
( A ^ 2 )  =  1 )
3 iftrue 3932 . . . . . 6  |-  ( ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =  1 )
4 ax-1ne0 9564 . . . . . . 7  |-  1  =/=  0
54a1i 11 . . . . . 6  |-  ( ( A ^ 2 )  =  1  ->  1  =/=  0 )
63, 5eqnetrd 2736 . . . . 5  |-  ( ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0 )
72, 6impbii 188 . . . 4  |-  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  <->  ( A ^ 2 )  =  1 )
8 zre 10874 . . . . . . . 8  |-  ( A  e.  ZZ  ->  A  e.  RR )
98ad2antrr 725 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  A  e.  RR )
10 absresq 13114 . . . . . . 7  |-  ( A  e.  RR  ->  (
( abs `  A
) ^ 2 )  =  ( A ^
2 ) )
119, 10syl 16 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( abs `  A ) ^
2 )  =  ( A ^ 2 ) )
12 sq1 12241 . . . . . . 7  |-  ( 1 ^ 2 )  =  1
1312a1i 11 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( 1 ^ 2 )  =  1 )
1411, 13eqeq12d 2465 . . . . 5  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( (
( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( A ^ 2 )  =  1 ) )
159recnd 9625 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  A  e.  CC )
1615abscld 13246 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( abs `  A )  e.  RR )
1715absge0d 13254 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  0  <_  ( abs `  A ) )
18 1re 9598 . . . . . . 7  |-  1  e.  RR
19 0le1 10082 . . . . . . 7  |-  0  <_  1
20 sq11 12219 . . . . . . 7  |-  ( ( ( ( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) )  /\  (
1  e.  RR  /\  0  <_  1 ) )  ->  ( ( ( abs `  A ) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A
)  =  1 ) )
2118, 19, 20mpanr12 685 . . . . . 6  |-  ( ( ( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) )  ->  (
( ( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A )  =  1 ) )
2216, 17, 21syl2anc 661 . . . . 5  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( (
( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A )  =  1 ) )
2314, 22bitr3d 255 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A ^ 2 )  =  1  <->  ( abs `  A
)  =  1 ) )
247, 23syl5bb 257 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  <->  ( abs `  A )  =  1 ) )
25 oveq2 6289 . . . . 5  |-  ( N  =  0  ->  ( A  /L N )  =  ( A  /L 0 ) )
26 lgs0 23456 . . . . . 6  |-  ( A  e.  ZZ  ->  ( A  /L 0 )  =  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) )
2726adantr 465 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( A  /L 0 )  =  if ( ( A ^
2 )  =  1 ,  1 ,  0 ) )
2825, 27sylan9eqr 2506 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( A  /L N )  =  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) )
2928neeq1d 2720 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  /L N )  =/=  0  <->  if (
( A ^ 2 )  =  1 ,  1 ,  0 )  =/=  0 ) )
30 oveq2 6289 . . . . 5  |-  ( N  =  0  ->  ( A  gcd  N )  =  ( A  gcd  0
) )
31 gcdid0 14039 . . . . . 6  |-  ( A  e.  ZZ  ->  ( A  gcd  0 )  =  ( abs `  A
) )
3231adantr 465 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( A  gcd  0
)  =  ( abs `  A ) )
3330, 32sylan9eqr 2506 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( A  gcd  N )  =  ( abs `  A ) )
3433eqeq1d 2445 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  gcd  N )  =  1  <->  ( abs `  A
)  =  1 ) )
3524, 29, 343bitr4d 285 . 2  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  /L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
36 eqid 2443 . . . . . 6  |-  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L
n ) ^ (
n  pCnt  N )
) ,  1 ) )  =  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L
n ) ^ (
n  pCnt  N )
) ,  1 ) )
3736lgsval4 23463 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( A  /L N )  =  ( if ( ( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  x.  (  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L
n ) ^ (
n  pCnt  N )
) ,  1 ) ) ) `  ( abs `  N ) ) ) )
3837neeq1d 2720 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
( A  /L
N )  =/=  0  <->  ( if ( ( N  <  0  /\  A  <  0 ) ,  -u
1 ,  1 )  x.  (  seq 1
(  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) ) )  =/=  0
) )
39 neeq1 2724 . . . . . . 7  |-  ( -u
1  =  if ( ( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  -> 
( -u 1  =/=  0  <->  if ( ( N  <  0  /\  A  <  0 ) ,  -u
1 ,  1 )  =/=  0 ) )
40 neeq1 2724 . . . . . . 7  |-  ( 1  =  if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  ->  ( 1  =/=  0  <->  if (
( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  =/=  0 ) )
41 neg1ne0 10647 . . . . . . 7  |-  -u 1  =/=  0
4239, 40, 41, 4keephyp 3991 . . . . . 6  |-  if ( ( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  =/=  0
4342biantrur 506 . . . . 5  |-  ( (  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =/=  0  <->  ( if ( ( N  <  0  /\  A  <  0 ) ,  -u
1 ,  1 )  =/=  0  /\  (  seq 1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) )  =/=  0 ) )
44 neg1cn 10645 . . . . . . . 8  |-  -u 1  e.  CC
45 ax-1cn 9553 . . . . . . . 8  |-  1  e.  CC
4644, 45keepel 3994 . . . . . . 7  |-  if ( ( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  e.  CC
4746a1i 11 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  if ( ( N  <  0  /\  A  <  0 ) ,  -u
1 ,  1 )  e.  CC )
48 nnabscl 13137 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  N  =/=  0 )  -> 
( abs `  N
)  e.  NN )
49483adant1 1015 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( abs `  N )  e.  NN )
50 nnuz 11125 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
5149, 50syl6eleq 2541 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( abs `  N )  e.  ( ZZ>= `  1 )
)
5236lgsfcl3 23464 . . . . . . . . 9  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) : NN --> ZZ )
53 elfznn 11723 . . . . . . . . 9  |-  ( k  e.  ( 1 ... ( abs `  N
) )  ->  k  e.  NN )
54 ffvelrn 6014 . . . . . . . . 9  |-  ( ( ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) : NN --> ZZ  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L
n ) ^ (
n  pCnt  N )
) ,  1 ) ) `  k )  e.  ZZ )
5552, 53, 54syl2an 477 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  k  e.  ( 1 ... ( abs `  N
) ) )  -> 
( ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) `  k )  e.  ZZ )
5655zcnd 10975 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  k  e.  ( 1 ... ( abs `  N
) ) )  -> 
( ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) `  k )  e.  CC )
57 mulcl 9579 . . . . . . . 8  |-  ( ( k  e.  CC  /\  x  e.  CC )  ->  ( k  x.  x
)  e.  CC )
5857adantl 466 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( k  e.  CC  /\  x  e.  CC ) )  ->  ( k  x.  x )  e.  CC )
5951, 56, 58seqcl 12106 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (  seq 1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) )  e.  CC )
6047, 59mulne0bd 10206 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
( if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  =/=  0  /\  (  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L
n ) ^ (
n  pCnt  N )
) ,  1 ) ) ) `  ( abs `  N ) )  =/=  0 )  <->  ( if ( ( N  <  0  /\  A  <  0 ) ,  -u
1 ,  1 )  x.  (  seq 1
(  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) ) )  =/=  0
) )
6143, 60syl5rbb 258 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
( if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  x.  (  seq 1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) ) )  =/=  0  <->  (  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =/=  0
) )
62 simpr 461 . . . . . . . . . 10  |-  ( ( A  =  0  /\  N  =  0 )  ->  N  =  0 )
6362necon3ai 2671 . . . . . . . . 9  |-  ( N  =/=  0  ->  -.  ( A  =  0  /\  N  =  0
) )
64 gcdn0cl 14029 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  -.  ( A  =  0  /\  N  =  0 ) )  ->  ( A  gcd  N )  e.  NN )
6563, 64sylan2 474 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =/=  0
)  ->  ( A  gcd  N )  e.  NN )
66653impa 1192 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( A  gcd  N )  e.  NN )
67 eluz2b3 11164 . . . . . . . . 9  |-  ( ( A  gcd  N )  e.  ( ZZ>= `  2
)  <->  ( ( A  gcd  N )  e.  NN  /\  ( A  gcd  N )  =/=  1 ) )
68 exprmfct 14128 . . . . . . . . 9  |-  ( ( A  gcd  N )  e.  ( ZZ>= `  2
)  ->  E. p  e.  Prime  p  ||  ( A  gcd  N ) )
6967, 68sylbir 213 . . . . . . . 8  |-  ( ( ( A  gcd  N
)  e.  NN  /\  ( A  gcd  N )  =/=  1 )  ->  E. p  e.  Prime  p 
||  ( A  gcd  N ) )
7057adantl 466 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  ( k  e.  CC  /\  x  e.  CC ) )  ->  ( k  x.  x )  e.  CC )
7156adantlr 714 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  k  e.  ( 1 ... ( abs `  N
) ) )  -> 
( ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) `  k )  e.  CC )
72 mul02 9761 . . . . . . . . . . 11  |-  ( k  e.  CC  ->  (
0  x.  k )  =  0 )
7372adantl 466 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  k  e.  CC )  ->  ( 0  x.  k
)  =  0 )
74 mul01 9762 . . . . . . . . . . 11  |-  ( k  e.  CC  ->  (
k  x.  0 )  =  0 )
7574adantl 466 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  k  e.  CC )  ->  ( k  x.  0 )  =  0 )
76 simprr 757 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  ( A  gcd  N ) )
77 prmz 14098 . . . . . . . . . . . . . . . . 17  |-  ( p  e.  Prime  ->  p  e.  ZZ )
7877ad2antrl 727 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ZZ )
79 simpl1 1000 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  A  e.  ZZ )
80 simpl2 1001 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  N  e.  ZZ )
81 dvdsgcdb 14059 . . . . . . . . . . . . . . . 16  |-  ( ( p  e.  ZZ  /\  A  e.  ZZ  /\  N  e.  ZZ )  ->  (
( p  ||  A  /\  p  ||  N )  <-> 
p  ||  ( A  gcd  N ) ) )
8278, 79, 80, 81syl3anc 1229 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( (
p  ||  A  /\  p  ||  N )  <->  p  ||  ( A  gcd  N ) ) )
8376, 82mpbird 232 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  A  /\  p  ||  N ) )
8483simprd 463 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  N
)
85 dvdsabsb 13880 . . . . . . . . . . . . . 14  |-  ( ( p  e.  ZZ  /\  N  e.  ZZ )  ->  ( p  ||  N  <->  p 
||  ( abs `  N
) ) )
8678, 80, 85syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  N  <->  p  ||  ( abs `  N ) ) )
8784, 86mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  ( abs `  N ) )
8849adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( abs `  N )  e.  NN )
89 dvdsle 13908 . . . . . . . . . . . . 13  |-  ( ( p  e.  ZZ  /\  ( abs `  N )  e.  NN )  -> 
( p  ||  ( abs `  N )  ->  p  <_  ( abs `  N
) ) )
9078, 88, 89syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  ( abs `  N
)  ->  p  <_  ( abs `  N ) ) )
9187, 90mpd 15 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  <_  ( abs `  N ) )
92 prmnn 14097 . . . . . . . . . . . . . 14  |-  ( p  e.  Prime  ->  p  e.  NN )
9392ad2antrl 727 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  NN )
9493, 50syl6eleq 2541 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ( ZZ>= `  1 )
)
9588nnzd 10973 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( abs `  N )  e.  ZZ )
96 elfz5 11689 . . . . . . . . . . . 12  |-  ( ( p  e.  ( ZZ>= ` 
1 )  /\  ( abs `  N )  e.  ZZ )  ->  (
p  e.  ( 1 ... ( abs `  N
) )  <->  p  <_  ( abs `  N ) ) )
9794, 95, 96syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  e.  ( 1 ... ( abs `  N ) )  <-> 
p  <_  ( abs `  N ) ) )
9891, 97mpbird 232 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ( 1 ... ( abs `  N ) ) )
99 eleq1 2515 . . . . . . . . . . . . . 14  |-  ( n  =  p  ->  (
n  e.  Prime  <->  p  e.  Prime ) )
100 oveq2 6289 . . . . . . . . . . . . . . 15  |-  ( n  =  p  ->  ( A  /L n )  =  ( A  /L p ) )
101 oveq1 6288 . . . . . . . . . . . . . . 15  |-  ( n  =  p  ->  (
n  pCnt  N )  =  ( p  pCnt  N ) )
102100, 101oveq12d 6299 . . . . . . . . . . . . . 14  |-  ( n  =  p  ->  (
( A  /L
n ) ^ (
n  pCnt  N )
)  =  ( ( A  /L p ) ^ ( p 
pCnt  N ) ) )
10399, 102ifbieq1d 3949 . . . . . . . . . . . . 13  |-  ( n  =  p  ->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 )  =  if ( p  e.  Prime ,  ( ( A  /L
p ) ^ (
p  pCnt  N )
) ,  1 ) )
104 ovex 6309 . . . . . . . . . . . . . 14  |-  ( ( A  /L p ) ^ ( p 
pCnt  N ) )  e. 
_V
105 1ex 9594 . . . . . . . . . . . . . 14  |-  1  e.  _V
106104, 105ifex 3995 . . . . . . . . . . . . 13  |-  if ( p  e.  Prime ,  ( ( A  /L
p ) ^ (
p  pCnt  N )
) ,  1 )  e.  _V
107103, 36, 106fvmpt 5941 . . . . . . . . . . . 12  |-  ( p  e.  NN  ->  (
( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) `  p
)  =  if ( p  e.  Prime ,  ( ( A  /L
p ) ^ (
p  pCnt  N )
) ,  1 ) )
10893, 107syl 16 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( (
n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) `  p
)  =  if ( p  e.  Prime ,  ( ( A  /L
p ) ^ (
p  pCnt  N )
) ,  1 ) )
109 iftrue 3932 . . . . . . . . . . . 12  |-  ( p  e.  Prime  ->  if ( p  e.  Prime ,  ( ( A  /L
p ) ^ (
p  pCnt  N )
) ,  1 )  =  ( ( A  /L p ) ^ ( p  pCnt  N ) ) )
110109ad2antrl 727 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  if (
p  e.  Prime ,  ( ( A  /L
p ) ^ (
p  pCnt  N )
) ,  1 )  =  ( ( A  /L p ) ^ ( p  pCnt  N ) ) )
111 oveq2 6289 . . . . . . . . . . . . . . . 16  |-  ( p  =  2  ->  ( A  /L p )  =  ( A  /L 2 ) )
112 lgs2 23460 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ZZ  ->  ( A  /L 2 )  =  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) )
11379, 112syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( A  /L 2 )  =  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) )
114111, 113sylan9eqr 2506 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  ( A  /L p )  =  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) )
115 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  p  =  2 )
11683simpld 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  A
)
117116adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  p  ||  A
)
118115, 117eqbrtrrd 4459 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  2  ||  A
)
119118iftrued 3934 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) )  =  0 )
120114, 119eqtrd 2484 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  ( A  /L p )  =  0 )
121 simpll1 1036 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  A  e.  ZZ )
122 simprl 756 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  Prime )
123122adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  Prime )
124 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  =/=  2 )
125 eldifsn 4140 . . . . . . . . . . . . . . . . 17  |-  ( p  e.  ( Prime  \  {
2 } )  <->  ( p  e.  Prime  /\  p  =/=  2 ) )
126123, 124, 125sylanbrc 664 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  ( Prime  \  { 2 } ) )
127 lgsval3 23461 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ZZ  /\  p  e.  ( Prime  \  { 2 } ) )  ->  ( A  /L p )  =  ( ( ( ( A ^ ( ( p  -  1 )  /  2 ) )  +  1 )  mod  p )  -  1 ) )
128121, 126, 127syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  /L
p )  =  ( ( ( ( A ^ ( ( p  -  1 )  / 
2 ) )  +  1 )  mod  p
)  -  1 ) )
129 oddprm 14216 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  e.  ( Prime  \  {
2 } )  -> 
( ( p  - 
1 )  /  2
)  e.  NN )
130126, 129syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( p  - 
1 )  /  2
)  e.  NN )
131130nnnn0d 10858 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( p  - 
1 )  /  2
)  e.  NN0 )
132 zexpcl 12160 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  ZZ  /\  ( ( p  - 
1 )  /  2
)  e.  NN0 )  ->  ( A ^ (
( p  -  1 )  /  2 ) )  e.  ZZ )
133121, 131, 132syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A ^ (
( p  -  1 )  /  2 ) )  e.  ZZ )
134133zred 10974 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A ^ (
( p  -  1 )  /  2 ) )  e.  RR )
135 0red 9600 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
0  e.  RR )
13618a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
1  e.  RR )
137123, 92syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  NN )
138137nnrpd 11264 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  RR+ )
139 0zd 10882 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
0  e.  ZZ )
140116adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  ||  A )
141 dvdsval3 13867 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( p  e.  NN  /\  A  e.  ZZ )  ->  ( p  ||  A  <->  ( A  mod  p )  =  0 ) )
142137, 121, 141syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( p  ||  A  <->  ( A  mod  p )  =  0 ) )
143140, 142mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  mod  p
)  =  0 )
144 0mod 12006 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  e.  RR+  ->  ( 0  mod  p )  =  0 )
145138, 144syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 0  mod  p
)  =  0 )
146143, 145eqtr4d 2487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  mod  p
)  =  ( 0  mod  p ) )
147 modexp 12280 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  e.  ZZ  /\  0  e.  ZZ )  /\  ( ( ( p  -  1 )  /  2 )  e. 
NN0  /\  p  e.  RR+ )  /\  ( A  mod  p )  =  ( 0  mod  p
) )  ->  (
( A ^ (
( p  -  1 )  /  2 ) )  mod  p )  =  ( ( 0 ^ ( ( p  -  1 )  / 
2 ) )  mod  p ) )
148121, 139, 131, 138, 146, 147syl221anc 1240 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( A ^
( ( p  - 
1 )  /  2
) )  mod  p
)  =  ( ( 0 ^ ( ( p  -  1 )  /  2 ) )  mod  p ) )
1491300expd 12305 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 0 ^ (
( p  -  1 )  /  2 ) )  =  0 )
150149oveq1d 6296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( 0 ^ ( ( p  - 
1 )  /  2
) )  mod  p
)  =  ( 0  mod  p ) )
151148, 150eqtrd 2484 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( A ^
( ( p  - 
1 )  /  2
) )  mod  p
)  =  ( 0  mod  p ) )
152 modadd1 12012 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A ^
( ( p  - 
1 )  /  2
) )  e.  RR  /\  0  e.  RR )  /\  ( 1  e.  RR  /\  p  e.  RR+ )  /\  (
( A ^ (
( p  -  1 )  /  2 ) )  mod  p )  =  ( 0  mod  p ) )  -> 
( ( ( A ^ ( ( p  -  1 )  / 
2 ) )  +  1 )  mod  p
)  =  ( ( 0  +  1 )  mod  p ) )
153134, 135, 136, 138, 151, 152syl221anc 1240 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( ( A ^ ( ( p  -  1 )  / 
2 ) )  +  1 )  mod  p
)  =  ( ( 0  +  1 )  mod  p ) )
154 0p1e1 10653 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  +  1 )  =  1
155154oveq1i 6291 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  +  1 )  mod  p )  =  ( 1  mod  p
)
156153, 155syl6eq 2500 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( ( A ^ ( ( p  -  1 )  / 
2 ) )  +  1 )  mod  p
)  =  ( 1  mod  p ) )
157137nnred 10557 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  RR )
158 prmuz2 14112 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  e.  Prime  ->  p  e.  ( ZZ>= `  2 )
)
159123, 158syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  ( ZZ>= ` 
2 ) )
160 eluz2b2 11163 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  e.  ( ZZ>= `  2
)  <->  ( p  e.  NN  /\  1  < 
p ) )
161159, 160sylib 196 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( p  e.  NN  /\  1  <  p ) )
162161simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
1  <  p )
163 1mod 12007 . . . . . . . . . . . . . . . . . . 19  |-  ( ( p  e.  RR  /\  1  <  p )  -> 
( 1  mod  p
)  =  1 )
164157, 162, 163syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 1  mod  p
)  =  1 )
165156, 164eqtrd 2484 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( ( A ^ ( ( p  -  1 )  / 
2 ) )  +  1 )  mod  p
)  =  1 )
166165oveq1d 6296 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( ( ( A ^ ( ( p  -  1 )  /  2 ) )  +  1 )  mod  p )  -  1 )  =  ( 1  -  1 ) )
167 1m1e0 10610 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
168166, 167syl6eq 2500 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( ( ( A ^ ( ( p  -  1 )  /  2 ) )  +  1 )  mod  p )  -  1 )  =  0 )
169128, 168eqtrd 2484 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  /L
p )  =  0 )
170120, 169pm2.61dane 2761 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( A  /L p )  =  0 )
171170oveq1d 6296 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( ( A  /L p ) ^ ( p  pCnt  N ) )  =  ( 0 ^ ( p 
pCnt  N ) ) )
172 zq 11197 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ZZ  ->  N  e.  QQ )
17380, 172syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  N  e.  QQ )
174 pcabs 14275 . . . . . . . . . . . . . . 15  |-  ( ( p  e.  Prime  /\  N  e.  QQ )  ->  (
p  pCnt  ( abs `  N ) )  =  ( p  pCnt  N
) )
175122, 173, 174syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  ( abs `  N
) )  =  ( p  pCnt  N )
)
176 pcelnn 14270 . . . . . . . . . . . . . . . 16  |-  ( ( p  e.  Prime  /\  ( abs `  N )  e.  NN )  ->  (
( p  pCnt  ( abs `  N ) )  e.  NN  <->  p  ||  ( abs `  N ) ) )
177122, 88, 176syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( (
p  pCnt  ( abs `  N ) )  e.  NN  <->  p  ||  ( abs `  N ) ) )
17887, 177mpbird 232 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  ( abs `  N
) )  e.  NN )
179175, 178eqeltrrd 2532 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  N )  e.  NN )
1801790expd 12305 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( 0 ^ ( p  pCnt  N ) )  =  0 )
181171, 180eqtrd 2484 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( ( A  /L p ) ^ ( p  pCnt  N ) )  =  0 )
182108, 110, 1813eqtrd 2488 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( (
n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) `  p
)  =  0 )
18370, 71, 73, 75, 98, 88, 182seqz 12134 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  (  seq 1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) )  =  0 )
184183rexlimdvaa 2936 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( E. p  e.  Prime  p 
||  ( A  gcd  N )  ->  (  seq 1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) )  =  0 ) )
18569, 184syl5 32 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
( ( A  gcd  N )  e.  NN  /\  ( A  gcd  N )  =/=  1 )  -> 
(  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =  0 ) )
18666, 185mpand 675 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
( A  gcd  N
)  =/=  1  -> 
(  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =  0 ) )
187186necon1d 2668 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
(  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =/=  0  ->  ( A  gcd  N
)  =  1 ) )
18851adantr 465 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  -> 
( abs `  N
)  e.  ( ZZ>= ` 
1 ) )
18953adantl 466 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  ( 1 ... ( abs `  N ) ) )  ->  k  e.  NN )
190 eleq1 2515 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
n  e.  Prime  <->  k  e.  Prime ) )
191 oveq2 6289 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  ( A  /L n )  =  ( A  /L k ) )
192 oveq1 6288 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
n  pCnt  N )  =  ( k  pCnt  N ) )
193191, 192oveq12d 6299 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( A  /L
n ) ^ (
n  pCnt  N )
)  =  ( ( A  /L k ) ^ ( k 
pCnt  N ) ) )
194190, 193ifbieq1d 3949 . . . . . . . . . . 11  |-  ( n  =  k  ->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 )  =  if ( k  e.  Prime ,  ( ( A  /L
k ) ^ (
k  pCnt  N )
) ,  1 ) )
195 ovex 6309 . . . . . . . . . . . 12  |-  ( ( A  /L k ) ^ ( k 
pCnt  N ) )  e. 
_V
196195, 105ifex 3995 . . . . . . . . . . 11  |-  if ( k  e.  Prime ,  ( ( A  /L
k ) ^ (
k  pCnt  N )
) ,  1 )  e.  _V
197194, 36, 196fvmpt 5941 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) `  k
)  =  if ( k  e.  Prime ,  ( ( A  /L
k ) ^ (
k  pCnt  N )
) ,  1 ) )
198189, 197syl 16 . . . . . . . . 9  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  ( 1 ... ( abs `  N ) ) )  ->  ( (
n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) `  k
)  =  if ( k  e.  Prime ,  ( ( A  /L
k ) ^ (
k  pCnt  N )
) ,  1 ) )
199 simpll1 1036 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  A  e.  ZZ )
200 prmz 14098 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  Prime  ->  k  e.  ZZ )
201200adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  ZZ )
202 lgscl 23457 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ZZ  /\  k  e.  ZZ )  ->  ( A  /L
k )  e.  ZZ )
203199, 201, 202syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  /L k )  e.  ZZ )
204203zcnd 10975 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  /L k )  e.  CC )
205204adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  ( A  /L k )  e.  CC )
206 oveq2 6289 . . . . . . . . . . . . . . . . 17  |-  ( k  =  2  ->  ( A  /L k )  =  ( A  /L 2 ) )
207199adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  A  e.  ZZ )
208207, 112syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  ( A  /L 2 )  =  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) )
209206, 208sylan9eqr 2506 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  -> 
( A  /L
k )  =  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) )
210 nprmdvds1 14129 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  Prime  ->  -.  k  ||  1 )
211210adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  -.  k  ||  1 )
212 simpll2 1037 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  e.  ZZ )
213 dvdsgcdb 14059 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( k  e.  ZZ  /\  A  e.  ZZ  /\  N  e.  ZZ )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  ( A  gcd  N ) ) )
214201, 199, 212, 213syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  ( A  gcd  N ) ) )
215 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  gcd  N )  =  1 )
216215breq2d 4449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  ( A  gcd  N )  <->  k  ||  1 ) )
217214, 216bitrd 253 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  1 ) )
218211, 217mtbird 301 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  -.  ( k  ||  A  /\  k  ||  N ) )
219 imnan 422 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  ||  A  ->  -.  k  ||  N )  <->  -.  ( k  ||  A  /\  k  ||  N ) )
220218, 219sylibr 212 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  A  ->  -.  k  ||  N ) )
221220con2d 115 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  N  ->  -.  k  ||  A ) )
222221imp 429 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  -.  k  ||  A )
223 breq1 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  2  ->  (
k  ||  A  <->  2  ||  A ) )
224223notbid 294 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  2  ->  ( -.  k  ||  A  <->  -.  2  ||  A ) )
225222, 224syl5ibcom 220 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  (
k  =  2  ->  -.  2  ||  A ) )
226225imp 429 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  ->  -.  2  ||  A )
227226iffalsed 3937 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  ->  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) )  =  if ( ( A  mod  8 )  e. 
{ 1 ,  7 } ,  1 , 
-u 1 ) )
228209, 227eqtrd 2484 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  -> 
( A  /L
k )  =  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) )
229 neeq1 2724 . . . . . . . . . . . . . . . . 17  |-  ( 1  =  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 )  -> 
( 1  =/=  0  <->  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 )  =/=  0
) )
230 neeq1 2724 . . . . . . . . . . . . . . . . 17  |-  ( -u
1  =  if ( ( A  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
)  ->  ( -u 1  =/=  0  <->  if ( ( A  mod  8 )  e. 
{ 1 ,  7 } ,  1 , 
-u 1 )  =/=  0 ) )
231229, 230, 4, 41keephyp 3991 . . . . . . . . . . . . . . . 16  |-  if ( ( A  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
)  =/=  0
232231a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  ->  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 )  =/=  0
)
233228, 232eqnetrd 2736 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  -> 
( A  /L
k )  =/=  0
)
234 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  Prime )
235234ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  Prime )
236235, 210syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  -.  k  ||  1 )
237 simplr 755 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  ||  N )
238235, 200syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  ZZ )
239207adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  A  e.  ZZ )
240 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  =/=  2 )
241 eldifsn 4140 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ( Prime  \  {
2 } )  <->  ( k  e.  Prime  /\  k  =/=  2 ) )
242235, 240, 241sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  ( Prime  \  { 2 } ) )
243 oddprm 14216 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  ( Prime  \  {
2 } )  -> 
( ( k  - 
1 )  /  2
)  e.  NN )
244242, 243syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( k  -  1 )  /  2 )  e.  NN )
245244nnnn0d 10858 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( k  -  1 )  /  2 )  e.  NN0 )
246 zexpcl 12160 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  ZZ  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )  ->  ( A ^ (
( k  -  1 )  /  2 ) )  e.  ZZ )
247239, 245, 246syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A ^ ( ( k  -  1 )  / 
2 ) )  e.  ZZ )
248212ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  N  e.  ZZ )
249 dvdsgcd 14058 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  ZZ  /\  ( A ^ ( ( k  -  1 )  /  2 ) )  e.  ZZ  /\  N  e.  ZZ )  ->  (
( k  ||  ( A ^ ( ( k  -  1 )  / 
2 ) )  /\  k  ||  N )  -> 
k  ||  ( ( A ^ ( ( k  -  1 )  / 
2 ) )  gcd 
N ) ) )
250238, 247, 248, 249syl3anc 1229 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( k  ||  ( A ^ ( ( k  -  1 )  / 
2 ) )  /\  k  ||  N )  -> 
k  ||  ( ( A ^ ( ( k  -  1 )  / 
2 ) )  gcd 
N ) ) )
251237, 250mpan2d 674 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
k  ||  ( A ^ ( ( k  -  1 )  / 
2 ) )  -> 
k  ||  ( ( A ^ ( ( k  -  1 )  / 
2 ) )  gcd 
N ) ) )
252239zcnd 10975 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  A  e.  CC )
253252, 245absexpd 13262 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( abs `  ( A ^
( ( k  - 
1 )  /  2
) ) )  =  ( ( abs `  A
) ^ ( ( k  -  1 )  /  2 ) ) )
254253oveq1d 6296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( abs `  ( A ^ ( ( k  -  1 )  / 
2 ) ) )  gcd  ( abs `  N
) )  =  ( ( ( abs `  A
) ^ ( ( k  -  1 )  /  2 ) )  gcd  ( abs `  N
) ) )
255 gcdabs 14048 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A ^ (
( k  -  1 )  /  2 ) )  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( abs `  ( A ^ ( ( k  -  1 )  / 
2 ) ) )  gcd  ( abs `  N
) )  =  ( ( A ^ (
( k  -  1 )  /  2 ) )  gcd  N ) )
256247, 248, 255syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( abs `  ( A ^ ( ( k  -  1 )  / 
2 ) ) )  gcd  ( abs `  N
) )  =  ( ( A ^ (
( k  -  1 )  /  2 ) )  gcd  N ) )
257 gcdabs 14048 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( abs `  A
)  gcd  ( abs `  N ) )  =  ( A  gcd  N
) )
258239, 248, 257syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( abs `  A
)  gcd  ( abs `  N ) )  =  ( A  gcd  N
) )
259215ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A  gcd  N )  =  1 )
260258, 259eqtrd 2484 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( abs `  A
)  gcd  ( abs `  N ) )  =  1 )
261222adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  -.  k  ||  A )
262 dvds0 13876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  e.  ZZ  ->  k  ||  0 )
263238, 262syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  ||  0 )
264 breq2 4441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  =  0  ->  (
k  ||  A  <->  k  ||  0 ) )
265263, 264syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A  =  0  ->  k 
||  A ) )
266265necon3bd 2655 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( -.  k  ||  A  ->  A  =/=  0 ) )
267261, 266mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  A  =/=  0 )
268 nnabscl 13137 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  ZZ  /\  A  =/=  0 )  -> 
( abs `  A
)  e.  NN )
269239, 267, 268syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( abs `  A )  e.  NN )
270 simpll3 1038 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  =/=  0 )
271212, 270, 48syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( abs `  N )  e.  NN )
272271ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( abs `  N )  e.  NN )
273 rplpwr 14071 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( abs `  A
)  e.  NN  /\  ( abs `  N )  e.  NN  /\  (
( k  -  1 )  /  2 )  e.  NN )  -> 
( ( ( abs `  A )  gcd  ( abs `  N ) )  =  1  ->  (
( ( abs `  A
) ^ ( ( k  -  1 )  /  2 ) )  gcd  ( abs `  N
) )  =  1 ) )
274269, 272, 244, 273syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( ( abs `  A
)  gcd  ( abs `  N ) )  =  1  ->  ( (
( abs `  A
) ^ ( ( k  -  1 )  /  2 ) )  gcd  ( abs `  N
) )  =  1 ) )
275260, 274mpd 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( ( abs `  A
) ^ ( ( k  -  1 )  /  2 ) )  gcd  ( abs `  N
) )  =  1 )
276254, 256, 2753eqtr3d 2492 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( A ^ (
( k  -  1 )  /  2 ) )  gcd  N )  =  1 )
277276breq2d 4449 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
k  ||  ( ( A ^ ( ( k  -  1 )  / 
2 ) )  gcd 
N )  <->  k  ||  1 ) )
278251, 277sylibd 214 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
k  ||  ( A ^ ( ( k  -  1 )  / 
2 ) )  -> 
k  ||  1 ) )
279236, 278mtod 177 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  -.  k  ||  ( A ^
( ( k  - 
1 )  /  2
) ) )
280 prmnn 14097 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Prime  ->  k  e.  NN )
281280adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  NN )
282281ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  NN )
283 dvdsval3 13867 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  ( A ^ ( ( k  -  1 )  /  2 ) )  e.  ZZ )  -> 
( k  ||  ( A ^ ( ( k  -  1 )  / 
2 ) )  <->  ( ( A ^ ( ( k  -  1 )  / 
2 ) )  mod  k )  =  0 ) )
284282, 247, 283syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
k  ||  ( A ^ ( ( k  -  1 )  / 
2 ) )  <->  ( ( A ^ ( ( k  -  1 )  / 
2 ) )  mod  k )  =  0 ) )
285284necon3bbid 2690 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( -.  k  ||  ( A ^ ( ( k  -  1 )  / 
2 ) )  <->  ( ( A ^ ( ( k  -  1 )  / 
2 ) )  mod  k )  =/=  0
) )
286279, 285mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( A ^ (
( k  -  1 )  /  2 ) )  mod  k )  =/=  0 )
287 lgsvalmod 23462 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ZZ  /\  k  e.  ( Prime  \  { 2 } ) )  ->  ( ( A  /L k )  mod  k )  =  ( ( A ^
( ( k  - 
1 )  /  2
) )  mod  k
) )
288239, 242, 287syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( A  /L
k )  mod  k
)  =  ( ( A ^ ( ( k  -  1 )  /  2 ) )  mod  k ) )
289282nnrpd 11264 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  RR+ )
290 0mod 12006 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  RR+  ->  ( 0  mod  k )  =  0 )
291289, 290syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
0  mod  k )  =  0 )
292286, 288, 2913netr4d 2748 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( A  /L
k )  mod  k
)  =/=  ( 0  mod  k ) )
293 oveq1 6288 . . . . . . . . . . . . . . . 16  |-  ( ( A  /L k )  =  0  -> 
( ( A  /L k )  mod  k )  =  ( 0  mod  k ) )
294293necon3i 2683 . . . . . . . . . . . . . . 15  |-  ( ( ( A  /L
k )  mod  k
)  =/=  ( 0  mod  k )  -> 
( A  /L
k )  =/=  0
)
295292, 294syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A  /L k )  =/=  0 )
296233, 295pm2.61dane 2761 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  ( A  /L k )  =/=  0 )
297 pczcl 14249 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  Prime  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( k  pCnt  N
)  e.  NN0 )
298234, 212, 270, 297syl12anc 1227 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  N )  e.  NN0 )
299298nn0zd 10972 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  N )  e.  ZZ )
300299adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  (
k  pCnt  N )  e.  ZZ )
301 expclz 12170 . . . . . . . . . . . . . 14  |-  ( ( ( A  /L
k )  e.  CC  /\  ( A  /L
k )  =/=  0  /\  ( k  pCnt  N
)  e.  ZZ )  ->  ( ( A  /L k ) ^ ( k  pCnt  N ) )  e.  CC )
302 expne0i 12177 . . . . . . . . . . . . . 14  |-  ( ( ( A  /L
k )  e.  CC  /\  ( A  /L
k )  =/=  0  /\  ( k  pCnt  N
)  e.  ZZ )  ->  ( ( A  /L k ) ^ ( k  pCnt  N ) )  =/=  0
)
303 neeq1 2724 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( A  /L k ) ^ ( k  pCnt  N ) )  ->  (
x  =/=  0  <->  (
( A  /L
k ) ^ (
k  pCnt  N )
)  =/=  0 ) )
304303elrab 3243 . . . . . . . . . . . . . 14  |-  ( ( ( A  /L
k ) ^ (
k  pCnt  N )
)  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( (
( A  /L
k ) ^ (
k  pCnt  N )
)  e.  CC  /\  ( ( A  /L k ) ^
( k  pCnt  N
) )  =/=  0
) )
305301, 302, 304sylanbrc 664 . . . . . . . . . . . . 13  |-  ( ( ( A  /L
k )  e.  CC  /\  ( A  /L
k )  =/=  0  /\  ( k  pCnt  N
)  e.  ZZ )  ->  ( ( A  /L k ) ^ ( k  pCnt  N ) )  e.  {
x  e.  CC  |  x  =/=  0 } )
306205, 296, 300, 305syl3anc 1229 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  (
( A  /L
k ) ^ (
k  pCnt  N )
)  e.  { x  e.  CC  |  x  =/=  0 } )
307 dvdsabsb 13880 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ZZ  /\  N  e.  ZZ )  ->  ( k  ||  N  <->  k 
||  ( abs `  N
) ) )
308201, 212, 307syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  N  <->  k  ||  ( abs `  N ) ) )
309308notbid 294 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( -.  k  ||  N  <->  -.  k  ||  ( abs `  N
) ) )
310 pceq0 14271 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  Prime  /\  ( abs `  N )  e.  NN )  ->  (
( k  pCnt  ( abs `  N ) )  =  0  <->  -.  k  ||  ( abs `  N
) ) )
311234, 271, 310syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  pCnt  ( abs `  N ) )  =  0  <->  -.  k  ||  ( abs `  N
) ) )
312212, 172syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  e.  QQ )
313 pcabs 14275 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  Prime  /\  N  e.  QQ )  ->  (
k  pCnt  ( abs `  N ) )  =  ( k  pCnt  N
) )
314234, 312, 313syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  ( abs `  N ) )  =  ( k  pCnt  N
) )
315314eqeq1d 2445 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  pCnt  ( abs `  N ) )  =  0  <->  ( k  pCnt  N )  =  0 ) )
316309, 311, 3153bitr2rd 282 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  pCnt  N
)  =  0  <->  -.  k  ||  N ) )
317316biimpar 485 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( k  pCnt  N
)  =  0 )
318317oveq2d 6297 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( ( A  /L k ) ^
( k  pCnt  N
) )  =  ( ( A  /L
k ) ^ 0 ) )
319204adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( A  /L
k )  e.  CC )
320319exp0d 12283 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( ( A  /L k ) ^
0 )  =  1 )
321318, 320eqtrd 2484 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( ( A  /L k ) ^
( k  pCnt  N
) )  =  1 )
322 neeq1 2724 . . . . . . . . . . . . . . 15  |-  ( x  =  1  ->  (
x  =/=  0  <->  1  =/=  0 ) )
323322elrab 3243 . . . . . . . . . . . . . 14  |-  ( 1  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( 1  e.  CC  /\  1  =/=  0 ) )
32445, 4, 323mpbir2an 920 . . . . . . . . . . . . 13  |-  1  e.  { x  e.  CC  |  x  =/=  0 }
325321, 324syl6eqel 2539 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( ( A  /L k ) ^
( k  pCnt  N
) )  e.  {
x  e.  CC  |  x  =/=  0 } )
326306, 325pm2.61dan 791 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( A  /L
k ) ^ (
k  pCnt  N )
)  e.  { x  e.  CC  |  x  =/=  0 } )
327324a1i 11 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  -.  k  e.  Prime )  -> 
1  e.  { x  e.  CC  |  x  =/=  0 } )
328326, 327ifclda 3958 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  ->  if ( k  e.  Prime ,  ( ( A  /L k ) ^
( k  pCnt  N
) ) ,  1 )  e.  { x  e.  CC  |  x  =/=  0 } )
329328adantr 465 . . . . . . . . 9  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  ( 1 ... ( abs `  N ) ) )  ->  if (
k  e.  Prime ,  ( ( A  /L
k ) ^ (
k  pCnt  N )
) ,  1 )  e.  { x  e.  CC  |  x  =/=  0 } )
330198, 329eqeltrd 2531 . . . . . . . 8  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  ( 1 ... ( abs `  N ) ) )  ->  ( (
n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) `  k
)  e.  { x  e.  CC  |  x  =/=  0 } )
331 neeq1 2724 . . . . . . . . . . . 12  |-  ( x  =  k  ->  (
x  =/=  0  <->  k  =/=  0 ) )
332331elrab 3243 . . . . . . . . . . 11  |-  ( k  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( k  e.  CC  /\  k  =/=  0 ) )
333 neeq1 2724 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
x  =/=  0  <->  y  =/=  0 ) )
334333elrab 3243 . . . . . . . . . . 11  |-  ( y  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( y  e.  CC  /\  y  =/=  0 ) )
335 mulcl 9579 . . . . . . . . . . . . 13  |-  ( ( k  e.  CC  /\  y  e.  CC )  ->  ( k  x.  y
)  e.  CC )
336335ad2ant2r 746 . . . . . . . . . . . 12  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( k  x.  y
)  e.  CC )
337 mulne0 10197 . . . . . . . . . . . 12  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( k  x.  y
)  =/=  0 )
338336, 337jca 532 . . . . . . . . . . 11  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( ( k  x.  y )  e.  CC  /\  ( k  x.  y
)  =/=  0 ) )
339332, 334, 338syl2anb 479 . . . . . . . . . 10  |-  ( ( k  e.  { x  e.  CC  |  x  =/=  0 }  /\  y  e.  { x  e.  CC  |  x  =/=  0 } )  ->  (
( k  x.  y
)  e.  CC  /\  ( k  x.  y
)  =/=  0 ) )
340 neeq1 2724 . . . . . . . . . . 11  |-  ( x  =  ( k  x.  y )  ->  (
x  =/=  0  <->  (
k  x.  y )  =/=  0 ) )
341340elrab 3243 . . . . . . . . . 10  |-  ( ( k  x.  y )  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( (
k  x.  y )  e.  CC  /\  (
k  x.  y )  =/=  0 ) )
342339, 341sylibr 212 . . . . . . . . 9  |-  ( ( k  e.  { x  e.  CC  |  x  =/=  0 }  /\  y  e.  { x  e.  CC  |  x  =/=  0 } )  ->  (
k  x.  y )  e.  { x  e.  CC  |  x  =/=  0 } )
343342adantl 466 . . . . . . . 8  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  (
k  e.  { x  e.  CC  |  x  =/=  0 }  /\  y  e.  { x  e.  CC  |  x  =/=  0 } ) )  -> 
( k  x.  y
)  e.  { x  e.  CC  |  x  =/=  0 } )
344188, 330, 343seqcl 12106 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  -> 
(  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  e.  {
x  e.  CC  |  x  =/=  0 } )
345 neeq1 2724 . . . . . . . . 9  |-  ( x  =  (  seq 1
(  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) )  ->  ( x  =/=  0  <->  (  seq 1
(  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) )  =/=  0 ) )
346345elrab 3243 . . . . . . . 8  |-  ( (  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  e.  {
x  e.  CC  |  x  =/=  0 }  <->  ( (  seq 1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^
( n  pCnt  N
) ) ,  1 ) ) ) `  ( abs `  N ) )  e.  CC  /\  (  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =/=  0
) )
347346simprbi 464 . . . . . . 7  |-  ( (  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  e.  {
x  e.  CC  |  x  =/=  0 }  ->  (  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =/=  0
)
348344, 347syl 16 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  -> 
(  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =/=  0
)
349348ex 434 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
( A  gcd  N
)  =  1  -> 
(  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =/=  0
) )
350187, 349impbid 191 . . . 4  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
(  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  /L n ) ^ ( n 
pCnt  N ) ) ,  1 ) ) ) `
 ( abs `  N
) )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
35138, 61, 3503bitrd 279 . . 3  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
( A  /L
N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
3523513expa 1197 . 2  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =/=  0
)  ->  ( ( A  /L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
35335, 352pm2.61dane 2761 1  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( A  /L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 974    = wceq 1383    e. wcel 1804    =/= wne 2638   E.wrex 2794   {crab 2797    \ cdif 3458   ifcif 3926   {csn 4014   {cpr 4016   class class class wbr 4437    |-> cmpt 4495   -->wf 5574   ` cfv 5578  (class class class)co 6281   CCcc 9493   RRcr 9494   0cc0 9495   1c1 9496    + caddc 9498    x. cmul 9500    < clt 9631    <_ cle 9632    - cmin 9810   -ucneg 9811    / cdiv 10212   NNcn 10542   2c2 10591   7c7 10596   8c8 10597   NN0cn0 10801   ZZcz 10870   ZZ>=cuz 11090   QQcq 11191   RR+crp 11229   ...cfz 11681    mod cmo 11975    seqcseq 12086   ^cexp 12145   abscabs 13046    || cdvds 13863    gcd cgcd 14021   Primecprime 14094    pCnt cpc 14237    /Lclgs 23441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri