Metamath Proof Explorer

Theorem lgsne0

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)

Ref Expression
Assertion lgsne0 
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( ( A /L N ) =/= 0 <-> ( A gcd N ) = 1 ) )

Proof

Step Hyp Ref Expression
1 iffalse 
 |-  ( -. ( A ^ 2 ) = 1 -> if ( ( A ^ 2 ) = 1 , 1 , 0 ) = 0 )
2 1 necon1ai 
 |-  ( if ( ( A ^ 2 ) = 1 , 1 , 0 ) =/= 0 -> ( A ^ 2 ) = 1 )
3 iftrue 
 |-  ( ( A ^ 2 ) = 1 -> if ( ( A ^ 2 ) = 1 , 1 , 0 ) = 1 )
4 ax-1ne0 
 |-  1 =/= 0
5 4 a1i 
 |-  ( ( A ^ 2 ) = 1 -> 1 =/= 0 )
6 3 5 eqnetrd 
 |-  ( ( A ^ 2 ) = 1 -> if ( ( A ^ 2 ) = 1 , 1 , 0 ) =/= 0 )
7 2 6 impbii 
 |-  ( if ( ( A ^ 2 ) = 1 , 1 , 0 ) =/= 0 <-> ( A ^ 2 ) = 1 )
8 zre 
 |-  ( A e. ZZ -> A e. RR )
9 8 ad2antrr 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> A e. RR )
10 absresq 
 |-  ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
11 9 10 syl 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
12 sq1 
 |-  ( 1 ^ 2 ) = 1
13 12 a1i 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( 1 ^ 2 ) = 1 )
14 11 13 eqeq12d 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( ( ( abs ` A ) ^ 2 ) = ( 1 ^ 2 ) <-> ( A ^ 2 ) = 1 ) )
15 9 recnd 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> A e. CC )
16 15 abscld 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( abs ` A ) e. RR )
17 15 absge0d 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> 0 <_ ( abs ` A ) )
18 1re 
 |-  1 e. RR
19 0le1 
 |-  0 <_ 1
20 sq11 
 |-  ( ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( ( abs ` A ) ^ 2 ) = ( 1 ^ 2 ) <-> ( abs ` A ) = 1 ) )
21 18 19 20 mpanr12 
 |-  ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) -> ( ( ( abs ` A ) ^ 2 ) = ( 1 ^ 2 ) <-> ( abs ` A ) = 1 ) )
22 16 17 21 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( ( ( abs ` A ) ^ 2 ) = ( 1 ^ 2 ) <-> ( abs ` A ) = 1 ) )
23 14 22 bitr3d 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( ( A ^ 2 ) = 1 <-> ( abs ` A ) = 1 ) )
24 7 23 syl5bb 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( if ( ( A ^ 2 ) = 1 , 1 , 0 ) =/= 0 <-> ( abs ` A ) = 1 ) )
25 oveq2 
 |-  ( N = 0 -> ( A /L N ) = ( A /L 0 ) )
26 lgs0 
 |-  ( A e. ZZ -> ( A /L 0 ) = if ( ( A ^ 2 ) = 1 , 1 , 0 ) )
27 26 adantr 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L 0 ) = if ( ( A ^ 2 ) = 1 , 1 , 0 ) )
28 25 27 sylan9eqr 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( A /L N ) = if ( ( A ^ 2 ) = 1 , 1 , 0 ) )
29 28 neeq1d 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( ( A /L N ) =/= 0 <-> if ( ( A ^ 2 ) = 1 , 1 , 0 ) =/= 0 ) )
30 oveq2 
 |-  ( N = 0 -> ( A gcd N ) = ( A gcd 0 ) )
31 gcdid0 
 |-  ( A e. ZZ -> ( A gcd 0 ) = ( abs ` A ) )
32 31 adantr 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A gcd 0 ) = ( abs ` A ) )
33 30 32 sylan9eqr 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( A gcd N ) = ( abs ` A ) )
34 33 eqeq1d 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( ( A gcd N ) = 1 <-> ( abs ` A ) = 1 ) )
35 24 29 34 3bitr4d 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( ( A /L N ) =/= 0 <-> ( A gcd N ) = 1 ) )
36 eqid 
 |-  ( 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 ) )
37 36 lgsval4 
 |-  ( ( 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 ) ) ) )
38 37 neeq1d 
 |-  ( ( 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 
 |-  ( -u 1 = if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) -> ( -u 1 =/= 0 <-> if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) =/= 0 ) )
40 neeq1 
 |-  ( 1 = if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) -> ( 1 =/= 0 <-> if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) =/= 0 ) )
41 neg1ne0 
 |-  -u 1 =/= 0
42 39 40 41 4 keephyp 
 |-  if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) =/= 0
43 42 biantrur 
 |-  ( ( 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 
 |-  -u 1 e. CC
45 ax-1cn 
 |-  1 e. CC
46 44 45 ifcli 
 |-  if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) e. CC
47 46 a1i 
 |-  ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) e. CC )
48 nnabscl 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN )
49 48 3adant1 
 |-  ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN )
50 nnuz 
 |-  NN = ( ZZ>= ` 1 )
51 49 50 eleqtrdi 
 |-  ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. ( ZZ>= ` 1 ) )
52 36 lgsfcl3 
 |-  ( ( 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 
 |-  ( k e. ( 1 ... ( abs ` N ) ) -> k e. NN )
54 ffvelrn 
 |-  ( ( ( 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 )
55 52 53 54 syl2an 
 |-  ( ( ( 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 )
56 55 zcnd 
 |-  ( ( ( 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 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
58 57 adantl 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
59 51 56 58 seqcl 
 |-  ( ( 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 )
60 47 59 mulne0bd 
 |-  ( ( 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 ) )
61 43 60 syl5rbb 
 |-  ( ( 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 gcd2n0cl 
 |-  ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( A gcd N ) e. NN )
63 eluz2b3 
 |-  ( ( A gcd N ) e. ( ZZ>= ` 2 ) <-> ( ( A gcd N ) e. NN /\ ( A gcd N ) =/= 1 ) )
64 exprmfct 
 |-  ( ( A gcd N ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( A gcd N ) )
65 63 64 sylbir 
 |-  ( ( ( A gcd N ) e. NN /\ ( A gcd N ) =/= 1 ) -> E. p e. Prime p || ( A gcd N ) )
66 57 adantl 
 |-  ( ( ( ( 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 )
67 56 adantlr 
 |-  ( ( ( ( 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 )
68 mul02 
 |-  ( k e. CC -> ( 0 x. k ) = 0 )
69 68 adantl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ k e. CC ) -> ( 0 x. k ) = 0 )
70 mul01 
 |-  ( k e. CC -> ( k x. 0 ) = 0 )
71 70 adantl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ k e. CC ) -> ( k x. 0 ) = 0 )
72 simprr 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p || ( A gcd N ) )
73 prmz 
 |-  ( p e. Prime -> p e. ZZ )
74 73 ad2antrl 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p e. ZZ )
75 simpl1 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> A e. ZZ )
76 simpl2 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> N e. ZZ )
77 dvdsgcdb 
 |-  ( ( p e. ZZ /\ A e. ZZ /\ N e. ZZ ) -> ( ( p || A /\ p || N ) <-> p || ( A gcd N ) ) )
78 74 75 76 77 syl3anc 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( ( p || A /\ p || N ) <-> p || ( A gcd N ) ) )
79 72 78 mpbird 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( p || A /\ p || N ) )
80 79 simprd 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p || N )
81 dvdsabsb 
 |-  ( ( p e. ZZ /\ N e. ZZ ) -> ( p || N <-> p || ( abs ` N ) ) )
82 74 76 81 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( p || N <-> p || ( abs ` N ) ) )
83 80 82 mpbid 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p || ( abs ` N ) )
84 49 adantr 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( abs ` N ) e. NN )
85 dvdsle 
 |-  ( ( p e. ZZ /\ ( abs ` N ) e. NN ) -> ( p || ( abs ` N ) -> p <_ ( abs ` N ) ) )
86 74 84 85 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( p || ( abs ` N ) -> p <_ ( abs ` N ) ) )
87 83 86 mpd 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p <_ ( abs ` N ) )
88 prmnn 
 |-  ( p e. Prime -> p e. NN )
89 88 ad2antrl 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p e. NN )
90 89 50 eleqtrdi 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p e. ( ZZ>= ` 1 ) )
91 84 nnzd 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( abs ` N ) e. ZZ )
92 elfz5 
 |-  ( ( p e. ( ZZ>= ` 1 ) /\ ( abs ` N ) e. ZZ ) -> ( p e. ( 1 ... ( abs ` N ) ) <-> p <_ ( abs ` N ) ) )
93 90 91 92 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( p e. ( 1 ... ( abs ` N ) ) <-> p <_ ( abs ` N ) ) )
94 87 93 mpbird 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p e. ( 1 ... ( abs ` N ) ) )
95 eleq1w 
 |-  ( n = p -> ( n e. Prime <-> p e. Prime ) )
96 oveq2 
 |-  ( n = p -> ( A /L n ) = ( A /L p ) )
97 oveq1 
 |-  ( n = p -> ( n pCnt N ) = ( p pCnt N ) )
98 96 97 oveq12d 
 |-  ( n = p -> ( ( A /L n ) ^ ( n pCnt N ) ) = ( ( A /L p ) ^ ( p pCnt N ) ) )
99 95 98 ifbieq1d 
 |-  ( n = p -> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) = if ( p e. Prime , ( ( A /L p ) ^ ( p pCnt N ) ) , 1 ) )
100 ovex 
 |-  ( ( A /L p ) ^ ( p pCnt N ) ) e. _V
101 1ex 
 |-  1 e. _V
102 100 101 ifex 
 |-  if ( p e. Prime , ( ( A /L p ) ^ ( p pCnt N ) ) , 1 ) e. _V
103 99 36 102 fvmpt 
 |-  ( 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 ) )
104 89 103 syl 
 |-  ( ( ( 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 ) )
105 iftrue 
 |-  ( p e. Prime -> if ( p e. Prime , ( ( A /L p ) ^ ( p pCnt N ) ) , 1 ) = ( ( A /L p ) ^ ( p pCnt N ) ) )
106 105 ad2antrl 
 |-  ( ( ( 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 ) ) )
107 oveq2 
 |-  ( p = 2 -> ( A /L p ) = ( A /L 2 ) )
108 lgs2 
 |-  ( A e. ZZ -> ( A /L 2 ) = if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) )
109 75 108 syl 
 |-  ( ( ( 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 ) ) )
110 107 109 sylan9eqr 
 |-  ( ( ( ( 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 ) ) )
111 simpr 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p = 2 ) -> p = 2 )
112 79 simpld 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p || A )
113 112 adantr 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p = 2 ) -> p || A )
114 111 113 eqbrtrrd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p = 2 ) -> 2 || A )
115 114 iftrued 
 |-  ( ( ( ( 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 )
116 110 115 eqtrd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p = 2 ) -> ( A /L p ) = 0 )
117 simpll1 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> A e. ZZ )
118 simprl 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> p e. Prime )
119 118 adantr 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> p e. Prime )
120 simpr 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> p =/= 2 )
121 eldifsn 
 |-  ( p e. ( Prime \ { 2 } ) <-> ( p e. Prime /\ p =/= 2 ) )
122 119 120 121 sylanbrc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> p e. ( Prime \ { 2 } ) )
123 lgsval3 
 |-  ( ( A e. ZZ /\ p e. ( Prime \ { 2 } ) ) -> ( A /L p ) = ( ( ( ( A ^ ( ( p - 1 ) / 2 ) ) + 1 ) mod p ) - 1 ) )
124 117 122 123 syl2anc 
 |-  ( ( ( ( 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 ) )
125 oddprm 
 |-  ( p e. ( Prime \ { 2 } ) -> ( ( p - 1 ) / 2 ) e. NN )
126 122 125 syl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( ( p - 1 ) / 2 ) e. NN )
127 126 nnnn0d 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( ( p - 1 ) / 2 ) e. NN0 )
128 zexpcl 
 |-  ( ( A e. ZZ /\ ( ( p - 1 ) / 2 ) e. NN0 ) -> ( A ^ ( ( p - 1 ) / 2 ) ) e. ZZ )
129 117 127 128 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( A ^ ( ( p - 1 ) / 2 ) ) e. ZZ )
130 129 zred 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( A ^ ( ( p - 1 ) / 2 ) ) e. RR )
131 0red 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> 0 e. RR )
132 18 a1i 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> 1 e. RR )
133 119 88 syl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> p e. NN )
134 133 nnrpd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> p e. RR+ )
135 0zd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> 0 e. ZZ )
136 112 adantr 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> p || A )
137 dvdsval3 
 |-  ( ( p e. NN /\ A e. ZZ ) -> ( p || A <-> ( A mod p ) = 0 ) )
138 133 117 137 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( p || A <-> ( A mod p ) = 0 ) )
139 136 138 mpbid 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( A mod p ) = 0 )
140 0mod 
 |-  ( p e. RR+ -> ( 0 mod p ) = 0 )
141 134 140 syl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( 0 mod p ) = 0 )
142 139 141 eqtr4d 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( A mod p ) = ( 0 mod p ) )
143 modexp 
 |-  ( ( ( 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 ) )
144 117 135 127 134 142 143 syl221anc 
 |-  ( ( ( ( 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 ) )
145 126 0expd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( 0 ^ ( ( p - 1 ) / 2 ) ) = 0 )
146 145 oveq1d 
 |-  ( ( ( ( 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 ) )
147 144 146 eqtrd 
 |-  ( ( ( ( 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 ) )
148 modadd1 
 |-  ( ( ( ( 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 ) )
149 130 131 132 134 147 148 syl221anc 
 |-  ( ( ( ( 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 ) )
150 0p1e1 
 |-  ( 0 + 1 ) = 1
151 150 oveq1i 
 |-  ( ( 0 + 1 ) mod p ) = ( 1 mod p )
152 149 151 eqtrdi 
 |-  ( ( ( ( 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 ) )
153 133 nnred 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> p e. RR )
154 prmuz2 
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
155 119 154 syl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> p e. ( ZZ>= ` 2 ) )
156 eluz2b2 
 |-  ( p e. ( ZZ>= ` 2 ) <-> ( p e. NN /\ 1 < p ) )
157 155 156 sylib 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( p e. NN /\ 1 < p ) )
158 157 simprd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> 1 < p )
159 1mod 
 |-  ( ( p e. RR /\ 1 < p ) -> ( 1 mod p ) = 1 )
160 153 158 159 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( 1 mod p ) = 1 )
161 152 160 eqtrd 
 |-  ( ( ( ( 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 )
162 161 oveq1d 
 |-  ( ( ( ( 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 ) )
163 1m1e0 
 |-  ( 1 - 1 ) = 0
164 162 163 eqtrdi 
 |-  ( ( ( ( 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 )
165 124 164 eqtrd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) /\ p =/= 2 ) -> ( A /L p ) = 0 )
166 116 165 pm2.61dane 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( A /L p ) = 0 )
167 166 oveq1d 
 |-  ( ( ( 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 ) ) )
168 zq 
 |-  ( N e. ZZ -> N e. QQ )
169 76 168 syl 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> N e. QQ )
170 pcabs 
 |-  ( ( p e. Prime /\ N e. QQ ) -> ( p pCnt ( abs ` N ) ) = ( p pCnt N ) )
171 118 169 170 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( p pCnt ( abs ` N ) ) = ( p pCnt N ) )
172 pcelnn 
 |-  ( ( p e. Prime /\ ( abs ` N ) e. NN ) -> ( ( p pCnt ( abs ` N ) ) e. NN <-> p || ( abs ` N ) ) )
173 118 84 172 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( ( p pCnt ( abs ` N ) ) e. NN <-> p || ( abs ` N ) ) )
174 83 173 mpbird 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( p pCnt ( abs ` N ) ) e. NN )
175 171 174 eqeltrrd 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( p pCnt N ) e. NN )
176 175 0expd 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( 0 ^ ( p pCnt N ) ) = 0 )
177 167 176 eqtrd 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( p e. Prime /\ p || ( A gcd N ) ) ) -> ( ( A /L p ) ^ ( p pCnt N ) ) = 0 )
178 104 106 177 3eqtrd 
 |-  ( ( ( 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 )
179 66 67 69 71 94 84 178 seqz 
 |-  ( ( ( 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 )
180 179 rexlimdvaa 
 |-  ( ( 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 ) )
181 65 180 syl5 
 |-  ( ( 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 ) )
182 62 181 mpand 
 |-  ( ( 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 ) )
183 182 necon1d 
 |-  ( ( 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 ) )
184 51 adantr 
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) -> ( abs ` N ) e. ( ZZ>= ` 1 ) )
185 53 adantl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. ( 1 ... ( abs ` N ) ) ) -> k e. NN )
186 eleq1w 
 |-  ( n = k -> ( n e. Prime <-> k e. Prime ) )
187 oveq2 
 |-  ( n = k -> ( A /L n ) = ( A /L k ) )
188 oveq1 
 |-  ( n = k -> ( n pCnt N ) = ( k pCnt N ) )
189 187 188 oveq12d 
 |-  ( n = k -> ( ( A /L n ) ^ ( n pCnt N ) ) = ( ( A /L k ) ^ ( k pCnt N ) ) )
190 186 189 ifbieq1d 
 |-  ( n = k -> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) )
191 ovex 
 |-  ( ( A /L k ) ^ ( k pCnt N ) ) e. _V
192 191 101 ifex 
 |-  if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) e. _V
193 190 36 192 fvmpt 
 |-  ( 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 ) )
194 185 193 syl 
 |-  ( ( ( ( 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 ) )
195 simpll1 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> A e. ZZ )
196 prmz 
 |-  ( k e. Prime -> k e. ZZ )
197 196 adantl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> k e. ZZ )
198 lgscl 
 |-  ( ( A e. ZZ /\ k e. ZZ ) -> ( A /L k ) e. ZZ )
199 195 197 198 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( A /L k ) e. ZZ )
200 199 zcnd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( A /L k ) e. CC )
201 200 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) -> ( A /L k ) e. CC )
202 oveq2 
 |-  ( k = 2 -> ( A /L k ) = ( A /L 2 ) )
203 195 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) -> A e. ZZ )
204 203 108 syl 
 |-  ( ( ( ( ( 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 ) ) )
205 202 204 sylan9eqr 
 |-  ( ( ( ( ( ( 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 ) ) )
206 nprmdvds1 
 |-  ( k e. Prime -> -. k || 1 )
207 206 adantl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> -. k || 1 )
208 simpll2 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> N e. ZZ )
209 dvdsgcdb 
 |-  ( ( k e. ZZ /\ A e. ZZ /\ N e. ZZ ) -> ( ( k || A /\ k || N ) <-> k || ( A gcd N ) ) )
210 197 195 208 209 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( ( k || A /\ k || N ) <-> k || ( A gcd N ) ) )
211 simplr 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( A gcd N ) = 1 )
212 211 breq2d 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( k || ( A gcd N ) <-> k || 1 ) )
213 210 212 bitrd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( ( k || A /\ k || N ) <-> k || 1 ) )
214 207 213 mtbird 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> -. ( k || A /\ k || N ) )
215 imnan 
 |-  ( ( k || A -> -. k || N ) <-> -. ( k || A /\ k || N ) )
216 214 215 sylibr 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( k || A -> -. k || N ) )
217 216 con2d 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( k || N -> -. k || A ) )
218 217 imp 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) -> -. k || A )
219 breq1 
 |-  ( k = 2 -> ( k || A <-> 2 || A ) )
220 219 notbid 
 |-  ( k = 2 -> ( -. k || A <-> -. 2 || A ) )
221 218 220 syl5ibcom 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) -> ( k = 2 -> -. 2 || A ) )
222 221 imp 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k = 2 ) -> -. 2 || A )
223 222 iffalsed 
 |-  ( ( ( ( ( ( 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 ) )
224 205 223 eqtrd 
 |-  ( ( ( ( ( ( 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 ) )
225 neeq1 
 |-  ( 1 = if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) -> ( 1 =/= 0 <-> if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) =/= 0 ) )
226 neeq1 
 |-  ( -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 ) )
227 225 226 4 41 keephyp 
 |-  if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) =/= 0
228 227 a1i 
 |-  ( ( ( ( ( ( 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 )
229 224 228 eqnetrd 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k = 2 ) -> ( A /L k ) =/= 0 )
230 simpr 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> k e. Prime )
231 230 ad2antrr 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> k e. Prime )
232 231 206 syl 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> -. k || 1 )
233 simplr 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> k || N )
234 231 196 syl 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> k e. ZZ )
235 203 adantr 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> A e. ZZ )
236 simpr 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> k =/= 2 )
237 eldifsn 
 |-  ( k e. ( Prime \ { 2 } ) <-> ( k e. Prime /\ k =/= 2 ) )
238 231 236 237 sylanbrc 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> k e. ( Prime \ { 2 } ) )
239 oddprm 
 |-  ( k e. ( Prime \ { 2 } ) -> ( ( k - 1 ) / 2 ) e. NN )
240 238 239 syl 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> ( ( k - 1 ) / 2 ) e. NN )
241 240 nnnn0d 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> ( ( k - 1 ) / 2 ) e. NN0 )
242 zexpcl 
 |-  ( ( A e. ZZ /\ ( ( k - 1 ) / 2 ) e. NN0 ) -> ( A ^ ( ( k - 1 ) / 2 ) ) e. ZZ )
243 235 241 242 syl2anc 
 |-  ( ( ( ( ( ( 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 )
244 208 ad2antrr 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> N e. ZZ )
245 dvdsgcd 
 |-  ( ( 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 ) ) )
246 234 243 244 245 syl3anc 
 |-  ( ( ( ( ( ( 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 ) ) )
247 233 246 mpan2d 
 |-  ( ( ( ( ( ( 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 ) ) )
248 235 zcnd 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> A e. CC )
249 248 241 absexpd 
 |-  ( ( ( ( ( ( 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 ) ) )
250 249 oveq1d 
 |-  ( ( ( ( ( ( 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 ) ) )
251 gcdabs 
 |-  ( ( ( A ^ ( ( k - 1 ) / 2 ) ) e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A ^ ( ( k - 1 ) / 2 ) ) ) gcd ( abs ` N ) ) = ( ( A ^ ( ( k - 1 ) / 2 ) ) gcd N ) )
252 243 244 251 syl2anc 
 |-  ( ( ( ( ( ( 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 ) )
253 gcdabs 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` A ) gcd ( abs ` N ) ) = ( A gcd N ) )
254 235 244 253 syl2anc 
 |-  ( ( ( ( ( ( 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 ) )
255 211 ad2antrr 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> ( A gcd N ) = 1 )
256 254 255 eqtrd 
 |-  ( ( ( ( ( ( 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 )
257 218 adantr 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> -. k || A )
258 dvds0 
 |-  ( k e. ZZ -> k || 0 )
259 234 258 syl 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> k || 0 )
260 breq2 
 |-  ( A = 0 -> ( k || A <-> k || 0 ) )
261 259 260 syl5ibrcom 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> ( A = 0 -> k || A ) )
262 261 necon3bd 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> ( -. k || A -> A =/= 0 ) )
263 257 262 mpd 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> A =/= 0 )
264 nnabscl 
 |-  ( ( A e. ZZ /\ A =/= 0 ) -> ( abs ` A ) e. NN )
265 235 263 264 syl2anc 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> ( abs ` A ) e. NN )
266 simpll3 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> N =/= 0 )
267 208 266 48 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( abs ` N ) e. NN )
268 267 ad2antrr 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> ( abs ` N ) e. NN )
269 rplpwr 
 |-  ( ( ( 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 ) )
270 265 268 240 269 syl3anc 
 |-  ( ( ( ( ( ( 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 ) )
271 256 270 mpd 
 |-  ( ( ( ( ( ( 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 )
272 250 252 271 3eqtr3d 
 |-  ( ( ( ( ( ( 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 )
273 272 breq2d 
 |-  ( ( ( ( ( ( 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 ) )
274 247 273 sylibd 
 |-  ( ( ( ( ( ( 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 ) )
275 232 274 mtod 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> -. k || ( A ^ ( ( k - 1 ) / 2 ) ) )
276 prmnn 
 |-  ( k e. Prime -> k e. NN )
277 276 adantl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> k e. NN )
278 277 ad2antrr 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> k e. NN )
279 dvdsval3 
 |-  ( ( k e. NN /\ ( A ^ ( ( k - 1 ) / 2 ) ) e. ZZ ) -> ( k || ( A ^ ( ( k - 1 ) / 2 ) ) <-> ( ( A ^ ( ( k - 1 ) / 2 ) ) mod k ) = 0 ) )
280 278 243 279 syl2anc 
 |-  ( ( ( ( ( ( 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 ) )
281 280 necon3bbid 
 |-  ( ( ( ( ( ( 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 ) )
282 275 281 mpbid 
 |-  ( ( ( ( ( ( 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 )
283 lgsvalmod 
 |-  ( ( A e. ZZ /\ k e. ( Prime \ { 2 } ) ) -> ( ( A /L k ) mod k ) = ( ( A ^ ( ( k - 1 ) / 2 ) ) mod k ) )
284 235 238 283 syl2anc 
 |-  ( ( ( ( ( ( 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 ) )
285 278 nnrpd 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> k e. RR+ )
286 0mod 
 |-  ( k e. RR+ -> ( 0 mod k ) = 0 )
287 285 286 syl 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> ( 0 mod k ) = 0 )
288 282 284 287 3netr4d 
 |-  ( ( ( ( ( ( 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 ) )
289 oveq1 
 |-  ( ( A /L k ) = 0 -> ( ( A /L k ) mod k ) = ( 0 mod k ) )
290 289 necon3i 
 |-  ( ( ( A /L k ) mod k ) =/= ( 0 mod k ) -> ( A /L k ) =/= 0 )
291 288 290 syl 
 |-  ( ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) /\ k =/= 2 ) -> ( A /L k ) =/= 0 )
292 229 291 pm2.61dane 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) -> ( A /L k ) =/= 0 )
293 pczcl 
 |-  ( ( k e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( k pCnt N ) e. NN0 )
294 230 208 266 293 syl12anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( k pCnt N ) e. NN0 )
295 294 nn0zd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( k pCnt N ) e. ZZ )
296 295 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ k || N ) -> ( k pCnt N ) e. ZZ )
297 neeq1 
 |-  ( x = ( ( A /L k ) ^ ( k pCnt N ) ) -> ( x =/= 0 <-> ( ( A /L k ) ^ ( k pCnt N ) ) =/= 0 ) )
298 expclz 
 |-  ( ( ( A /L k ) e. CC /\ ( A /L k ) =/= 0 /\ ( k pCnt N ) e. ZZ ) -> ( ( A /L k ) ^ ( k pCnt N ) ) e. CC )
299 expne0i 
 |-  ( ( ( A /L k ) e. CC /\ ( A /L k ) =/= 0 /\ ( k pCnt N ) e. ZZ ) -> ( ( A /L k ) ^ ( k pCnt N ) ) =/= 0 )
300 297 298 299 elrabd 
 |-  ( ( ( 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 } )
301 201 292 296 300 syl3anc 
 |-  ( ( ( ( ( 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 } )
302 dvdsabsb 
 |-  ( ( k e. ZZ /\ N e. ZZ ) -> ( k || N <-> k || ( abs ` N ) ) )
303 197 208 302 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( k || N <-> k || ( abs ` N ) ) )
304 303 notbid 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( -. k || N <-> -. k || ( abs ` N ) ) )
305 pceq0 
 |-  ( ( k e. Prime /\ ( abs ` N ) e. NN ) -> ( ( k pCnt ( abs ` N ) ) = 0 <-> -. k || ( abs ` N ) ) )
306 230 267 305 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( ( k pCnt ( abs ` N ) ) = 0 <-> -. k || ( abs ` N ) ) )
307 208 168 syl 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> N e. QQ )
308 pcabs 
 |-  ( ( k e. Prime /\ N e. QQ ) -> ( k pCnt ( abs ` N ) ) = ( k pCnt N ) )
309 230 307 308 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( k pCnt ( abs ` N ) ) = ( k pCnt N ) )
310 309 eqeq1d 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( ( k pCnt ( abs ` N ) ) = 0 <-> ( k pCnt N ) = 0 ) )
311 304 306 310 3bitr2rd 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) -> ( ( k pCnt N ) = 0 <-> -. k || N ) )
312 311 biimpar 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ -. k || N ) -> ( k pCnt N ) = 0 )
313 312 oveq2d 
 |-  ( ( ( ( ( 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 ) )
314 200 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ -. k || N ) -> ( A /L k ) e. CC )
315 314 exp0d 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ -. k || N ) -> ( ( A /L k ) ^ 0 ) = 1 )
316 313 315 eqtrd 
 |-  ( ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ k e. Prime ) /\ -. k || N ) -> ( ( A /L k ) ^ ( k pCnt N ) ) = 1 )
317 neeq1 
 |-  ( x = 1 -> ( x =/= 0 <-> 1 =/= 0 ) )
318 317 elrab 
 |-  ( 1 e. { x e. CC | x =/= 0 } <-> ( 1 e. CC /\ 1 =/= 0 ) )
319 45 4 318 mpbir2an 
 |-  1 e. { x e. CC | x =/= 0 }
320 316 319 eqeltrdi 
 |-  ( ( ( ( ( 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 } )
321 301 320 pm2.61dan 
 |-  ( ( ( ( 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 } )
322 319 a1i 
 |-  ( ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( A gcd N ) = 1 ) /\ -. k e. Prime ) -> 1 e. { x e. CC | x =/= 0 } )
323 321 322 ifclda 
 |-  ( ( ( 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 } )
324 323 adantr 
 |-  ( ( ( ( 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 } )
325 194 324 eqeltrd 
 |-  ( ( ( ( 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 } )
326 neeq1 
 |-  ( x = k -> ( x =/= 0 <-> k =/= 0 ) )
327 326 elrab 
 |-  ( k e. { x e. CC | x =/= 0 } <-> ( k e. CC /\ k =/= 0 ) )
328 neeq1 
 |-  ( x = y -> ( x =/= 0 <-> y =/= 0 ) )
329 328 elrab 
 |-  ( y e. { x e. CC | x =/= 0 } <-> ( y e. CC /\ y =/= 0 ) )
330 mulcl 
 |-  ( ( k e. CC /\ y e. CC ) -> ( k x. y ) e. CC )
331 330 ad2ant2r 
 |-  ( ( ( k e. CC /\ k =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( k x. y ) e. CC )
332 mulne0 
 |-  ( ( ( k e. CC /\ k =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( k x. y ) =/= 0 )
333 331 332 jca 
 |-  ( ( ( k e. CC /\ k =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( ( k x. y ) e. CC /\ ( k x. y ) =/= 0 ) )
334 327 329 333 syl2anb 
 |-  ( ( k e. { x e. CC | x =/= 0 } /\ y e. { x e. CC | x =/= 0 } ) -> ( ( k x. y ) e. CC /\ ( k x. y ) =/= 0 ) )
335 neeq1 
 |-  ( x = ( k x. y ) -> ( x =/= 0 <-> ( k x. y ) =/= 0 ) )
336 335 elrab 
 |-  ( ( k x. y ) e. { x e. CC | x =/= 0 } <-> ( ( k x. y ) e. CC /\ ( k x. y ) =/= 0 ) )
337 334 336 sylibr 
 |-  ( ( k e. { x e. CC | x =/= 0 } /\ y e. { x e. CC | x =/= 0 } ) -> ( k x. y ) e. { x e. CC | x =/= 0 } )
338 337 adantl 
 |-  ( ( ( ( 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 } )
339 184 325 338 seqcl 
 |-  ( ( ( 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 } )
340 neeq1 
 |-  ( 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 ) )
341 340 elrab 
 |-  ( ( 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 ) )
342 341 simprbi 
 |-  ( ( 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 )
343 339 342 syl 
 |-  ( ( ( 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 )
344 343 ex 
 |-  ( ( 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 ) )
345 183 344 impbid 
 |-  ( ( 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 ) )
346 38 61 345 3bitrd 
 |-  ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( ( A /L N ) =/= 0 <-> ( A gcd N ) = 1 ) )
347 346 3expa 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ N =/= 0 ) -> ( ( A /L N ) =/= 0 <-> ( A gcd N ) = 1 ) )
348 35 347 pm2.61dane 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( A /L N ) =/= 0 <-> ( A gcd N ) = 1 ) )