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

Theorem lgsne0 24198
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 3858 . . . . . 6  |-  ( -.  ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =  0 )
21necon1ai 2623 . . . . 5  |-  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  -> 
( A ^ 2 )  =  1 )
3 iftrue 3855 . . . . . 6  |-  ( ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =  1 )
4 ax-1ne0 9554 . . . . . . 7  |-  1  =/=  0
54a1i 11 . . . . . 6  |-  ( ( A ^ 2 )  =  1  ->  1  =/=  0 )
63, 5eqnetrd 2663 . . . . 5  |-  ( ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0 )
72, 6impbii 190 . . . 4  |-  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  <->  ( A ^ 2 )  =  1 )
8 zre 10887 . . . . . . . 8  |-  ( A  e.  ZZ  ->  A  e.  RR )
98ad2antrr 730 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  A  e.  RR )
10 absresq 13304 . . . . . . 7  |-  ( A  e.  RR  ->  (
( abs `  A
) ^ 2 )  =  ( A ^
2 ) )
119, 10syl 17 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( abs `  A ) ^
2 )  =  ( A ^ 2 ) )
12 sq1 12314 . . . . . . 7  |-  ( 1 ^ 2 )  =  1
1312a1i 11 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( 1 ^ 2 )  =  1 )
1411, 13eqeq12d 2438 . . . . 5  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( (
( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( A ^ 2 )  =  1 ) )
159recnd 9615 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  A  e.  CC )
1615abscld 13436 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( abs `  A )  e.  RR )
1715absge0d 13444 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  0  <_  ( abs `  A ) )
18 1re 9588 . . . . . . 7  |-  1  e.  RR
19 0le1 10083 . . . . . . 7  |-  0  <_  1
20 sq11 12292 . . . . . . 7  |-  ( ( ( ( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) )  /\  (
1  e.  RR  /\  0  <_  1 ) )  ->  ( ( ( abs `  A ) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A
)  =  1 ) )
2118, 19, 20mpanr12 689 . . . . . 6  |-  ( ( ( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) )  ->  (
( ( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A )  =  1 ) )
2216, 17, 21syl2anc 665 . . . . 5  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( (
( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A )  =  1 ) )
2314, 22bitr3d 258 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A ^ 2 )  =  1  <->  ( abs `  A
)  =  1 ) )
247, 23syl5bb 260 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  <->  ( abs `  A )  =  1 ) )
25 oveq2 6252 . . . . 5  |-  ( N  =  0  ->  ( A  /L N )  =  ( A  /L 0 ) )
26 lgs0 24174 . . . . . 6  |-  ( A  e.  ZZ  ->  ( A  /L 0 )  =  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) )
2726adantr 466 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( A  /L 0 )  =  if ( ( A ^
2 )  =  1 ,  1 ,  0 ) )
2825, 27sylan9eqr 2479 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( A  /L N )  =  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) )
2928neeq1d 2655 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  /L N )  =/=  0  <->  if (
( A ^ 2 )  =  1 ,  1 ,  0 )  =/=  0 ) )
30 oveq2 6252 . . . . 5  |-  ( N  =  0  ->  ( A  gcd  N )  =  ( A  gcd  0
) )
31 gcdid0 14426 . . . . . 6  |-  ( A  e.  ZZ  ->  ( A  gcd  0 )  =  ( abs `  A
) )
3231adantr 466 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( A  gcd  0
)  =  ( abs `  A ) )
3330, 32sylan9eqr 2479 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( A  gcd  N )  =  ( abs `  A ) )
3433eqeq1d 2425 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  gcd  N )  =  1  <->  ( abs `  A
)  =  1 ) )
3524, 29, 343bitr4d 288 . 2  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  /L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
36 eqid 2423 . . . . . 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 24181 . . . . 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 2655 . . . 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 2658 . . . . . . 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 2658 . . . . . . 7  |-  ( 1  =  if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  ->  ( 1  =/=  0  <->  if (
( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  =/=  0 ) )
41 neg1ne0 10661 . . . . . . 7  |-  -u 1  =/=  0
4239, 40, 41, 4keephyp 3913 . . . . . 6  |-  if ( ( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  =/=  0
4342biantrur 508 . . . . 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 10659 . . . . . . . 8  |-  -u 1  e.  CC
45 ax-1cn 9543 . . . . . . . 8  |-  1  e.  CC
4644, 45keepel 3916 . . . . . . 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 13327 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  N  =/=  0 )  -> 
( abs `  N
)  e.  NN )
49483adant1 1023 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( abs `  N )  e.  NN )
50 nnuz 11140 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
5149, 50syl6eleq 2511 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( abs `  N )  e.  ( ZZ>= `  1 )
)
5236lgsfcl3 24182 . . . . . . . . 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 11774 . . . . . . . . 9  |-  ( k  e.  ( 1 ... ( abs `  N
) )  ->  k  e.  NN )
54 ffvelrn 5974 . . . . . . . . 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 479 . . . . . . . 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 10987 . . . . . . 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 9569 . . . . . . . 8  |-  ( ( k  e.  CC  /\  x  e.  CC )  ->  ( k  x.  x
)  e.  CC )
5857adantl 467 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( k  e.  CC  /\  x  e.  CC ) )  ->  ( k  x.  x )  e.  CC )
5951, 56, 58seqcl 12178 . . . . . 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 10209 . . . . 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 261 . . . 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 462 . . . . . . . . . 10  |-  ( ( A  =  0  /\  N  =  0 )  ->  N  =  0 )
6362necon3ai 2621 . . . . . . . . 9  |-  ( N  =/=  0  ->  -.  ( A  =  0  /\  N  =  0
) )
64 gcdn0cl 14414 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  -.  ( A  =  0  /\  N  =  0 ) )  ->  ( A  gcd  N )  e.  NN )
6563, 64sylan2 476 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =/=  0
)  ->  ( A  gcd  N )  e.  NN )
66653impa 1200 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( A  gcd  N )  e.  NN )
67 eluz2b3 11178 . . . . . . . . 9  |-  ( ( A  gcd  N )  e.  ( ZZ>= `  2
)  <->  ( ( A  gcd  N )  e.  NN  /\  ( A  gcd  N )  =/=  1 ) )
68 exprmfct 14586 . . . . . . . . 9  |-  ( ( A  gcd  N )  e.  ( ZZ>= `  2
)  ->  E. p  e.  Prime  p  ||  ( A  gcd  N ) )
6967, 68sylbir 216 . . . . . . . 8  |-  ( ( ( A  gcd  N
)  e.  NN  /\  ( A  gcd  N )  =/=  1 )  ->  E. p  e.  Prime  p 
||  ( A  gcd  N ) )
7057adantl 467 . . . . . . . . . 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 719 . . . . . . . . . 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 9757 . . . . . . . . . . 11  |-  ( k  e.  CC  ->  (
0  x.  k )  =  0 )
7372adantl 467 . . . . . . . . . 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 9758 . . . . . . . . . . 11  |-  ( k  e.  CC  ->  (
k  x.  0 )  =  0 )
7574adantl 467 . . . . . . . . . 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 764 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  ( A  gcd  N ) )
77 prmz 14564 . . . . . . . . . . . . . . . . 17  |-  ( p  e.  Prime  ->  p  e.  ZZ )
7877ad2antrl 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ZZ )
79 simpl1 1008 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  A  e.  ZZ )
80 simpl2 1009 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  N  e.  ZZ )
81 dvdsgcdb 14450 . . . . . . . . . . . . . . . 16  |-  ( ( p  e.  ZZ  /\  A  e.  ZZ  /\  N  e.  ZZ )  ->  (
( p  ||  A  /\  p  ||  N )  <-> 
p  ||  ( A  gcd  N ) ) )
8278, 79, 80, 81syl3anc 1264 . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  A  /\  p  ||  N ) )
8483simprd 464 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  N
)
85 dvdsabsb 14260 . . . . . . . . . . . . . 14  |-  ( ( p  e.  ZZ  /\  N  e.  ZZ )  ->  ( p  ||  N  <->  p 
||  ( abs `  N
) ) )
8678, 80, 85syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  N  <->  p  ||  ( abs `  N ) ) )
8784, 86mpbid 213 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  ( abs `  N ) )
8849adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( abs `  N )  e.  NN )
89 dvdsle 14288 . . . . . . . . . . . . 13  |-  ( ( p  e.  ZZ  /\  ( abs `  N )  e.  NN )  -> 
( p  ||  ( abs `  N )  ->  p  <_  ( abs `  N
) ) )
9078, 88, 89syl2anc 665 . . . . . . . . . . . 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 14563 . . . . . . . . . . . . . 14  |-  ( p  e.  Prime  ->  p  e.  NN )
9392ad2antrl 732 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  NN )
9493, 50syl6eleq 2511 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ( ZZ>= `  1 )
)
9588nnzd 10985 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( abs `  N )  e.  ZZ )
96 elfz5 11738 . . . . . . . . . . . 12  |-  ( ( p  e.  ( ZZ>= ` 
1 )  /\  ( abs `  N )  e.  ZZ )  ->  (
p  e.  ( 1 ... ( abs `  N
) )  <->  p  <_  ( abs `  N ) ) )
9794, 95, 96syl2anc 665 . . . . . . . . . . 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 235 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ( 1 ... ( abs `  N ) ) )
99 eleq1 2489 . . . . . . . . . . . . . 14  |-  ( n  =  p  ->  (
n  e.  Prime  <->  p  e.  Prime ) )
100 oveq2 6252 . . . . . . . . . . . . . . 15  |-  ( n  =  p  ->  ( A  /L n )  =  ( A  /L p ) )
101 oveq1 6251 . . . . . . . . . . . . . . 15  |-  ( n  =  p  ->  (
n  pCnt  N )  =  ( p  pCnt  N ) )
102100, 101oveq12d 6262 . . . . . . . . . . . . . 14  |-  ( n  =  p  ->  (
( A  /L
n ) ^ (
n  pCnt  N )
)  =  ( ( A  /L p ) ^ ( p 
pCnt  N ) ) )
10399, 102ifbieq1d 3872 . . . . . . . . . . . . 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 6272 . . . . . . . . . . . . . 14  |-  ( ( A  /L p ) ^ ( p 
pCnt  N ) )  e. 
_V
105 1ex 9584 . . . . . . . . . . . . . 14  |-  1  e.  _V
106104, 105ifex 3917 . . . . . . . . . . . . 13  |-  if ( p  e.  Prime ,  ( ( A  /L
p ) ^ (
p  pCnt  N )
) ,  1 )  e.  _V
107103, 36, 106fvmpt 5903 . . . . . . . . . . . 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 17 . . . . . . . . . . 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 3855 . . . . . . . . . . . 12  |-  ( p  e.  Prime  ->  if ( p  e.  Prime ,  ( ( A  /L
p ) ^ (
p  pCnt  N )
) ,  1 )  =  ( ( A  /L p ) ^ ( p  pCnt  N ) ) )
110109ad2antrl 732 . . . . . . . . . . 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 6252 . . . . . . . . . . . . . . . 16  |-  ( p  =  2  ->  ( A  /L p )  =  ( A  /L 2 ) )
112 lgs2 24178 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ZZ  ->  ( A  /L 2 )  =  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) )
11379, 112syl 17 . . . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  p  =  2 )
11683simpld 460 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  A
)
117116adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  p  ||  A
)
118115, 117eqbrtrrd 4384 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  2  ||  A
)
119118iftrued 3857 . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  ( A  /L p )  =  0 )
121 simpll1 1044 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  A  e.  ZZ )
122 simprl 762 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  Prime )
123122adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  Prime )
124 simpr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  =/=  2 )
125 eldifsn 4063 . . . . . . . . . . . . . . . . 17  |-  ( p  e.  ( Prime  \  {
2 } )  <->  ( p  e.  Prime  /\  p  =/=  2 ) )
126123, 124, 125sylanbrc 668 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  ( Prime  \  { 2 } ) )
127 lgsval3 24179 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ZZ  /\  p  e.  ( Prime  \  { 2 } ) )  ->  ( A  /L p )  =  ( ( ( ( A ^ ( ( p  -  1 )  /  2 ) )  +  1 )  mod  p )  -  1 ) )
128121, 126, 127syl2anc 665 . . . . . . . . . . . . . . 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 14703 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  e.  ( Prime  \  {
2 } )  -> 
( ( p  - 
1 )  /  2
)  e.  NN )
130126, 129syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( p  - 
1 )  /  2
)  e.  NN )
131130nnnn0d 10871 . . . . . . . . . . . . . . . . . . . . . 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 12232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  ZZ  /\  ( ( p  - 
1 )  /  2
)  e.  NN0 )  ->  ( A ^ (
( p  -  1 )  /  2 ) )  e.  ZZ )
133121, 131, 132syl2anc 665 . . . . . . . . . . . . . . . . . . . . 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 10986 . . . . . . . . . . . . . . . . . . . 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 9590 . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  NN )
138137nnrpd 11285 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  RR+ )
139 0zd 10895 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
0  e.  ZZ )
140116adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  ||  A )
141 dvdsval3 14247 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( p  e.  NN  /\  A  e.  ZZ )  ->  ( p  ||  A  <->  ( A  mod  p )  =  0 ) )
142137, 121, 141syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  mod  p
)  =  0 )
144 0mod 12073 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  e.  RR+  ->  ( 0  mod  p )  =  0 )
145138, 144syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 0  mod  p
)  =  0 )
146143, 145eqtr4d 2460 . . . . . . . . . . . . . . . . . . . . . 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 12352 . . . . . . . . . . . . . . . . . . . . . 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 1275 . . . . . . . . . . . . . . . . . . . . 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 12377 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 0 ^ (
( p  -  1 )  /  2 ) )  =  0 )
150149oveq1d 6259 . . . . . . . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . . . . . . . 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 12079 . . . . . . . . . . . . . . . . . . . 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 1275 . . . . . . . . . . . . . . . . . . 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 10667 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  +  1 )  =  1
155154oveq1i 6254 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  +  1 )  mod  p )  =  ( 1  mod  p
)
156153, 155syl6eq 2473 . . . . . . . . . . . . . . . . . 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 10570 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  RR )
158 prmuz2 14580 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  e.  Prime  ->  p  e.  ( ZZ>= `  2 )
)
159123, 158syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  ( ZZ>= ` 
2 ) )
160 eluz2b2 11177 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  e.  ( ZZ>= `  2
)  <->  ( p  e.  NN  /\  1  < 
p ) )
161159, 160sylib 199 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( p  e.  NN  /\  1  <  p ) )
162161simprd 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
1  <  p )
163 1mod 12074 . . . . . . . . . . . . . . . . . . 19  |-  ( ( p  e.  RR  /\  1  <  p )  -> 
( 1  mod  p
)  =  1 )
164157, 162, 163syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 1  mod  p
)  =  1 )
165156, 164eqtrd 2457 . . . . . . . . . . . . . . . . 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 6259 . . . . . . . . . . . . . . . 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 10624 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
168166, 167syl6eq 2473 . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . 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 2683 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( A  /L p )  =  0 )
171170oveq1d 6259 . . . . . . . . . . . 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 11216 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ZZ  ->  N  e.  QQ )
17380, 172syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  N  e.  QQ )
174 pcabs 14762 . . . . . . . . . . . . . . 15  |-  ( ( p  e.  Prime  /\  N  e.  QQ )  ->  (
p  pCnt  ( abs `  N ) )  =  ( p  pCnt  N
) )
175122, 173, 174syl2anc 665 . . . . . . . . . . . . . 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 14757 . . . . . . . . . . . . . . . 16  |-  ( ( p  e.  Prime  /\  ( abs `  N )  e.  NN )  ->  (
( p  pCnt  ( abs `  N ) )  e.  NN  <->  p  ||  ( abs `  N ) ) )
177122, 88, 176syl2anc 665 . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  ( abs `  N
) )  e.  NN )
179175, 178eqeltrrd 2502 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  N )  e.  NN )
1801790expd 12377 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( 0 ^ ( p  pCnt  N ) )  =  0 )
181171, 180eqtrd 2457 . . . . . . . . . . 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 2461 . . . . . . . . . 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 12206 . . . . . . . . 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 2852 . . . . . . . 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 33 . . . . . . 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 679 . . . . . 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 2618 . . . . 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 466 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  -> 
( abs `  N
)  e.  ( ZZ>= ` 
1 ) )
18953adantl 467 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  ( 1 ... ( abs `  N ) ) )  ->  k  e.  NN )
190 eleq1 2489 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
n  e.  Prime  <->  k  e.  Prime ) )
191 oveq2 6252 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  ( A  /L n )  =  ( A  /L k ) )
192 oveq1 6251 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
n  pCnt  N )  =  ( k  pCnt  N ) )
193191, 192oveq12d 6262 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( A  /L
n ) ^ (
n  pCnt  N )
)  =  ( ( A  /L k ) ^ ( k 
pCnt  N ) ) )
194190, 193ifbieq1d 3872 . . . . . . . . . . 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 6272 . . . . . . . . . . . 12  |-  ( ( A  /L k ) ^ ( k 
pCnt  N ) )  e. 
_V
196195, 105ifex 3917 . . . . . . . . . . 11  |-  if ( k  e.  Prime ,  ( ( A  /L
k ) ^ (
k  pCnt  N )
) ,  1 )  e.  _V
197194, 36, 196fvmpt 5903 . . . . . . . . . 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 17 . . . . . . . . 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 1044 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  A  e.  ZZ )
200 prmz 14564 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  Prime  ->  k  e.  ZZ )
201200adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  ZZ )
202 lgscl 24175 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ZZ  /\  k  e.  ZZ )  ->  ( A  /L
k )  e.  ZZ )
203199, 201, 202syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  /L k )  e.  ZZ )
204203zcnd 10987 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  /L k )  e.  CC )
205204adantr 466 . . . . . . . . . . . . 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 6252 . . . . . . . . . . . . . . . . 17  |-  ( k  =  2  ->  ( A  /L k )  =  ( A  /L 2 ) )
207199adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  A  e.  ZZ )
208207, 112syl 17 . . . . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . . . . 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 14588 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  Prime  ->  -.  k  ||  1 )
211210adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  -.  k  ||  1 )
212 simpll2 1045 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  e.  ZZ )
213 dvdsgcdb 14450 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( k  e.  ZZ  /\  A  e.  ZZ  /\  N  e.  ZZ )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  ( A  gcd  N ) ) )
214201, 199, 212, 213syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  gcd  N )  =  1 )
216215breq2d 4373 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  ( A  gcd  N )  <->  k  ||  1 ) )
217214, 216bitrd 256 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  1 ) )
218211, 217mtbird 302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  -.  ( k  ||  A  /\  k  ||  N ) )
219 imnan 423 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  ||  A  ->  -.  k  ||  N )  <->  -.  ( k  ||  A  /\  k  ||  N ) )
220218, 219sylibr 215 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  A  ->  -.  k  ||  N ) )
221220con2d 118 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  N  ->  -.  k  ||  A ) )
222221imp 430 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  -.  k  ||  A )
223 breq1 4364 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  2  ->  (
k  ||  A  <->  2  ||  A ) )
224223notbid 295 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  2  ->  ( -.  k  ||  A  <->  -.  2  ||  A ) )
225222, 224syl5ibcom 223 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  (
k  =  2  ->  -.  2  ||  A ) )
226225imp 430 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  ->  -.  2  ||  A )
227226iffalsed 3860 . . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . . 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 2658 . . . . . . . . . . . . . . . . 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 2658 . . . . . . . . . . . . . . . . 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 3913 . . . . . . . . . . . . . . . 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 2663 . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  Prime )
235234ad2antrr 730 . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  -.  k  ||  1 )
237 simplr 760 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  ||  N )
238235, 200syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  ZZ )
239207adantr 466 . . . . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  =/=  2 )
241 eldifsn 4063 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ( Prime  \  {
2 } )  <->  ( k  e.  Prime  /\  k  =/=  2 ) )
242235, 240, 241sylanbrc 668 . . . . . . . . . . . . . . . . . . . . . . . 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 14703 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  ( Prime  \  {
2 } )  -> 
( ( k  - 
1 )  /  2
)  e.  NN )
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . 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 10871 . . . . . . . . . . . . . . . . . . . . . 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 12232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  ZZ  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )  ->  ( A ^ (
( k  -  1 )  /  2 ) )  e.  ZZ )
247239, 245, 246syl2anc 665 . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . 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 14449 . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . 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 678 . . . . . . . . . . . . . . . . . . 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 10987 . . . . . . . . . . . . . . . . . . . . . . 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 13452 . . . . . . . . . . . . . . . . . . . . . 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 6259 . . . . . . . . . . . . . . . . . . . . 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 14435 . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . 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 14435 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( abs `  A
)  gcd  ( abs `  N ) )  =  ( A  gcd  N
) )
258239, 248, 257syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  -.  k  ||  A )
262 dvds0 14256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  e.  ZZ  ->  k  ||  0 )
263238, 262syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  ||  0 )
264 breq2 4365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  =  0  ->  (
k  ||  A  <->  k  ||  0 ) )
265263, 264syl5ibrcom 225 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2610 . . . . . . . . . . . . . . . . . . . . . . . . 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 13327 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  ZZ  /\  A  =/=  0 )  -> 
( abs `  A
)  e.  NN )
269239, 267, 268syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 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 1046 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  =/=  0 )
271212, 270, 48syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( abs `  N )  e.  NN )
272271ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 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 14462 . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . 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 2465 . . . . . . . . . . . . . . . . . . . 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 4373 . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . 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 180 . . . . . . . . . . . . . . . . 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 14563 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Prime  ->  k  e.  NN )
281280adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  NN )
282281ad2antrr 730 . . . . . . . . . . . . . . . . . . 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 14247 . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . 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 2633 . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . 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 24180 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ZZ  /\  k  e.  ( Prime  \  { 2 } ) )  ->  ( ( A  /L k )  mod  k )  =  ( ( A ^
( ( k  - 
1 )  /  2
) )  mod  k
) )
288239, 242, 287syl2anc 665 . . . . . . . . . . . . . . . 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 11285 . . . . . . . . . . . . . . . . 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 12073 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  RR+  ->  ( 0  mod  k )  =  0 )
291289, 290syl 17 . . . . . . . . . . . . . . . 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 2673 . . . . . . . . . . . . . . 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 6251 . . . . . . . . . . . . . . . 16  |-  ( ( A  /L k )  =  0  -> 
( ( A  /L k )  mod  k )  =  ( 0  mod  k ) )
294293necon3i 2628 . . . . . . . . . . . . . . 15  |-  ( ( ( A  /L
k )  mod  k
)  =/=  ( 0  mod  k )  -> 
( A  /L
k )  =/=  0
)
295292, 294syl 17 . . . . . . . . . . . . . 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 2683 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  ( A  /L k )  =/=  0 )
297 pczcl 14736 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  Prime  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( k  pCnt  N
)  e.  NN0 )
298234, 212, 270, 297syl12anc 1262 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  N )  e.  NN0 )
299298nn0zd 10984 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  N )  e.  ZZ )
300299adantr 466 . . . . . . . . . . . . 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 12242 . . . . . . . . . . . . . 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 12249 . . . . . . . . . . . . . 14  |-  ( ( ( A  /L
k )  e.  CC  /\  ( A  /L
k )  =/=  0  /\  ( k  pCnt  N
)  e.  ZZ )  ->  ( ( A  /L k ) ^ ( k  pCnt  N ) )  =/=  0
)
303 neeq1 2658 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( A  /L k ) ^ ( k  pCnt  N ) )  ->  (
x  =/=  0  <->  (
( A  /L
k ) ^ (
k  pCnt  N )
)  =/=  0 ) )
304303elrab 3166 . . . . . . . . . . . . . 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 668 . . . . . . . . . . . . 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 1264 . . . . . . . . . . . 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 14260 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ZZ  /\  N  e.  ZZ )  ->  ( k  ||  N  <->  k 
||  ( abs `  N
) ) )
308201, 212, 307syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  N  <->  k  ||  ( abs `  N ) ) )
309308notbid 295 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( -.  k  ||  N  <->  -.  k  ||  ( abs `  N
) ) )
310 pceq0 14758 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  Prime  /\  ( abs `  N )  e.  NN )  ->  (
( k  pCnt  ( abs `  N ) )  =  0  <->  -.  k  ||  ( abs `  N
) ) )
311234, 271, 310syl2anc 665 . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  e.  QQ )
313 pcabs 14762 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  Prime  /\  N  e.  QQ )  ->  (
k  pCnt  ( abs `  N ) )  =  ( k  pCnt  N
) )
314234, 312, 313syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  ( abs `  N ) )  =  ( k  pCnt  N
) )
315314eqeq1d 2425 . . . . . . . . . . . . . . . . 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 285 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  pCnt  N
)  =  0  <->  -.  k  ||  N ) )
317316biimpar 487 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( k  pCnt  N
)  =  0 )
318317oveq2d 6260 . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( A  /L
k )  e.  CC )
320319exp0d 12355 . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . 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 2658 . . . . . . . . . . . . . . 15  |-  ( x  =  1  ->  (
x  =/=  0  <->  1  =/=  0 ) )
323322elrab 3166 . . . . . . . . . . . . . 14  |-  ( 1  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( 1  e.  CC  /\  1  =/=  0 ) )
32445, 4, 323mpbir2an 928 . . . . . . . . . . . . 13  |-  1  e.  { x  e.  CC  |  x  =/=  0 }
325321, 324syl6eqel 2509 . . . . . . . . . . . 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 798 . . . . . . . . . . 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 3881 . . . . . . . . . 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 466 . . . . . . . . 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 2501 . . . . . . . 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 2658 . . . . . . . . . . . 12  |-  ( x  =  k  ->  (
x  =/=  0  <->  k  =/=  0 ) )
332331elrab 3166 . . . . . . . . . . 11  |-  ( k  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( k  e.  CC  /\  k  =/=  0 ) )
333 neeq1 2658 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
x  =/=  0  <->  y  =/=  0 ) )
334333elrab 3166 . . . . . . . . . . 11  |-  ( y  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( y  e.  CC  /\  y  =/=  0 ) )
335 mulcl 9569 . . . . . . . . . . . . 13  |-  ( ( k  e.  CC  /\  y  e.  CC )  ->  ( k  x.  y
)  e.  CC )
336335ad2ant2r 751 . . . . . . . . . . . 12  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( k  x.  y
)  e.  CC )
337 mulne0 10200 . . . . . . . . . . . 12  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( k  x.  y
)  =/=  0 )
338336, 337jca 534 . . . . . . . . . . 11  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( ( k  x.  y )  e.  CC  /\  ( k  x.  y
)  =/=  0 ) )
339332, 334, 338syl2anb 481 . . . . . . . . . 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 2658 . . . . . . . . . . 11  |-  ( x  =  ( k  x.  y )  ->  (
x  =/=  0  <->  (
k  x.  y )  =/=  0 ) )
341340elrab 3166 . . . . . . . . . 10  |-  ( ( k  x.  y )  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( (
k  x.  y )  e.  CC  /\  (
k  x.  y )  =/=  0 ) )
342339, 341sylibr 215 . . . . . . . . 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 467 . . . . . . . 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 12178 . . . . . . 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 2658 . . . . . . . . 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 3166 . . . . . . . 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 465 . . . . . . 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 17 . . . . . 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 435 . . . . 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 193 . . . 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 282 . . 3  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
( A  /L
N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
3523513expa 1205 . 2  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =/=  0
)  ->  ( ( A  /L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
35335, 352pm2.61dane 2683 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 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872    =/= wne 2594   E.wrex 2710   {crab 2713    \ cdif 3371   ifcif 3849   {csn 3936   {cpr 3938   class class class wbr 4361    |-> cmpt 4420   -->wf 5535   ` cfv 5539  (class class class)co 6244   CCcc 9483   RRcr 9484   0cc0 9485   1c1 9486    + caddc 9488    x. cmul 9490    < clt 9621    <_ cle 9622    - cmin 9806   -ucneg 9807    / cdiv 10215   NNcn 10555   2c2 10605   7c7 10610   8c8 10611   NN0cn0 10815   ZZcz 10883   ZZ>=cuz 11105   QQcq 11210   RR+crp 11248   ...cfz 11730    mod cmo 12041    seqcseq 12158   ^cexp 12217   abscabs 13236    || cdvds 14243    gcd cgcd 14406   Primecprime 14560    pCnt cpc 14724    /Lclgs 24159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559