Step | Hyp | Ref
| Expression |
1 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝐴 < 0 → if(𝐴 < 0, -1, 1) =
-1) |
2 | 1 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(𝐴 < 0, -1, 1) = -1) |
3 | 2 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = (-1 · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))) |
4 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (if(𝑁 < 0, -1, 1) = -1 → (-1
· if(𝑁 < 0, -1,
1)) = (-1 · -1)) |
5 | | neg1mulneg1e1 11122 |
. . . . . . . . . 10
⊢ (-1
· -1) = 1 |
6 | 4, 5 | syl6eq 2660 |
. . . . . . . . 9
⊢ (if(𝑁 < 0, -1, 1) = -1 → (-1
· if(𝑁 < 0, -1,
1)) = 1) |
7 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (if(𝑁 < 0, -1, 1) = 1 → (-1
· if(𝑁 < 0, -1,
1)) = (-1 · 1)) |
8 | | ax-1cn 9873 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
9 | 8 | mulm1i 10354 |
. . . . . . . . . 10
⊢ (-1
· 1) = -1 |
10 | 7, 9 | syl6eq 2660 |
. . . . . . . . 9
⊢ (if(𝑁 < 0, -1, 1) = 1 → (-1
· if(𝑁 < 0, -1,
1)) = -1) |
11 | 6, 10 | ifsb 4049 |
. . . . . . . 8
⊢ (-1
· if(𝑁 < 0, -1,
1)) = if(𝑁 < 0, 1,
-1) |
12 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 𝐴 < 0) |
13 | 12 | biantrud 527 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 < 0 ↔ (𝑁 < 0 ∧ 𝐴 < 0))) |
14 | 13 | ifbid 4058 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(𝑁 < 0, -1, 1) = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) |
15 | 14 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (-1 · if(𝑁 < 0, -1, 1)) = (-1 ·
if((𝑁 < 0 ∧ 𝐴 < 0), -1,
1))) |
16 | | simpl2 1058 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 𝑁 ∈ ℤ) |
17 | 16 | zred 11358 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 𝑁 ∈ ℝ) |
18 | | 0re 9919 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
19 | | ltlen 10017 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑁 < 0
↔ (𝑁 ≤ 0 ∧ 0
≠ 𝑁))) |
20 | 17, 18, 19 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁))) |
21 | | simpl3 1059 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 𝑁 ≠ 0) |
22 | 21 | necomd 2837 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 0 ≠ 𝑁) |
23 | 22 | biantrud 527 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 ≤ 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁))) |
24 | 20, 23 | bitr4d 270 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 < 0 ↔ 𝑁 ≤ 0)) |
25 | 17 | le0neg1d 10478 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 ≤ 0 ↔ 0 ≤ -𝑁)) |
26 | 17 | renegcld 10336 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → -𝑁 ∈ ℝ) |
27 | | lenlt 9995 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ -𝑁
∈ ℝ) → (0 ≤ -𝑁 ↔ ¬ -𝑁 < 0)) |
28 | 18, 26, 27 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (0 ≤ -𝑁 ↔ ¬ -𝑁 < 0)) |
29 | 24, 25, 28 | 3bitrd 293 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 < 0 ↔ ¬ -𝑁 < 0)) |
30 | 29 | ifbid 4058 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(𝑁 < 0, 1, -1) = if(¬ -𝑁 < 0, 1,
-1)) |
31 | | ifnot 4083 |
. . . . . . . . 9
⊢ if(¬
-𝑁 < 0, 1, -1) =
if(-𝑁 < 0, -1,
1) |
32 | 30, 31 | syl6eq 2660 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(𝑁 < 0, 1, -1) = if(-𝑁 < 0, -1, 1)) |
33 | 11, 15, 32 | 3eqtr3a 2668 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (-1 · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = if(-𝑁 < 0, -1, 1)) |
34 | 12 | biantrud 527 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (-𝑁 < 0 ↔ (-𝑁 < 0 ∧ 𝐴 < 0))) |
35 | 34 | ifbid 4058 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(-𝑁 < 0, -1, 1) = if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) |
36 | 3, 33, 35 | 3eqtrd 2648 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) |
37 | | 1t1e1 11052 |
. . . . . . 7
⊢ (1
· 1) = 1 |
38 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
𝐴 < 0 → if(𝐴 < 0, -1, 1) =
1) |
39 | 38 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → if(𝐴 < 0, -1, 1) =
1) |
40 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → ¬ 𝐴 < 0) |
41 | 40 | intnand 953 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → ¬ (𝑁 < 0 ∧ 𝐴 < 0)) |
42 | 41 | iffalsed 4047 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = 1) |
43 | 39, 42 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → (if(𝐴 < 0, -1, 1) ·
if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = (1 ·
1)) |
44 | 40 | intnand 953 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → ¬ (-𝑁 < 0 ∧ 𝐴 < 0)) |
45 | 44 | iffalsed 4047 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = 1) |
46 | 37, 43, 45 | 3eqtr4a 2670 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → (if(𝐴 < 0, -1, 1) ·
if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) |
47 | 36, 46 | pm2.61dan 828 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if(𝐴 < 0, -1, 1) ·
if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) |
48 | 47 | eqcomd 2616 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = (if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))) |
49 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈
ℙ) |
50 | | simpl2 1058 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → 𝑁 ∈
ℤ) |
51 | | zq 11670 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℚ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → 𝑁 ∈
ℚ) |
53 | | pcneg 15416 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑛 pCnt -𝑁) = (𝑛 pCnt 𝑁)) |
54 | 49, 52, 53 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt -𝑁) = (𝑛 pCnt 𝑁)) |
55 | 54 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → ((𝐴 /L 𝑛)↑(𝑛 pCnt -𝑁)) = ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁))) |
56 | 55 | ifeq1da 4066 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt -𝑁)), 1) = if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
57 | 56 | mpteq2dv 4673 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt -𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))) |
58 | 57 | seqeq3d 12671 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt -𝑁)), 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))) |
59 | | zcn 11259 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
60 | 59 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝑁 ∈
ℂ) |
61 | 60 | absnegd 14036 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) →
(abs‘-𝑁) =
(abs‘𝑁)) |
62 | 58, 61 | fveq12d 6109 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) |
63 | 48, 62 | oveq12d 6567 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁))) = ((if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
64 | | neg1cn 11001 |
. . . . . 6
⊢ -1 ∈
ℂ |
65 | 64, 8 | keepel 4105 |
. . . . 5
⊢ if(𝐴 < 0, -1, 1) ∈
ℂ |
66 | 65 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if(𝐴 < 0, -1, 1) ∈
ℂ) |
67 | 64, 8 | keepel 4105 |
. . . . 5
⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ |
68 | 67 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ) |
69 | | nnabscl 13913 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
70 | 69 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
71 | | nnuz 11599 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
72 | 70, 71 | syl6eleq 2698 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
(ℤ≥‘1)) |
73 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
74 | 73 | lgsfcl3 24843 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
75 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑥 ∈ (1...(abs‘𝑁)) → 𝑥 ∈ ℕ) |
76 | | ffvelrn 6265 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑥 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑥) ∈ ℤ) |
77 | 74, 75, 76 | syl2an 493 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑥 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑥) ∈ ℤ) |
78 | | zmulcl 11303 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) |
79 | 78 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ) |
80 | 72, 77, 79 | seqcl 12683 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℤ) |
81 | 80 | zcnd 11359 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ) |
82 | 66, 68, 81 | mulassd 9942 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if(𝐴 < 0, -1, 1) ·
if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) ·
(seq1( · , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, ((𝐴
/L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) = (if(𝐴 < 0, -1, 1) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
83 | 63, 82 | eqtrd 2644 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁))) = (if(𝐴 < 0, -1, 1) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
84 | | simp1 1054 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐴 ∈
ℤ) |
85 | | znegcl 11289 |
. . . 4
⊢ (𝑁 ∈ ℤ → -𝑁 ∈
ℤ) |
86 | 85 | 3ad2ant2 1076 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → -𝑁 ∈
ℤ) |
87 | | simp3 1056 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0) |
88 | 60, 87 | negne0d 10269 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → -𝑁 ≠ 0) |
89 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt -𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt -𝑁)), 1)) |
90 | 89 | lgsval4 24842 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ -𝑁 ∈ ℤ ∧ -𝑁 ≠ 0) → (𝐴 /L -𝑁) = (if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁)))) |
91 | 84, 86, 88, 90 | syl3anc 1318 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L -𝑁) = (if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁)))) |
92 | 73 | lgsval4 24842 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
93 | 92 | oveq2d 6565 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if(𝐴 < 0, -1, 1) · (𝐴 /L 𝑁)) = (if(𝐴 < 0, -1, 1) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
94 | 83, 91, 93 | 3eqtr4d 2654 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L -𝑁) = (if(𝐴 < 0, -1, 1) · (𝐴 /L 𝑁))) |