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

Theorem lgsne0 21119
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 3748 . . . . . 6  |-  ( -.  ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =  0 )
21necon1ai 2648 . . . . 5  |-  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  -> 
( A ^ 2 )  =  1 )
3 iftrue 3747 . . . . . 6  |-  ( ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =  1 )
4 ax-1ne0 9061 . . . . . . 7  |-  1  =/=  0
54a1i 11 . . . . . 6  |-  ( ( A ^ 2 )  =  1  ->  1  =/=  0 )
63, 5eqnetrd 2621 . . . . 5  |-  ( ( A ^ 2 )  =  1  ->  if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0 )
72, 6impbii 182 . . . 4  |-  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  <->  ( A ^ 2 )  =  1 )
8 zre 10288 . . . . . . . 8  |-  ( A  e.  ZZ  ->  A  e.  RR )
98ad2antrr 708 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  A  e.  RR )
10 absresq 12109 . . . . . . 7  |-  ( A  e.  RR  ->  (
( abs `  A
) ^ 2 )  =  ( A ^
2 ) )
119, 10syl 16 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( abs `  A ) ^
2 )  =  ( A ^ 2 ) )
12 sq1 11478 . . . . . . 7  |-  ( 1 ^ 2 )  =  1
1312a1i 11 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( 1 ^ 2 )  =  1 )
1411, 13eqeq12d 2452 . . . . 5  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( (
( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( A ^ 2 )  =  1 ) )
159recnd 9116 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  A  e.  CC )
1615abscld 12240 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( abs `  A )  e.  RR )
1715absge0d 12248 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  0  <_  ( abs `  A ) )
18 1re 9092 . . . . . . 7  |-  1  e.  RR
19 0le1 9553 . . . . . . 7  |-  0  <_  1
20 sq11 11456 . . . . . . 7  |-  ( ( ( ( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) )  /\  (
1  e.  RR  /\  0  <_  1 ) )  ->  ( ( ( abs `  A ) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A
)  =  1 ) )
2118, 19, 20mpanr12 668 . . . . . 6  |-  ( ( ( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) )  ->  (
( ( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A )  =  1 ) )
2216, 17, 21syl2anc 644 . . . . 5  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( (
( abs `  A
) ^ 2 )  =  ( 1 ^ 2 )  <->  ( abs `  A )  =  1 ) )
2314, 22bitr3d 248 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A ^ 2 )  =  1  <->  ( abs `  A
)  =  1 ) )
247, 23syl5bb 250 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( if ( ( A ^
2 )  =  1 ,  1 ,  0 )  =/=  0  <->  ( abs `  A )  =  1 ) )
25 oveq2 6091 . . . . 5  |-  ( N  =  0  ->  ( A  / L N )  =  ( A  / L 0 ) )
26 lgs0 21095 . . . . . 6  |-  ( A  e.  ZZ  ->  ( A  / L 0 )  =  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) )
2726adantr 453 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( A  / L
0 )  =  if ( ( A ^
2 )  =  1 ,  1 ,  0 ) )
2825, 27sylan9eqr 2492 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( A  / L N )  =  if ( ( A ^ 2 )  =  1 ,  1 ,  0 ) )
2928neeq1d 2616 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  / L N )  =/=  0  <->  if (
( A ^ 2 )  =  1 ,  1 ,  0 )  =/=  0 ) )
30 oveq2 6091 . . . . 5  |-  ( N  =  0  ->  ( A  gcd  N )  =  ( A  gcd  0
) )
31 gcdid0 13026 . . . . . 6  |-  ( A  e.  ZZ  ->  ( A  gcd  0 )  =  ( abs `  A
) )
3231adantr 453 . . . . 5  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( A  gcd  0
)  =  ( abs `  A ) )
3330, 32sylan9eqr 2492 . . . 4  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( A  gcd  N )  =  ( abs `  A ) )
3433eqeq1d 2446 . . 3  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  gcd  N )  =  1  <->  ( abs `  A
)  =  1 ) )
3524, 29, 343bitr4d 278 . 2  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =  0 )  ->  ( ( A  / L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
36 eqid 2438 . . . . . 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 21102 . . . . 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 2616 . . . 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 2611 . . . . . . 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 2611 . . . . . . 7  |-  ( 1  =  if ( ( N  <  0  /\  A  <  0 ) ,  -u 1 ,  1 )  ->  ( 1  =/=  0  <->  if (
( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  =/=  0 ) )
41 ax-1cn 9050 . . . . . . . 8  |-  1  e.  CC
4241, 4negne0i 9377 . . . . . . 7  |-  -u 1  =/=  0
4339, 40, 42, 4keephyp 3795 . . . . . 6  |-  if ( ( N  <  0  /\  A  <  0
) ,  -u 1 ,  1 )  =/=  0
4443biantrur 494 . . . . 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 10069 . . . . . . . 8  |-  -u 1  e.  CC
4645, 41keepel 3798 . . . . . . 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 12131 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  N  =/=  0 )  -> 
( abs `  N
)  e.  NN )
49483adant1 976 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( abs `  N )  e.  NN )
50 nnuz 10523 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
5149, 50syl6eleq 2528 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( abs `  N )  e.  ( ZZ>= `  1 )
)
5236lgsfcl3 21103 . . . . . . . . 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 11082 . . . . . . . . 9  |-  ( k  e.  ( 1 ... ( abs `  N
) )  ->  k  e.  NN )
54 ffvelrn 5870 . . . . . . . . 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 465 . . . . . . . 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 10378 . . . . . . 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 9076 . . . . . . . 8  |-  ( ( k  e.  CC  /\  x  e.  CC )  ->  ( k  x.  x
)  e.  CC )
5857adantl 454 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( k  e.  CC  /\  x  e.  CC ) )  ->  ( k  x.  x )  e.  CC )
5951, 56, 58seqcl 11345 . . . . . 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 9675 . . . . 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 251 . . . 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 449 . . . . . . . . . 10  |-  ( ( A  =  0  /\  N  =  0 )  ->  N  =  0 )
6362necon3ai 2646 . . . . . . . . 9  |-  ( N  =/=  0  ->  -.  ( A  =  0  /\  N  =  0
) )
64 gcdn0cl 13016 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  -.  ( A  =  0  /\  N  =  0 ) )  ->  ( A  gcd  N )  e.  NN )
6563, 64sylan2 462 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =/=  0
)  ->  ( A  gcd  N )  e.  NN )
66653impa 1149 . . . . . . 7  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  ( A  gcd  N )  e.  NN )
67 eluz2b3 10551 . . . . . . . . 9  |-  ( ( A  gcd  N )  e.  ( ZZ>= `  2
)  <->  ( ( A  gcd  N )  e.  NN  /\  ( A  gcd  N )  =/=  1 ) )
68 exprmfct 13112 . . . . . . . . 9  |-  ( ( A  gcd  N )  e.  ( ZZ>= `  2
)  ->  E. p  e.  Prime  p  ||  ( A  gcd  N ) )
6967, 68sylbir 206 . . . . . . . 8  |-  ( ( ( A  gcd  N
)  e.  NN  /\  ( A  gcd  N )  =/=  1 )  ->  E. p  e.  Prime  p 
||  ( A  gcd  N ) )
7057adantl 454 . . . . . . . . . 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 697 . . . . . . . . . 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 9246 . . . . . . . . . . 11  |-  ( k  e.  CC  ->  (
0  x.  k )  =  0 )
7372adantl 454 . . . . . . . . . 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 9247 . . . . . . . . . . 11  |-  ( k  e.  CC  ->  (
k  x.  0 )  =  0 )
7574adantl 454 . . . . . . . . . 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 735 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  ( A  gcd  N ) )
77 prmz 13085 . . . . . . . . . . . . . . . . 17  |-  ( p  e.  Prime  ->  p  e.  ZZ )
7877ad2antrl 710 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ZZ )
79 simpl1 961 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  A  e.  ZZ )
80 simpl2 962 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  N  e.  ZZ )
81 dvdsgcdb 13046 . . . . . . . . . . . . . . . 16  |-  ( ( p  e.  ZZ  /\  A  e.  ZZ  /\  N  e.  ZZ )  ->  (
( p  ||  A  /\  p  ||  N )  <-> 
p  ||  ( A  gcd  N ) ) )
8278, 79, 80, 81syl3anc 1185 . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  A  /\  p  ||  N ) )
8483simprd 451 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  N
)
85 dvdsabsb 12871 . . . . . . . . . . . . . 14  |-  ( ( p  e.  ZZ  /\  N  e.  ZZ )  ->  ( p  ||  N  <->  p 
||  ( abs `  N
) ) )
8678, 80, 85syl2anc 644 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  ||  N  <->  p  ||  ( abs `  N ) ) )
8784, 86mpbid 203 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  ( abs `  N ) )
8849adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( abs `  N )  e.  NN )
89 dvdsle 12897 . . . . . . . . . . . . 13  |-  ( ( p  e.  ZZ  /\  ( abs `  N )  e.  NN )  -> 
( p  ||  ( abs `  N )  ->  p  <_  ( abs `  N
) ) )
9078, 88, 89syl2anc 644 . . . . . . . . . . . 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 13084 . . . . . . . . . . . . . 14  |-  ( p  e.  Prime  ->  p  e.  NN )
9392ad2antrl 710 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  NN )
9493, 50syl6eleq 2528 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ( ZZ>= `  1 )
)
9588nnzd 10376 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( abs `  N )  e.  ZZ )
96 elfz5 11053 . . . . . . . . . . . 12  |-  ( ( p  e.  ( ZZ>= ` 
1 )  /\  ( abs `  N )  e.  ZZ )  ->  (
p  e.  ( 1 ... ( abs `  N
) )  <->  p  <_  ( abs `  N ) ) )
9794, 95, 96syl2anc 644 . . . . . . . . . . 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 225 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  ( 1 ... ( abs `  N ) ) )
99 eleq1 2498 . . . . . . . . . . . . . 14  |-  ( n  =  p  ->  (
n  e.  Prime  <->  p  e.  Prime ) )
100 oveq2 6091 . . . . . . . . . . . . . . 15  |-  ( n  =  p  ->  ( A  / L n )  =  ( A  / L p ) )
101 oveq1 6090 . . . . . . . . . . . . . . 15  |-  ( n  =  p  ->  (
n  pCnt  N )  =  ( p  pCnt  N ) )
102100, 101oveq12d 6101 . . . . . . . . . . . . . 14  |-  ( n  =  p  ->  (
( A  / L
n ) ^ (
n  pCnt  N )
)  =  ( ( A  / L p ) ^ ( p 
pCnt  N ) ) )
103 eqidd 2439 . . . . . . . . . . . . . 14  |-  ( n  =  p  ->  1  =  1 )
10499, 102, 103ifbieq12d 3763 . . . . . . . . . . . . 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 ) )
105 ovex 6108 . . . . . . . . . . . . . 14  |-  ( ( A  / L p ) ^ ( p 
pCnt  N ) )  e. 
_V
106 1ex 9088 . . . . . . . . . . . . . 14  |-  1  e.  _V
107105, 106ifex 3799 . . . . . . . . . . . . 13  |-  if ( p  e.  Prime ,  ( ( A  / L
p ) ^ (
p  pCnt  N )
) ,  1 )  e.  _V
108104, 36, 107fvmpt 5808 . . . . . . . . . . . 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 ) )
10993, 108syl 16 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( (
n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  / L n ) ^
( n  pCnt  N
) ) ,  1 ) ) `  p
)  =  if ( p  e.  Prime ,  ( ( A  / L
p ) ^ (
p  pCnt  N )
) ,  1 ) )
110 iftrue 3747 . . . . . . . . . . . 12  |-  ( p  e.  Prime  ->  if ( p  e.  Prime ,  ( ( A  / L
p ) ^ (
p  pCnt  N )
) ,  1 )  =  ( ( A  / L p ) ^ ( p  pCnt  N ) ) )
111110ad2antrl 710 . . . . . . . . . . 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 ) ) )
112 oveq2 6091 . . . . . . . . . . . . . . . 16  |-  ( p  =  2  ->  ( A  / L p )  =  ( A  / L 2 ) )
113 lgs2 21099 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  ZZ  ->  ( A  / L 2 )  =  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) )
11479, 113syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( A  / L 2 )  =  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) )
115112, 114sylan9eqr 2492 . . . . . . . . . . . . . . 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 ) ) )
116 simpr 449 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  p  =  2 )
11783simpld 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  ||  A
)
118117adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  p  ||  A
)
119116, 118eqbrtrrd 4236 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  2  ||  A
)
120 iftrue 3747 . . . . . . . . . . . . . . . 16  |-  ( 2 
||  A  ->  if ( 2  ||  A ,  0 ,  if ( ( A  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) )  =  0 )
121119, 120syl 16 . . . . . . . . . . . . . . 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 )
122115, 121eqtrd 2470 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =  2 )  ->  ( A  / L p )  =  0 )
123 simpll1 997 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  A  e.  ZZ )
124 simprl 734 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  p  e.  Prime )
125124adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  Prime )
126 simpr 449 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  =/=  2 )
127 eldifsn 3929 . . . . . . . . . . . . . . . . 17  |-  ( p  e.  ( Prime  \  {
2 } )  <->  ( p  e.  Prime  /\  p  =/=  2 ) )
128125, 126, 127sylanbrc 647 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  ( Prime  \  { 2 } ) )
129 lgsval3 21100 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ZZ  /\  p  e.  ( Prime  \  { 2 } ) )  ->  ( A  / L p )  =  ( ( ( ( A ^ ( ( p  -  1 )  /  2 ) )  +  1 )  mod  p )  -  1 ) )
130123, 128, 129syl2anc 644 . . . . . . . . . . . . . . 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 ) )
131 oddprm 13191 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  e.  ( Prime  \  {
2 } )  -> 
( ( p  - 
1 )  /  2
)  e.  NN )
132128, 131syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( p  - 
1 )  /  2
)  e.  NN )
133132nnnn0d 10276 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( ( p  - 
1 )  /  2
)  e.  NN0 )
134 zexpcl 11398 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  ZZ  /\  ( ( p  - 
1 )  /  2
)  e.  NN0 )  ->  ( A ^ (
( p  -  1 )  /  2 ) )  e.  ZZ )
135123, 133, 134syl2anc 644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A ^ (
( p  -  1 )  /  2 ) )  e.  ZZ )
136135zred 10377 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 9093 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  RR
138137a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
0  e.  RR )
13918a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
1  e.  RR )
140125, 92syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  NN )
141140nnrpd 10649 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  RR+ )
142 0z 10295 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ZZ
143142a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
0  e.  ZZ )
144117adantr 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  ||  A )
145 dvdsval3 12858 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( p  e.  NN  /\  A  e.  ZZ )  ->  ( p  ||  A  <->  ( A  mod  p )  =  0 ) )
146140, 123, 145syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 203 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  mod  p
)  =  0 )
148 0mod 11274 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  e.  RR+  ->  ( 0  mod  p )  =  0 )
149141, 148syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 0  mod  p
)  =  0 )
150147, 149eqtr4d 2473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 11516 . . . . . . . . . . . . . . . . . . . . . 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 ) )
152123, 143, 133, 141, 150, 151syl221anc 1196 . . . . . . . . . . . . . . . . . . . . 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 ) )
1531320expd 11541 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 0 ^ (
( p  -  1 )  /  2 ) )  =  0 )
154153oveq1d 6098 . . . . . . . . . . . . . . . . . . . . 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 ) )
155152, 154eqtrd 2470 . . . . . . . . . . . . . . . . . . . 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 ) )
156 modadd1 11280 . . . . . . . . . . . . . . . . . . . 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 ) )
157136, 138, 139, 141, 155, 156syl221anc 1196 . . . . . . . . . . . . . . . . . . 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 ) )
158 0p1e1 10095 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  +  1 )  =  1
159158oveq1i 6093 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  +  1 )  mod  p )  =  ( 1  mod  p
)
160157, 159syl6eq 2486 . . . . . . . . . . . . . . . . . 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 ) )
161140nnred 10017 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  RR )
162 prmuz2 13099 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  e.  Prime  ->  p  e.  ( ZZ>= `  2 )
)
163125, 162syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  ->  p  e.  ( ZZ>= ` 
2 ) )
164 eluz2b2 10550 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  e.  ( ZZ>= `  2
)  <->  ( p  e.  NN  /\  1  < 
p ) )
165163, 164sylib 190 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( p  e.  NN  /\  1  <  p ) )
166165simprd 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
1  <  p )
167 1mod 11275 . . . . . . . . . . . . . . . . . . 19  |-  ( ( p  e.  RR  /\  1  <  p )  -> 
( 1  mod  p
)  =  1 )
168161, 166, 167syl2anc 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( 1  mod  p
)  =  1 )
169160, 168eqtrd 2470 . . . . . . . . . . . . . . . . 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 )
170169oveq1d 6098 . . . . . . . . . . . . . . . 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 ) )
171 1m1e0 10070 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
172170, 171syl6eq 2486 . . . . . . . . . . . . . . 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 )
173130, 172eqtrd 2470 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  (
p  e.  Prime  /\  p  ||  ( A  gcd  N
) ) )  /\  p  =/=  2 )  -> 
( A  / L
p )  =  0 )
174122, 173pm2.61dane 2684 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( A  / L p )  =  0 )
175174oveq1d 6098 . . . . . . . . . . . 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 ) ) )
176 zq 10582 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ZZ  ->  N  e.  QQ )
17780, 176syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  N  e.  QQ )
178 pcabs 13250 . . . . . . . . . . . . . . 15  |-  ( ( p  e.  Prime  /\  N  e.  QQ )  ->  (
p  pCnt  ( abs `  N ) )  =  ( p  pCnt  N
) )
179124, 177, 178syl2anc 644 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  ( abs `  N
) )  =  ( p  pCnt  N )
)
180 pcelnn 13245 . . . . . . . . . . . . . . . 16  |-  ( ( p  e.  Prime  /\  ( abs `  N )  e.  NN )  ->  (
( p  pCnt  ( abs `  N ) )  e.  NN  <->  p  ||  ( abs `  N ) ) )
181124, 88, 180syl2anc 644 . . . . . . . . . . . . . . 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 ) ) )
18287, 181mpbird 225 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  ( abs `  N
) )  e.  NN )
183179, 182eqeltrrd 2513 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( p  pCnt  N )  e.  NN )
1841830expd 11541 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( p  e.  Prime  /\  p  ||  ( A  gcd  N ) ) )  ->  ( 0 ^ ( p  pCnt  N ) )  =  0 )
185175, 184eqtrd 2470 . . . . . . . . . . 11  |-  ( ( ( 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 2474 . . . . . . . . . 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 )
18770, 71, 73, 75, 98, 88, 186seqz 11373 . . . . . . . . 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 )
188187rexlimdvaa 2833 . . . . . . . 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 ) )
18969, 188syl5 31 . . . . . . 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 ) )
19066, 189mpand 658 . . . . . 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 ) )
191190necon1d 2675 . . . . 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 ) )
19251adantr 453 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  -> 
( abs `  N
)  e.  ( ZZ>= ` 
1 ) )
19353adantl 454 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  ( 1 ... ( abs `  N ) ) )  ->  k  e.  NN )
194 eleq1 2498 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
n  e.  Prime  <->  k  e.  Prime ) )
195 oveq2 6091 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  ( A  / L n )  =  ( A  / L k ) )
196 oveq1 6090 . . . . . . . . . . . . 13  |-  ( n  =  k  ->  (
n  pCnt  N )  =  ( k  pCnt  N ) )
197195, 196oveq12d 6101 . . . . . . . . . . . 12  |-  ( n  =  k  ->  (
( A  / L
n ) ^ (
n  pCnt  N )
)  =  ( ( A  / L k ) ^ ( k 
pCnt  N ) ) )
198 eqidd 2439 . . . . . . . . . . . 12  |-  ( n  =  k  ->  1  =  1 )
199194, 197, 198ifbieq12d 3763 . . . . . . . . . . 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 ) )
200 ovex 6108 . . . . . . . . . . . 12  |-  ( ( A  / L k ) ^ ( k 
pCnt  N ) )  e. 
_V
201200, 106ifex 3799 . . . . . . . . . . 11  |-  if ( k  e.  Prime ,  ( ( A  / L
k ) ^ (
k  pCnt  N )
) ,  1 )  e.  _V
202199, 36, 201fvmpt 5808 . . . . . . . . . 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 ) )
203193, 202syl 16 . . . . . . . . 9  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  ( 1 ... ( abs `  N ) ) )  ->  ( (
n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  / L n ) ^
( n  pCnt  N
) ) ,  1 ) ) `  k
)  =  if ( k  e.  Prime ,  ( ( A  / L
k ) ^ (
k  pCnt  N )
) ,  1 ) )
204 simpll1 997 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  A  e.  ZZ )
205 prmz 13085 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  Prime  ->  k  e.  ZZ )
206205adantl 454 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  ZZ )
207 lgscl 21096 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ZZ  /\  k  e.  ZZ )  ->  ( A  / L
k )  e.  ZZ )
208204, 206, 207syl2anc 644 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  / L k )  e.  ZZ )
209208zcnd 10378 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  / L k )  e.  CC )
210209adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  ( A  / L k )  e.  CC )
211 oveq2 6091 . . . . . . . . . . . . . . . . 17  |-  ( k  =  2  ->  ( A  / L k )  =  ( A  / L 2 ) )
212204adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  A  e.  ZZ )
213212, 113syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  ( A  / L 2 )  =  if ( 2 
||  A ,  0 ,  if ( ( A  mod  8 )  e.  { 1 ,  7 } ,  1 ,  -u 1 ) ) )
214211, 213sylan9eqr 2492 . . . . . . . . . . . . . . . 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 ) ) )
215 nprmdvds1 13113 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  Prime  ->  -.  k  ||  1 )
216215adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  -.  k  ||  1 )
217 simpll2 998 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  e.  ZZ )
218 dvdsgcdb 13046 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( k  e.  ZZ  /\  A  e.  ZZ  /\  N  e.  ZZ )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  ( A  gcd  N ) ) )
219206, 204, 217, 218syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  ( A  gcd  N ) ) )
220 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( A  gcd  N )  =  1 )
221220breq2d 4226 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  ( A  gcd  N )  <->  k  ||  1 ) )
222219, 221bitrd 246 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  ||  A  /\  k  ||  N )  <-> 
k  ||  1 ) )
223216, 222mtbird 294 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  -.  ( k  ||  A  /\  k  ||  N ) )
224 imnan 413 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  ||  A  ->  -.  k  ||  N )  <->  -.  ( k  ||  A  /\  k  ||  N ) )
225223, 224sylibr 205 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  A  ->  -.  k  ||  N ) )
226225con2d 110 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  N  ->  -.  k  ||  A ) )
227226imp 420 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  -.  k  ||  A )
228 breq1 4217 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  2  ->  (
k  ||  A  <->  2  ||  A ) )
229228notbid 287 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  2  ->  ( -.  k  ||  A  <->  -.  2  ||  A ) )
230227, 229syl5ibcom 213 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  (
k  =  2  ->  -.  2  ||  A ) )
231230imp 420 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  ->  -.  2  ||  A )
232 iffalse 3748 . . . . . . . . . . . . . . . . 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 ) )
233231, 232syl 16 . . . . . . . . . . . . . . . 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 ) )
234214, 233eqtrd 2470 . . . . . . . . . . . . . . 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 ) )
235 neeq1 2611 . . . . . . . . . . . . . . . . 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
) )
236 neeq1 2611 . . . . . . . . . . . . . . . . 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 ) )
237235, 236, 4, 42keephyp 3795 . . . . . . . . . . . . . . . 16  |-  if ( ( A  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
)  =/=  0
238237a1i 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
)
239234, 238eqnetrd 2621 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =  2 )  -> 
( A  / L
k )  =/=  0
)
240 simpr 449 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  Prime )
241240ad2antrr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  Prime )
242241, 215syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  -.  k  ||  1 )
243 simplr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  ||  N )
244241, 205syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  ZZ )
245212adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  A  e.  ZZ )
246 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  =/=  2 )
247 eldifsn 3929 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ( Prime  \  {
2 } )  <->  ( k  e.  Prime  /\  k  =/=  2 ) )
248241, 246, 247sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  ( Prime  \  { 2 } ) )
249 oddprm 13191 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  ( Prime  \  {
2 } )  -> 
( ( k  - 
1 )  /  2
)  e.  NN )
250248, 249syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
( k  -  1 )  /  2 )  e.  NN )
251250nnnn0d 10276 . . . . . . . . . . . . . . . . . . . . . 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 )
252 zexpcl 11398 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  ZZ  /\  ( ( k  - 
1 )  /  2
)  e.  NN0 )  ->  ( A ^ (
( k  -  1 )  /  2 ) )  e.  ZZ )
253245, 251, 252syl2anc 644 . . . . . . . . . . . . . . . . . . . . 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 )
254217ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  N  e.  ZZ )
255 dvdsgcd 13045 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
256244, 253, 254, 255syl3anc 1185 . . . . . . . . . . . . . . . . . . . 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 ) ) )
257243, 256mpan2d 657 . . . . . . . . . . . . . . . . . . 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 ) ) )
258245zcnd 10378 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  A  e.  CC )
259258, 251absexpd 12256 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
260259oveq1d 6098 . . . . . . . . . . . . . . . . . . . . 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
) ) )
261 gcdabs 13035 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A ^ (
( k  -  1 )  /  2 ) )  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( abs `  ( A ^ ( ( k  -  1 )  / 
2 ) ) )  gcd  ( abs `  N
) )  =  ( ( A ^ (
( k  -  1 )  /  2 ) )  gcd  N ) )
262253, 254, 261syl2anc 644 . . . . . . . . . . . . . . . . . . . . 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 ) )
263 gcdabs 13035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( abs `  A
)  gcd  ( abs `  N ) )  =  ( A  gcd  N
) )
264245, 254, 263syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . 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
) )
265220ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A  gcd  N )  =  1 )
266264, 265eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . 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 )
267227adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  -.  k  ||  A )
268 dvds0 12867 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  e.  ZZ  ->  k  ||  0 )
269244, 268syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  ||  0 )
270 breq2 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  =  0  ->  (
k  ||  A  <->  k  ||  0 ) )
271269, 270syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A  =  0  ->  k 
||  A ) )
272271necon3bd 2640 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( -.  k  ||  A  ->  A  =/=  0 ) )
273267, 272mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  A  =/=  0 )
274 nnabscl 12131 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  ZZ  /\  A  =/=  0 )  -> 
( abs `  A
)  e.  NN )
275245, 273, 274syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( abs `  A )  e.  NN )
276 simpll3 999 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  =/=  0 )
277217, 276, 48syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( abs `  N )  e.  NN )
278277ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( abs `  N )  e.  NN )
279 rplpwr 13058 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
280275, 278, 250, 279syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . 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 ) )
281266, 280mpd 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 )
282260, 262, 2813eqtr3d 2478 . . . . . . . . . . . . . . . . . . . 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 )
283282breq2d 4226 . . . . . . . . . . . . . . . . . . 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 ) )
284257, 283sylibd 207 . . . . . . . . . . . . . . . . . 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 ) )
285242, 284mtod 171 . . . . . . . . . . . . . . . . 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
) ) )
286 prmnn 13084 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  Prime  ->  k  e.  NN )
287286adantl 454 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  k  e.  NN )
288287ad2antrr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  NN )
289 dvdsval3 12858 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  ( A ^ ( ( k  -  1 )  /  2 ) )  e.  ZZ )  -> 
( k  ||  ( A ^ ( ( k  -  1 )  / 
2 ) )  <->  ( ( A ^ ( ( k  -  1 )  / 
2 ) )  mod  k )  =  0 ) )
290288, 253, 289syl2anc 644 . . . . . . . . . . . . . . . . . 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 ) )
291290necon3bbid 2637 . . . . . . . . . . . . . . . . 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
) )
292285, 291mpbid 203 . . . . . . . . . . . . . . . 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 )
293 lgsvalmod 21101 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ZZ  /\  k  e.  ( Prime  \  { 2 } ) )  ->  ( ( A  / L k )  mod  k )  =  ( ( A ^
( ( k  - 
1 )  /  2
) )  mod  k
) )
294245, 248, 293syl2anc 644 . . . . . . . . . . . . . . . 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 ) )
295288nnrpd 10649 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  k  e.  RR+ )
296 0mod 11274 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  RR+  ->  ( 0  mod  k )  =  0 )
297295, 296syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  (
0  mod  k )  =  0 )
298292, 294, 2973netr4d 2630 . . . . . . . . . . . . . . 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 ) )
299 oveq1 6090 . . . . . . . . . . . . . . . 16  |-  ( ( A  / L k )  =  0  -> 
( ( A  / L k )  mod  k )  =  ( 0  mod  k ) )
300299necon3i 2645 . . . . . . . . . . . . . . 15  |-  ( ( ( A  / L
k )  mod  k
)  =/=  ( 0  mod  k )  -> 
( A  / L
k )  =/=  0
)
301298, 300syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  /\  k  =/=  2 )  ->  ( A  / L k )  =/=  0 )
302239, 301pm2.61dane 2684 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  ( A  / L k )  =/=  0 )
303 pczcl 13224 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  Prime  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( k  pCnt  N
)  e.  NN0 )
304240, 217, 276, 303syl12anc 1183 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  N )  e.  NN0 )
305304nn0zd 10375 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  N )  e.  ZZ )
306305adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  k  ||  N )  ->  (
k  pCnt  N )  e.  ZZ )
307 expclz 11408 . . . . . . . . . . . . . 14  |-  ( ( ( A  / L
k )  e.  CC  /\  ( A  / L
k )  =/=  0  /\  ( k  pCnt  N
)  e.  ZZ )  ->  ( ( A  / L k ) ^ ( k  pCnt  N ) )  e.  CC )
308 expne0i 11414 . . . . . . . . . . . . . 14  |-  ( ( ( A  / L
k )  e.  CC  /\  ( A  / L
k )  =/=  0  /\  ( k  pCnt  N
)  e.  ZZ )  ->  ( ( A  / L k ) ^ ( k  pCnt  N ) )  =/=  0
)
309 neeq1 2611 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( A  / L k ) ^ ( k  pCnt  N ) )  ->  (
x  =/=  0  <->  (
( A  / L
k ) ^ (
k  pCnt  N )
)  =/=  0 ) )
310309elrab 3094 . . . . . . . . . . . . . 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
) )
311307, 308, 310sylanbrc 647 . . . . . . . . . . . . 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 } )
312210, 302, 306, 311syl3anc 1185 . . . . . . . . . . . 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 } )
313 dvdsabsb 12871 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ZZ  /\  N  e.  ZZ )  ->  ( k  ||  N  <->  k 
||  ( abs `  N
) ) )
314206, 217, 313syl2anc 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  ||  N  <->  k  ||  ( abs `  N ) ) )
315314notbid 287 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  ( -.  k  ||  N  <->  -.  k  ||  ( abs `  N
) ) )
316 pceq0 13246 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  Prime  /\  ( abs `  N )  e.  NN )  ->  (
( k  pCnt  ( abs `  N ) )  =  0  <->  -.  k  ||  ( abs `  N
) ) )
317240, 277, 316syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  pCnt  ( abs `  N ) )  =  0  <->  -.  k  ||  ( abs `  N
) ) )
318217, 176syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  N  e.  QQ )
319 pcabs 13250 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  Prime  /\  N  e.  QQ )  ->  (
k  pCnt  ( abs `  N ) )  =  ( k  pCnt  N
) )
320240, 318, 319syl2anc 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
k  pCnt  ( abs `  N ) )  =  ( k  pCnt  N
) )
321320eqeq1d 2446 . . . . . . . . . . . . . . . . 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 ) )
322315, 317, 3213bitr2rd 275 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  ->  (
( k  pCnt  N
)  =  0  <->  -.  k  ||  N ) )
323322biimpar 473 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( k  pCnt  N
)  =  0 )
324323oveq2d 6099 . . . . . . . . . . . . . 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 ) )
325209adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( A  / L
k )  e.  CC )
326325exp0d 11519 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  k  e.  Prime )  /\  -.  k  ||  N )  -> 
( ( A  / L k ) ^
0 )  =  1 )
327324, 326eqtrd 2470 . . . . . . . . . . . . 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 )
328 neeq1 2611 . . . . . . . . . . . . . . 15  |-  ( x  =  1  ->  (
x  =/=  0  <->  1  =/=  0 ) )
329328elrab 3094 . . . . . . . . . . . . . 14  |-  ( 1  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( 1  e.  CC  /\  1  =/=  0 ) )
33041, 4, 329mpbir2an 888 . . . . . . . . . . . . 13  |-  1  e.  { x  e.  CC  |  x  =/=  0 }
331327, 330syl6eqel 2526 . . . . . . . . . . . 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 } )
332312, 331pm2.61dan 768 . . . . . . . . . . 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 } )
333330a1i 11 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  /\  -.  k  e.  Prime )  -> 
1  e.  { x  e.  CC  |  x  =/=  0 } )
334332, 333ifclda 3768 . . . . . . . . . 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 } )
335334adantr 453 . . . . . . . . 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 } )
336203, 335eqeltrd 2512 . . . . . . . 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 } )
337 neeq1 2611 . . . . . . . . . . . 12  |-  ( x  =  k  ->  (
x  =/=  0  <->  k  =/=  0 ) )
338337elrab 3094 . . . . . . . . . . 11  |-  ( k  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( k  e.  CC  /\  k  =/=  0 ) )
339 neeq1 2611 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
x  =/=  0  <->  y  =/=  0 ) )
340339elrab 3094 . . . . . . . . . . 11  |-  ( y  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( y  e.  CC  /\  y  =/=  0 ) )
341 mulcl 9076 . . . . . . . . . . . . 13  |-  ( ( k  e.  CC  /\  y  e.  CC )  ->  ( k  x.  y
)  e.  CC )
342341ad2ant2r 729 . . . . . . . . . . . 12  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( k  x.  y
)  e.  CC )
343 mulne0 9666 . . . . . . . . . . . 12  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( k  x.  y
)  =/=  0 )
344342, 343jca 520 . . . . . . . . . . 11  |-  ( ( ( k  e.  CC  /\  k  =/=  0 )  /\  ( y  e.  CC  /\  y  =/=  0 ) )  -> 
( ( k  x.  y )  e.  CC  /\  ( k  x.  y
)  =/=  0 ) )
345338, 340, 344syl2anb 467 . . . . . . . . . 10  |-  ( ( k  e.  { x  e.  CC  |  x  =/=  0 }  /\  y  e.  { x  e.  CC  |  x  =/=  0 } )  ->  (
( k  x.  y
)  e.  CC  /\  ( k  x.  y
)  =/=  0 ) )
346 neeq1 2611 . . . . . . . . . . 11  |-  ( x  =  ( k  x.  y )  ->  (
x  =/=  0  <->  (
k  x.  y )  =/=  0 ) )
347346elrab 3094 . . . . . . . . . 10  |-  ( ( k  x.  y )  e.  { x  e.  CC  |  x  =/=  0 }  <->  ( (
k  x.  y )  e.  CC  /\  (
k  x.  y )  =/=  0 ) )
348345, 347sylibr 205 . . . . . . . . 9  |-  ( ( k  e.  { x  e.  CC  |  x  =/=  0 }  /\  y  e.  { x  e.  CC  |  x  =/=  0 } )  ->  (
k  x.  y )  e.  { x  e.  CC  |  x  =/=  0 } )
349348adantl 454 . . . . . . . 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 } )
350192, 336, 349seqcl 11345 . . . . . . 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 } )
351 neeq1 2611 . . . . . . . . 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 ) )
352351elrab 3094 . . . . . . . 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
) )
353352simprbi 452 . . . . . . 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
)
354350, 353syl 16 . . . . . 6  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  /\  ( A  gcd  N )  =  1 )  -> 
(  seq  1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( ( A  / L
n ) ^ (
n  pCnt  N )
) ,  1 ) ) ) `  ( abs `  N ) )  =/=  0 )
355354ex 425 . . . . 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 ) )
356191, 355impbid 185 . . . 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 ) )
35738, 61, 3563bitrd 272 . . 3  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ  /\  N  =/=  0 )  ->  (
( A  / L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
3583573expa 1154 . 2  |-  ( ( ( A  e.  ZZ  /\  N  e.  ZZ )  /\  N  =/=  0
)  ->  ( ( A  / L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
35935, 358pm2.61dane 2684 1  |-  ( ( A  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( A  / L N )  =/=  0  <->  ( A  gcd  N )  =  1 ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937    = wceq 1653    e. wcel 1726    =/= wne 2601   E.wrex 2708   {crab 2711    \ cdif 3319   ifcif 3741   {csn 3816   {cpr 3817   class class class wbr 4214    e. cmpt 4268