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

Theorem lgsne0 20572
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 3572 . . . . . 6  |-  ( -.  ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =  0 )
21necon1ai 2488 . . . . 5  |-  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  -> 
( A ^ 2 )  =  1 )
3 iftrue 3571 . . . . . 6  |-  ( ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =  1 )
4 ax-1ne0 8806 . . . . . . 7  |-  1  =/=  0
54a1i 10 . . . . . 6  |-  ( ( A ^ 2 )  =  1  ->  1  =/=  0 )
63, 5eqnetrd 2464 . . . . 5  |-  ( ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0 )
72, 6impbii 180 . . . 4  |-  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  <->  ( A ^ 2 )  =  1 )
8 zre 10028 . . . . . . . 8  |-  ( A  e.  ZZ  ->  A  e.  RR )
98ad2antrr 706 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  A  e.  RR )
10 absresq 11787 . . . . . . 7  |-  ( A  e.  RR  ->  (
( abs `  A
) ^ 2 )  =  ( A ^
2 ) )
119, 10syl 15 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( abs `  A ) ^
2 )  =  ( A ^ 2 ) )
12 sq1 11198 . . . . . . 7  |-  ( 1 ^ 2 )  =  1
1312a1i 10 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( 1 ^ 2 )  =  1 )
1411, 13eqeq12d 2297 . . . . 5  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( (
( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( A ^ 2 )  =  1 ) )
159recnd 8861 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  A  e.  CC )
1615abscld 11918 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( abs `  A )  e.  RR )
1715absge0d 11926 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  0  <_  ( abs `  A ) )
18 1re 8837 . . . . . . 7  |-  1  e.  RR
19 0le1 9297 . . . . . . 7  |-  0  <_  1
20 sq11 11176 . . . . . . 7  |-  ( ( ( ( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) )  /\  (
1  e.  RR  /\  0  <_  1 ) )  ->  ( ( ( abs `  A ) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A
)  =  1 ) )
2118, 19, 20mpanr12 666 . . . . . 6  |-  ( ( ( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) )  ->  (
( ( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A )  =  1 ) )
2216, 17, 21syl2anc 642 . . . . 5  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( (
( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A )  =  1 ) )
2314, 22bitr3d 246 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A ^ 2 )  =  1  <->  ( abs `  A
)  =  1 ) )
247, 23syl5bb 248 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  <->  ( abs `  A )  =  1 ) )
25 oveq2 5866 . . . . 5  |-  ( N  =  0  ->  ( A  / L N )  =  ( A  / L 0 ) )
26 lgs0 20548 . . . . . 6  |-  ( A  e.  ZZ  ->  ( A  / L 0 )  =  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) )
2726adantr 451 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( A  / L
0 )  =  if ( ( A ^
2 )  =  1 ,  1 ,  0 ) )
2825, 27sylan9eqr 2337 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( A  / L N )  =  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) )
2928neeq1d 2459 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  / L N )  =/=  0  <->  if (
( A ^ 2 )  =  1 ,  1 ,  0 )  =/=  0 ) )
30 oveq2 5866 . . . . 5  |-  ( N  =  0  ->  ( A  gcd  N )  =  ( A  gcd  0
) )
31 gcdid0 12703 . . . . . 6  |-  ( A  e.  ZZ  ->  ( A  gcd  0 )  =  ( abs `  A
) )
3231adantr 451 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( A  gcd  0
)  =  ( abs `  A ) )
3330, 32sylan9eqr 2337 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( A  gcd  N )  =  ( abs `  A ) )
3433eqeq1d 2291 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  gcd  N )  =  1  <->  ( abs `  A
)  =  1 ) )
3524, 29, 343bitr4d 276 . 2  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  / L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
36 eqid 2283 . . . . . 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 20555 . . . . 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 2459 . . . 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 2454 . . . . . . 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 2454 . . . . . . 7  |-  ( 1  =  if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  ->  ( 1  =/=  0  <->  if (
( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  =/=  0 ) )
41 ax-1cn 8795 . . . . . . . 8  |-  1  e.  CC
4241, 4negne0i 9121 . . . . . . 7  |-  -u 1  =/=  0
4339, 40, 42, 4keephyp 3619 . . . . . 6  |-  if ( ( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  =/=  0
4443biantrur 492 . . . . 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 ) )
45 neg1cn 9813 . . . . . . . 8  |-  -u 1  e.  CC
4645, 41keepel 3622 . . . . . . 7  |-  if ( ( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  e.  CC
4746a1i 10 . . . . . 6  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  if ( ( N  <  0  /\  A  <  0 ) ,  -u
1 ,  1 )  e.  CC )
48 nnabscl 11809 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  N  =/=  0 )  -> 
( abs `  N
)  e.  NN )
49483adant1 973 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( abs `  N )  e.  NN )
50 nnuz 10263 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
5149, 50syl6eleq 2373 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( abs `  N )  e.  ( ZZ>= `  1 )
)
5236lgsfcl3 20556 . . . . . . . . 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 10819 . . . . . . . . 9  |-  ( k  e.  ( 1 ... ( abs `  N
) )  ->  k  e.  NN )
54 ffvelrn 5663 . . . . . . . . 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 463 . . . . . . . 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 10118 . . . . . . 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 8821 . . . . . . . 8  |-  ( ( k  e.  CC  /\  x  e.  CC )  ->  ( k  x.  x
)  e.  CC )
5857adantl 452 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( k  e.  CC  /\  x  e.  CC ) )  ->  ( k  x.  x )  e.  CC )
5951, 56, 58seqcl 11066 . . . . . 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 9419 . . . . 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
) )
6144, 60syl5rbb 249 . . . 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 447 . . . . . . . . . 10  |-  ( ( A  =  0  /\  N  =  0 )  ->  N  =  0 )
6362necon3ai 2486 . . . . . . . . 9  |-  ( N  =/=  0  ->  -.  ( A  =  0  /\  N  =  0
) )
64 gcdn0cl 12693 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  -.  ( A  =  0  /\  N  =  0 ) )  ->  ( A  gcd  N )  e.  NN )
6563, 64sylan2 460 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =/=  0
)  ->  ( A  gcd  N )  e.  NN )
66653impa 1146 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( A  gcd  N )  e.  NN )
67 eluz2b3 10291 . . . . . . . . 9  |-  ( ( A  gcd  N )  e.  ( ZZ>= `  2
)  <->  ( ( A  gcd  N )  e.  NN  /\  ( A  gcd  N )  =/=  1 ) )
68 exprmfct 12789 . . . . . . . . 9  |-  ( ( A  gcd  N )  e.  ( ZZ>= `  2
)  ->  E. p  e.  Prime  p  ||  ( A  gcd  N ) )
6967, 68sylbir 204 . . . . . . . 8  |-  ( ( ( A  gcd  N
)  e.  NN  /\  ( A  gcd  N )  =/=  1 )  ->  E. p  e.  Prime  p 
||  ( A  gcd  N ) )
7057adantl 452 . . . . . . . . . . 11  |-  ( ( ( ( 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 695 . . . . . . . . . . 11  |-  ( ( ( ( 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 8990 . . . . . . . . . . . 12  |-  ( k  e.  CC  ->  (
0  x.  k )  =  0 )
7372adantl 452 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  k  e.  CC )  ->  ( 0  x.  k
)  =  0 )
74 mul01 8991 . . . . . . . . . . . 12  |-  ( k  e.  CC  ->  (
k  x.  0 )  =  0 )
7574adantl 452 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  k  e.  CC )  ->  ( k  x.  0 )  =  0 )
76 simprr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  ( A  gcd  N ) )
77 prmz 12762 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  Prime  ->  p  e.  ZZ )
7877ad2antrl 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ZZ )
79 simpl1 958 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  A  e.  ZZ )
80 simpl2 959 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  N  e.  ZZ )
81 dvdsgcdb 12723 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  ZZ  /\  A  e.  ZZ  /\  N  e.  ZZ )  ->  (
( p  ||  A  /\  p  ||  N )  <-> 
p  ||  ( A  gcd  N ) ) )
8278, 79, 80, 81syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 223 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  A  /\  p  ||  N ) )
8483simprd 449 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  N
)
85 dvdsabsb 12548 . . . . . . . . . . . . . . 15  |-  ( ( p  e.  ZZ  /\  N  e.  ZZ )  ->  ( p  ||  N  <->  p 
||  ( abs `  N
) ) )
8678, 80, 85syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  N  <->  p  ||  ( abs `  N ) ) )
8784, 86mpbid 201 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  ( abs `  N ) )
8849adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( abs `  N )  e.  NN )
89 dvdsle 12574 . . . . . . . . . . . . . 14  |-  ( ( p  e.  ZZ  /\  ( abs `  N )  e.  NN )  -> 
( p  ||  ( abs `  N )  ->  p  <_  ( abs `  N
) ) )
9078, 88, 89syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  ( abs `  N
)  ->  p  <_  ( abs `  N ) ) )
9187, 90mpd 14 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  <_  ( abs `  N ) )
92 prmnn 12761 . . . . . . . . . . . . . . 15  |-  ( p  e.  Prime  ->  p  e.  NN )
9392ad2antrl 708 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  NN )
9493, 50syl6eleq 2373 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ( ZZ>= `  1 )
)
9588nnzd 10116 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( abs `  N )  e.  ZZ )
96 elfz5 10790 . . . . . . . . . . . . 13  |-  ( ( p  e.  ( ZZ>= ` 
1 )  /\  ( abs `  N )  e.  ZZ )  ->  (
p  e.  ( 1 ... ( abs `  N
) )  <->  p  <_  ( abs `  N ) ) )
9794, 95, 96syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( 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 223 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ( 1 ... ( abs `  N ) ) )
99 eleq1 2343 . . . . . . . . . . . . . . 15  |-  ( n  =  p  ->  (
n  e.  Prime  <->  p  e.  Prime ) )
100 oveq2 5866 . . . . . . . . . . . . . . . 16  |-  ( n  =  p  ->  ( A  / L n )  =  ( A  / L p ) )
101 oveq1 5865 . . . . . . . . . . . . . . . 16  |-  ( n  =  p  ->  (
n  pCnt  N )  =  ( p  pCnt  N ) )
102100, 101oveq12d 5876 . . . . . . . . . . . . . . 15  |-  ( n  =  p  ->  (
( A  / L
n ) ^ (
n  pCnt  N )
)  =  ( ( A  / L p ) ^ ( p 
pCnt  N ) ) )
103 eqidd 2284 . . . . . . . . . . . . . . 15  |-  ( n  =  p  ->  1  =  1 )
10499, 102, 103ifbieq12d 3587 . . . . . . . . . . . . . 14  |-  ( n  =  p  ->  if ( n  e.  Prime ,  ( ( A  / L n ) ^
( n  pCnt  N
) ) ,  1 )  =  if ( p  e.  Prime ,  ( ( A  / L
p ) ^ (
p  pCnt  N )
) ,  1 ) )
105 ovex 5883 . . . . . . . . . . . . . . 15  |-  ( ( A  / L p ) ^ ( p 
pCnt  N ) )  e. 
_V
106 1ex 8833 . . . . . . . . . . . . . . 15  |-  1  e.  _V
107105, 106ifex 3623 . . . . . . . . . . . . . 14  |-  if ( p  e.  Prime ,  ( ( A  / L
p ) ^ (
p  pCnt  N )
) ,  1 )  e.  _V
108104, 36, 107fvmpt 5602 . . . . . . . . . . . . 13  |-  ( 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 ) )
10993, 108syl 15 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
110 iftrue 3571 . . . . . . . . . . . . 13  |-  ( p  e.  Prime  ->  if ( p  e.  Prime ,  ( ( A  / L
p ) ^ (
p  pCnt  N )
) ,  1 )  =  ( ( A  / L p ) ^ ( p  pCnt  N ) ) )
111110ad2antrl 708 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
112 oveq2 5866 . . . . . . . . . . . . . . . . 17  |-  ( p  =  2  ->  ( A  / L p )  =  ( A  / L 2 ) )
113 lgs2 20552 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  ZZ  ->  ( A  / L 2 )  =  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) )
11479, 113syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )
115112, 114sylan9eqr 2337 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) )
116 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  p  =  2 )
11783simpld 445 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  A
)
118117adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  p  ||  A
)
119116, 118eqbrtrrd 4045 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  2  ||  A
)
120 iftrue 3571 . . . . . . . . . . . . . . . . 17  |-  ( 2 
||  A  ->  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) )  =  0 )
121119, 120syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )
122115, 121eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  ( A  / L p )  =  0 )
123 simpll1 994 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  A  e.  ZZ )
124 simprl 732 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  Prime )
125124adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  Prime )
126 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  =/=  2 )
127 eldifsn 3749 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  ( Prime  \  {
2 } )  <->  ( p  e.  Prime  /\  p  =/=  2 ) )
128125, 126, 127sylanbrc 645 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  ( Prime  \  { 2 } ) )
129 lgsval3 20553 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ZZ  /\  p  e.  ( Prime  \  { 2 } ) )  ->  ( A  / L p )  =  ( ( ( ( A ^ ( ( p  -  1 )  /  2 ) )  +  1 )  mod  p )  -  1 ) )
130123, 128, 129syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
131 oddprm 12868 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  e.  ( Prime  \  {
2 } )  -> 
( ( p  - 
1 )  /  2
)  e.  NN )
132128, 131syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( p  - 
1 )  /  2
)  e.  NN )
133132nnnn0d 10018 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( p  - 
1 )  /  2
)  e.  NN0 )
134 zexpcl 11118 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  ZZ  /\  ( ( p  - 
1 )  /  2
)  e.  NN0 )  ->  ( A ^ (
( p  -  1 )  /  2 ) )  e.  ZZ )
135123, 133, 134syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A ^ (
( p  -  1 )  /  2 ) )  e.  ZZ )
136135zred 10117 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A ^ (
( p  -  1 )  /  2 ) )  e.  RR )
137 0re 8838 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
138137a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
0  e.  RR )
13918a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
1  e.  RR )
140125, 92syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  NN )
141140nnrpd 10389 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  RR+ )
142 0z 10035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  ZZ
143142a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
0  e.  ZZ )
144117adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  ||  A )
145 dvdsval3 12535 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( p  e.  NN  /\  A  e.  ZZ )  ->  ( p  ||  A  <->  ( A  mod  p )  =  0 ) )
146140, 123, 145syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( p  ||  A  <->  ( A  mod  p )  =  0 ) )
147144, 146mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  mod  p
)  =  0 )
148 0mod 10995 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  e.  RR+  ->  ( 0  mod  p )  =  0 )
149141, 148syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 0  mod  p
)  =  0 )
150147, 149eqtr4d 2318 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  mod  p
)  =  ( 0  mod  p ) )
151 modexp 11236 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) )
152123, 143, 133, 141, 150, 151syl221anc 1193 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 ) )
1531320expd 11261 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 0 ^ (
( p  -  1 )  /  2 ) )  =  0 )
154153oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 ) )
155152, 154eqtrd 2315 . . . . . . . . . . . . . . . . . . . . 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  mod  p ) )
156 modadd1 11001 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 ) )
157136, 138, 139, 141, 155, 156syl221anc 1193 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) )
158 0p1e1 9839 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  +  1 )  =  1
159158oveq1i 5868 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  +  1 )  mod  p )  =  ( 1  mod  p
)
160157, 159syl6eq 2331 . . . . . . . . . . . . . . . . . . 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
)  =  ( 1  mod  p ) )
161140nnred 9761 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  RR )
162 prmuz2 12776 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( p  e.  Prime  ->  p  e.  ( ZZ>= `  2 )
)
163125, 162syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  ( ZZ>= ` 
2 ) )
164 eluz2b2 10290 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  e.  ( ZZ>= `  2
)  <->  ( p  e.  NN  /\  1  < 
p ) )
165163, 164sylib 188 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( p  e.  NN  /\  1  <  p ) )
166165simprd 449 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
1  <  p )
167 1mod 10996 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( p  e.  RR  /\  1  <  p )  -> 
( 1  mod  p
)  =  1 )
168161, 166, 167syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 1  mod  p
)  =  1 )
169160, 168eqtrd 2315 . . . . . . . . . . . . . . . . . 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 )
170169oveq1d 5873 . . . . . . . . . . . . . . . . 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 )  =  ( 1  -  1 ) )
171 1m1e0 9814 . . . . . . . . . . . . . . . . 17  |-  ( 1  -  1 )  =  0
172170, 171syl6eq 2331 . . . . . . . . . . . . . . . 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 )  =  0 )
173130, 172eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  / L
p )  =  0 )
174122, 173pm2.61dane 2524 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( A  / L p )  =  0 )
175174oveq1d 5873 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
176 zq 10322 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ZZ  ->  N  e.  QQ )
17780, 176syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  N  e.  QQ )
178 pcabs 12927 . . . . . . . . . . . . . . . 16  |-  ( ( p  e.  Prime  /\  N  e.  QQ )  ->  (
p  pCnt  ( abs `  N ) )  =  ( p  pCnt  N
) )
179124, 177, 178syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  ( abs `  N
) )  =  ( p  pCnt  N )
)
180 pcelnn 12922 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  Prime  /\  ( abs `  N )  e.  NN )  ->  (
( p  pCnt  ( abs `  N ) )  e.  NN  <->  p  ||  ( abs `  N ) ) )
181124, 88, 180syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( (
p  pCnt  ( abs `  N ) )  e.  NN  <->  p  ||  ( abs `  N ) ) )
18287, 181mpbird 223 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  ( abs `  N
) )  e.  NN )
183179, 182eqeltrrd 2358 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  N )  e.  NN )
1841830expd 11261 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( 0 ^ ( p  pCnt  N ) )  =  0 )
185175, 184eqtrd 2315 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( ( A  / L p ) ^ ( p  pCnt  N ) )  =  0 )
186109, 111, 1853eqtrd 2319 . . . . . . . . . . 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
)  =  0 )
18770, 71, 73, 75, 98, 88, 186seqz 11094 . . . . . . . . . 10  |-  ( ( ( 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 )
188187expr 598 . . . . . . . . 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 ) )
189188rexlimdva 2667 . . . . . . . 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 ) )
19069, 189syl5 28 . . . . . . 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 ) )
19166, 190mpand 656 . . . . . 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 ) )
192191necon1d 2515 . . . . 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 ) )
19351adantr 451 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  -> 
( abs `  N
)  e.  ( ZZ>= ` 
1 ) )
19453adantl 452 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  ( 1 ... ( abs `  N ) ) )  ->  k  e.  NN )
195 eleq1 2343 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
n  e.  Prime  <->  k  e.  Prime ) )
196 oveq2 5866 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  ( A  / L n )  =  ( A  / L k ) )
197 oveq1 5865 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
n  pCnt  N )  =  ( k  pCnt  N ) )
198196, 197oveq12d 5876 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( A  / L
n ) ^ (
n  pCnt  N )
)  =  ( ( A  / L k ) ^ ( k 
pCnt  N ) ) )
199 eqidd 2284 . . . . . . . . . . . 12  |-  ( n  =  k  ->  1  =  1 )
200195, 198, 199ifbieq12d 3587 . . . . . . . . . . 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 ) )
201 ovex 5883 . . . . . . . . . . . 12  |-  ( ( A  / L k ) ^ ( k 
pCnt  N ) )  e. 
_V
202201, 106ifex 3623 . . . . . . . . . . 11  |-  if ( k  e.  Prime ,  ( ( A  / L
k ) ^ (
k  pCnt  N )
) ,  1 )  e.  _V
203200, 36, 202fvmpt 5602 . . . . . . . . . 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 ) )
204194, 203syl 15 . . . . . . . . 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 ) )
205 simpll1 994 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  A  e.  ZZ )
206 prmz 12762 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  Prime  ->  k  e.  ZZ )
207206adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  ZZ )
208 lgscl 20549 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ZZ  /\  k  e.  ZZ )  ->  ( A  / L
k )  e.  ZZ )
209205, 207, 208syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  / L k )  e.  ZZ )
210209zcnd 10118 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  / L k )  e.  CC )
211210adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  ( A  / L k )  e.  CC )
212 oveq2 5866 . . . . . . . . . . . . . . . . 17  |-  ( k  =  2  ->  ( A  / L k )  =  ( A  / L 2 ) )
213205adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  A  e.  ZZ )
214213, 113syl 15 . . . . . . . . . . . . . . . . 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 ) ) )
215212, 214sylan9eqr 2337 . . . . . . . . . . . . . . . 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 ) ) )
216 nprmdvds1 12790 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  Prime  ->  -.  k  ||  1 )
217216adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  -.  k  ||  1 )
218 simpll2 995 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  e.  ZZ )
219 dvdsgcdb 12723 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( k  e.  ZZ  /\  A  e.  ZZ  /\  N  e.  ZZ )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  ( A  gcd  N ) ) )
220207, 205, 218, 219syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  ( A  gcd  N ) ) )
221 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  gcd  N )  =  1 )
222221breq2d 4035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  ( A  gcd  N )  <->  k  ||  1 ) )
223220, 222bitrd 244 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  1 ) )
224217, 223mtbird 292 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  -.  ( k  ||  A  /\  k  ||  N ) )
225 imnan 411 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  ||  A  ->  -.  k  ||  N )  <->  -.  ( k  ||  A  /\  k  ||  N ) )
226224, 225sylibr 203 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  A  ->  -.  k  ||  N ) )
227226con2d 107 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  N  ->  -.  k  ||  A ) )
228227imp 418 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  -.  k  ||  A )
229 breq1 4026 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  2  ->  (
k  ||  A  <->  2  ||  A ) )
230229notbid 285 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  2  ->  ( -.  k  ||  A  <->  -.  2  ||  A ) )
231228, 230syl5ibcom 211 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  (
k  =  2  ->  -.  2  ||  A ) )
232231imp 418 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  ->  -.  2  ||  A )
233 iffalse 3572 . . . . . . . . . . . . . . . . 17  |-  ( -.  2  ||  A  ->  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) )  =  if ( ( A  mod  8 )  e. 
{ 1 ,  7 } ,  1 , 
-u 1 ) )
234232, 233syl 15 . . . . . . . . . . . . . . . 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 ) )
235215, 234eqtrd 2315 . . . . . . . . . . . . . . 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 ) )
236 neeq1 2454 . . . . . . . . . . . . . . . . 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
) )
237 neeq1 2454 . . . . . . . . . . . . . . . . 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 ) )
238236, 237, 4, 42keephyp 3619 . . . . . . . . . . . . . . . 16  |-  if ( ( A  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
)  =/=  0
239238a1i 10 . . . . . . . . . . . . . . 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
)
240235, 239eqnetrd 2464 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  -> 
( A  / L
k )  =/=  0
)
241 simpr 447 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  Prime )
242241ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  Prime )
243242, 216syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  -.  k  ||  1 )
244 simplr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  ||  N )
245242, 206syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  ZZ )
246213adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  A  e.  ZZ )
247 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  =/=  2 )
248 eldifsn 3749 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ( Prime  \  {
2 } )  <->  ( k  e.  Prime  /\  k  =/=  2 ) )
249242, 247, 248sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  ( Prime  \  { 2 } ) )
250 oddprm 12868 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  ( Prime  \  {
2 } )  -> 
( ( k  - 
1 )  /  2
)  e.  NN )
251249, 250syl 15 . . . . . . . . . . . . . . . . . . . . . . 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 )
252251nnnn0d 10018 . . . . . . . . . . . . . . . . . . . . . 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 )
253 zexpcl 11118 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  ZZ  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )  ->  ( A ^ (
( k  -  1 )  /  2 ) )  e.  ZZ )
254246, 252, 253syl2anc 642 . . . . . . . . . . . . . . . . . . . . 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 )
255218ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  N  e.  ZZ )
256 dvdsgcd 12722 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
257245, 254, 255, 256syl3anc 1182 . . . . . . . . . . . . . . . . . . . 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 ) ) )
258244, 257mpan2d 655 . . . . . . . . . . . . . . . . . . 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 ) ) )
259246zcnd 10118 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  A  e.  CC )
260259, 252absexpd 11934 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
261260oveq1d 5873 . . . . . . . . . . . . . . . . . . . . 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
) ) )
262 gcdabs 12712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A ^ (
( k  -  1 )  /  2 ) )  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( abs `  ( A ^ ( ( k  -  1 )  / 
2 ) ) )  gcd  ( abs `  N
) )  =  ( ( A ^ (
( k  -  1 )  /  2 ) )  gcd  N ) )
263254, 255, 262syl2anc 642 . . . . . . . . . . . . . . . . . . . . 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 ) )
264 gcdabs 12712 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( abs `  A
)  gcd  ( abs `  N ) )  =  ( A  gcd  N
) )
265246, 255, 264syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 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
) )
266221ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A  gcd  N )  =  1 )
267265, 266eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . 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 )
268228adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  -.  k  ||  A )
269 dvds0 12544 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  e.  ZZ  ->  k  ||  0 )
270245, 269syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  ||  0 )
271 breq2 4027 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  =  0  ->  (
k  ||  A  <->  k  ||  0 ) )
272270, 271syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A  =  0  ->  k 
||  A ) )
273272necon3bd 2483 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( -.  k  ||  A  ->  A  =/=  0 ) )
274268, 273mpd 14 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  A  =/=  0 )
275 nnabscl 11809 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  ZZ  /\  A  =/=  0 )  -> 
( abs `  A
)  e.  NN )
276246, 274, 275syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( abs `  A )  e.  NN )
277 simpll3 996 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  =/=  0 )
278218, 277, 48syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( abs `  N )  e.  NN )
279278ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( abs `  N )  e.  NN )
280 rplpwr 12735 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
281276, 279, 251, 280syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . 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 ) )
282267, 281mpd 14 . . . . . . . . . . . . . . . . . . . . 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 )
283261, 263, 2823eqtr3d 2323 . . . . . . . . . . . . . . . . . . . 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 )
284283breq2d 4035 . . . . . . . . . . . . . . . . . . 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 ) )
285258, 284sylibd 205 . . . . . . . . . . . . . . . . . 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 ) )
286243, 285mtod 168 . . . . . . . . . . . . . . . . 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
) ) )
287 prmnn 12761 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Prime  ->  k  e.  NN )
288287adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  NN )
289288ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  NN )
290 dvdsval3 12535 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  ( A ^ ( ( k  -  1 )  /  2 ) )  e.  ZZ )  -> 
( k  ||  ( A ^ ( ( k  -  1 )  / 
2 ) )  <->  ( ( A ^ ( ( k  -  1 )  / 
2 ) )  mod  k )  =  0 ) )
291289, 254, 290syl2anc 642 . . . . . . . . . . . . . . . . . 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 ) )
292291necon3bbid 2480 . . . . . . . . . . . . . . . . 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
) )
293286, 292mpbid 201 . . . . . . . . . . . . . . . 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 )
294 lgsvalmod 20554 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ZZ  /\  k  e.  ( Prime  \  { 2 } ) )  ->  ( ( A  / L k )  mod  k )  =  ( ( A ^
( ( k  - 
1 )  /  2
) )  mod  k
) )
295246, 249, 294syl2anc 642 . . . . . . . . . . . . . . . 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 ) )
296289nnrpd 10389 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  RR+ )
297 0mod 10995 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  RR+  ->  ( 0  mod  k )  =  0 )
298296, 297syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
0  mod  k )  =  0 )
299293, 295, 2983netr4d 2473 . . . . . . . . . . . . . . 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 ) )
300 oveq1 5865 . . . . . . . . . . . . . . . 16  |-  ( ( A  / L k )  =  0  -> 
( ( A  / L k )  mod  k )  =  ( 0  mod  k ) )
301300necon3i 2485 . . . . . . . . . . . . . . 15  |-  ( ( ( A  / L
k )  mod  k
)  =/=  ( 0  mod  k )  -> 
( A  / L
k )  =/=  0
)
302299, 301syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A  / L k )  =/=  0 )
303240, 302pm2.61dane 2524 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  ( A  / L k )  =/=  0 )
304 pczcl 12901 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  Prime  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( k  pCnt  N
)  e.  NN0 )
305241, 218, 277, 304syl12anc 1180 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  N )  e.  NN0 )
306305nn0zd 10115 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  N )  e.  ZZ )
307306adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  (
k  pCnt  N )  e.  ZZ )
308 expclz 11128 . . . . . . . . . . . . . 14  |-  ( ( ( A  / L
k )  e.  CC  /\  ( A  / L
k )  =/=  0  /\  ( k  pCnt  N
)  e.  ZZ )  ->  ( ( A  / L k ) ^ ( k  pCnt  N ) )  e.  CC )
309 expne0i 11134 . . . . . . . . . . . . . 14  |-  ( ( ( A  / L
k )  e.  CC  /\  ( A  / L
k )  =/=  0  /\  ( k  pCnt  N
)  e.  ZZ )  ->  ( ( A  / L k ) ^ ( k  pCnt  N ) )  =/=  0
)
310 neeq1 2454 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( A  / L k ) ^ ( k  pCnt  N ) )  ->  (
x  =/=  0  <->  (
( A  / L
k ) ^ (
k  pCnt  N )
)  =/=  0 ) )
311310elrab 2923 . . . . . . . . . . . . . 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
) )
312308, 309, 311sylanbrc 645 . . . . . . . . . . . . 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 } )
313211, 303, 307, 312syl3anc 1182 . . . . . . . . . . . 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 } )
314 dvdsabsb 12548 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ZZ  /\  N  e.  ZZ )  ->  ( k  ||  N  <->  k 
||  ( abs `  N
) ) )
315207, 218, 314syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  N  <->  k  ||  ( abs `  N ) ) )
316315notbid 285 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( -.  k  ||  N  <->  -.  k  ||  ( abs `  N
) ) )
317 pceq0 12923 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  Prime  /\  ( abs `  N )  e.  NN )  ->  (
( k  pCnt  ( abs `  N ) )  =  0  <->  -.  k  ||  ( abs `  N
) ) )
318241, 278, 317syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  pCnt  ( abs `  N ) )  =  0  <->  -.  k  ||  ( abs `  N
) ) )
319218, 176syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  e.  QQ )
320 pcabs 12927 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  Prime  /\  N  e.  QQ )  ->  (
k  pCnt  ( abs `  N ) )  =  ( k  pCnt  N
) )
321241, 319, 320syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  ( abs `  N ) )  =  ( k  pCnt  N
) )
322321eqeq1d 2291 . . . . . . . . . . . . . . . . 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 ) )
323316, 318, 3223bitr2rd 273 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  pCnt  N
)  =  0  <->  -.  k  ||  N ) )
324323biimpar 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( k  pCnt  N
)  =  0 )
325324oveq2d 5874 . . . . . . . . . . . . . 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 ) )
326210adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( A  / L
k )  e.  CC )
327326exp0d 11239 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( ( A  / L k ) ^
0 )  =  1 )
328325, 327eqtrd 2315 . . . . . . . . . . . . 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 )
329 neeq1 2454 . . . . . . . . . . . . . . 15  |-  ( x  =  1  ->  (
x  =/=  0  <->  1  =/=  0 ) )
330329elrab 2923 . . . . . . . . . . . . . 14  |-  ( 1  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( 1  e.  CC  /\  1  =/=  0 ) )
33141, 4, 330mpbir2an 886 . . . . . . . . . . . . 13  |-  1  e.  { x  e.  CC  |  x  =/=  0 }
332328, 331syl6eqel 2371 . . . . . . . . . . . 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 } )
333313, 332pm2.61dan 766 . . . . . . . . . . 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 } )
334331a1i 10 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  -.  k  e.  Prime )  -> 
1  e.  { x  e.  CC  |  x  =/=  0 } )
335333, 334ifclda 3592 . . . . . . . . . 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 } )
336335adantr 451 . . . . . . . . 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 } )
337204, 336eqeltrd 2357 . . . . . . . 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 } )
338 neeq1 2454 . . . . . . . . . . . 12  |-  ( x  =  k  ->  (
x  =/=  0  <->  k  =/=  0 ) )
339338elrab 2923 . . . . . . . . . . 11  |-  ( k  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( k  e.  CC  /\  k  =/=  0 ) )
340 neeq1 2454 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
x  =/=  0  <->  y  =/=  0 ) )
341340elrab 2923 . . . . . . . . . . 11  |-  ( y  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( y  e.  CC  /\  y  =/=  0 ) )
342 mulcl 8821 . . . . . . . . . . . . 13  |-  ( ( k  e.  CC  /\  y  e.  CC )  ->  ( k  x.  y
)  e.  CC )
343342ad2ant2r 727 . . . . . . . . . . . 12  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( k  x.  y
)  e.  CC )
344 mulne0 9410 . . . . . . . . . . . 12  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( k  x.  y
)  =/=  0 )
345343, 344jca 518 . . . . . . . . . . 11  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( ( k  x.  y )  e.  CC  /\  ( k  x.  y
)  =/=  0 ) )
346339, 341, 345syl2anb 465 . . . . . . . . . 10  |-  ( ( k  e.  { x  e.  CC  |  x  =/=  0 }  /\  y  e.  { x  e.  CC  |  x  =/=  0 } )  ->  (
( k  x.  y
)  e.  CC  /\  ( k  x.  y
)  =/=  0 ) )
347 neeq1 2454 . . . . . . . . . . 11  |-  ( x  =  ( k  x.  y )  ->  (
x  =/=  0  <->  (
k  x.  y )  =/=  0 ) )
348347elrab 2923 . . . . . . . . . 10  |-  ( ( k  x.  y )  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( (
k  x.  y )  e.  CC  /\  (
k  x.  y )  =/=  0 ) )
349346, 348sylibr 203 . . . . . . . . 9  |-  ( ( k  e.  { x  e.  CC  |  x  =/=  0 }  /\  y  e.  { x  e.  CC  |  x  =/=  0 } )  ->  (
k  x.  y )  e.  { x  e.  CC  |  x  =/=  0 } )
350349adantl 452 . . . . . . . 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 } )
351193, 337, 350seqcl 11066 . . . . . . 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 } )
352 neeq1 2454 . . . . . . . . 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 ) )
353352elrab 2923 . . . . . . . 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
) )
354353simprbi 450 . . . . . . 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
)
355351, 354syl 15 . . . . . 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 )
356355ex 423 . . . . 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 ) )
357192, 356impbid 183 . . . 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 )