Metamath Proof Explorer

Theorem lgsneg

Description: The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsneg ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L - 𝑁 ) = ( if ( 𝐴 < 0 , - 1 , 1 ) · ( 𝐴 /L 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 iftrue ⊢ ( 𝐴 < 0 → if ( 𝐴 < 0 , - 1 , 1 ) = - 1 )
2 1 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → if ( 𝐴 < 0 , - 1 , 1 ) = - 1 )
3 2 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( if ( 𝐴 < 0 , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) = ( - 1 · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) )
4 oveq2 ⊢ ( if ( 𝑁 < 0 , - 1 , 1 ) = - 1 → ( - 1 · if ( 𝑁 < 0 , - 1 , 1 ) ) = ( - 1 · - 1 ) )
5 neg1mulneg1e1 ⊢ ( - 1 · - 1 ) = 1
6 4 5 eqtrdi ⊢ ( if ( 𝑁 < 0 , - 1 , 1 ) = - 1 → ( - 1 · if ( 𝑁 < 0 , - 1 , 1 ) ) = 1 )
7 oveq2 ⊢ ( if ( 𝑁 < 0 , - 1 , 1 ) = 1 → ( - 1 · if ( 𝑁 < 0 , - 1 , 1 ) ) = ( - 1 · 1 ) )
8 ax-1cn ⊢ 1 ∈ ℂ
9 8 mulm1i ⊢ ( - 1 · 1 ) = - 1
10 7 9 eqtrdi ⊢ ( if ( 𝑁 < 0 , - 1 , 1 ) = 1 → ( - 1 · if ( 𝑁 < 0 , - 1 , 1 ) ) = - 1 )
11 6 10 ifsb ⊢ ( - 1 · if ( 𝑁 < 0 , - 1 , 1 ) ) = if ( 𝑁 < 0 , 1 , - 1 )
12 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → 𝐴 < 0 )
13 12 biantrud ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( 𝑁 < 0 ↔ ( 𝑁 < 0 ∧ 𝐴 < 0 ) ) )
14 13 ifbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → if ( 𝑁 < 0 , - 1 , 1 ) = if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) )
15 14 oveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( - 1 · if ( 𝑁 < 0 , - 1 , 1 ) ) = ( - 1 · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) )
16 simpl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → 𝑁 ≠ 0 )
17 16 necomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → 0 ≠ 𝑁 )
18 simpl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → 𝑁 ∈ ℤ )
19 18 zred ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → 𝑁 ∈ ℝ )
20 0re ⊢ 0 ∈ ℝ
21 ltlen ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑁 < 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≠ 𝑁 ) ) )
22 19 20 21 sylancl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( 𝑁 < 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≠ 𝑁 ) ) )
23 17 22 mpbiran2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( 𝑁 < 0 ↔ 𝑁 ≤ 0 ) )
24 19 le0neg1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( 𝑁 ≤ 0 ↔ 0 ≤ - 𝑁 ) )
25 19 renegcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → - 𝑁 ∈ ℝ )
26 lenlt ⊢ ( ( 0 ∈ ℝ ∧ - 𝑁 ∈ ℝ ) → ( 0 ≤ - 𝑁 ↔ ¬ - 𝑁 < 0 ) )
27 20 25 26 sylancr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( 0 ≤ - 𝑁 ↔ ¬ - 𝑁 < 0 ) )
28 23 24 27 3bitrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( 𝑁 < 0 ↔ ¬ - 𝑁 < 0 ) )
29 28 ifbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → if ( 𝑁 < 0 , 1 , - 1 ) = if ( ¬ - 𝑁 < 0 , 1 , - 1 ) )
30 ifnot ⊢ if ( ¬ - 𝑁 < 0 , 1 , - 1 ) = if ( - 𝑁 < 0 , - 1 , 1 )
31 29 30 eqtrdi ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → if ( 𝑁 < 0 , 1 , - 1 ) = if ( - 𝑁 < 0 , - 1 , 1 ) )
32 11 15 31 3eqtr3a ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( - 1 · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) = if ( - 𝑁 < 0 , - 1 , 1 ) )
33 12 biantrud ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( - 𝑁 < 0 ↔ ( - 𝑁 < 0 ∧ 𝐴 < 0 ) ) )
34 33 ifbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → if ( - 𝑁 < 0 , - 1 , 1 ) = if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) )
35 3 32 34 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝐴 < 0 ) → ( if ( 𝐴 < 0 , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) = if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) )
36 1t1e1 ⊢ ( 1 · 1 ) = 1
37 iffalse ⊢ ( ¬ 𝐴 < 0 → if ( 𝐴 < 0 , - 1 , 1 ) = 1 )
38 37 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ¬ 𝐴 < 0 ) → if ( 𝐴 < 0 , - 1 , 1 ) = 1 )
39 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ¬ 𝐴 < 0 ) → ¬ 𝐴 < 0 )
40 39 intnand ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ¬ 𝐴 < 0 ) → ¬ ( 𝑁 < 0 ∧ 𝐴 < 0 ) )
41 40 iffalsed ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ¬ 𝐴 < 0 ) → if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = 1 )
42 38 41 oveq12d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ¬ 𝐴 < 0 ) → ( if ( 𝐴 < 0 , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) = ( 1 · 1 ) )
43 39 intnand ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ¬ 𝐴 < 0 ) → ¬ ( - 𝑁 < 0 ∧ 𝐴 < 0 ) )
44 43 iffalsed ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ¬ 𝐴 < 0 ) → if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = 1 )
45 36 42 44 3eqtr4a ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ¬ 𝐴 < 0 ) → ( if ( 𝐴 < 0 , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) = if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) )
46 35 45 pm2.61dan ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( if ( 𝐴 < 0 , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) = if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) )
47 46 eqcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = ( if ( 𝐴 < 0 , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) )
48 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝑛 ∈ ℙ ) → 𝑛 ∈ ℙ )
49 simpl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝑛 ∈ ℙ ) → 𝑁 ∈ ℤ )
50 zq ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℚ )
51 49 50 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝑛 ∈ ℙ ) → 𝑁 ∈ ℚ )
52 pcneg ⊢ ( ( 𝑛 ∈ ℙ ∧ 𝑁 ∈ ℚ ) → ( 𝑛 pCnt - 𝑁 ) = ( 𝑛 pCnt 𝑁 ) )
53 48 51 52 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt - 𝑁 ) = ( 𝑛 pCnt 𝑁 ) )
54 53 oveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) = ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) )
55 54 ifeq1da ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) = if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
56 55 mpteq2dv ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) )
57 56 seqeq3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) )
58 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
59 58 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝑁 ∈ ℂ )
60 59 absnegd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ - 𝑁 ) = ( abs ‘ 𝑁 ) )
61 57 60 fveq12d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ - 𝑁 ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) )
62 47 61 oveq12d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ - 𝑁 ) ) ) = ( ( if ( 𝐴 < 0 , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
63 neg1cn ⊢ - 1 ∈ ℂ
64 63 8 ifcli ⊢ if ( 𝐴 < 0 , - 1 , 1 ) ∈ ℂ
65 64 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → if ( 𝐴 < 0 , - 1 , 1 ) ∈ ℂ )
66 63 8 ifcli ⊢ if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ ℂ
67 66 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ∈ ℂ )
68 nnabscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
69 68 3adant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
70 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
71 69 70 eleqtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
72 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
73 72 lgsfcl3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ )
74 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) → 𝑥 ∈ ℕ )
75 ffvelrn ⊢ ( ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) : ℕ ⟶ ℤ ∧ 𝑥 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑥 ) ∈ ℤ )
76 73 74 75 syl2an ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ 𝑥 ∈ ( 1 ... ( abs ‘ 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ‘ 𝑥 ) ∈ ℤ )
77 zmulcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
78 77 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
79 71 76 78 seqcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ∈ ℤ )
80 79 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ∈ ℂ )
81 65 67 80 mulassd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( ( if ( 𝐴 < 0 , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) = ( if ( 𝐴 < 0 , - 1 , 1 ) · ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
82 62 81 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ - 𝑁 ) ) ) = ( if ( 𝐴 < 0 , - 1 , 1 ) · ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
83 simp1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝐴 ∈ ℤ )
84 znegcl ⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
85 84 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → - 𝑁 ∈ ℤ )
86 simp3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝑁 ≠ 0 )
87 59 86 negne0d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → - 𝑁 ≠ 0 )
88 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) )
89 88 lgsval4 ⊢ ( ( 𝐴 ∈ ℤ ∧ - 𝑁 ∈ ℤ ∧ - 𝑁 ≠ 0 ) → ( 𝐴 /L - 𝑁 ) = ( if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ - 𝑁 ) ) ) )
90 83 85 87 89 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L - 𝑁 ) = ( if ( ( - 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt - 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ - 𝑁 ) ) ) )
91 72 lgsval4 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
92 91 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( if ( 𝐴 < 0 , - 1 , 1 ) · ( 𝐴 /L 𝑁 ) ) = ( if ( 𝐴 < 0 , - 1 , 1 ) · ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
93 82 90 92 3eqtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L - 𝑁 ) = ( if ( 𝐴 < 0 , - 1 , 1 ) · ( 𝐴 /L 𝑁 ) ) )