Step |
Hyp |
Ref |
Expression |
1 |
|
iftrue |
|- ( A < 0 -> if ( A < 0 , -u 1 , 1 ) = -u 1 ) |
2 |
1
|
adantl |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> if ( A < 0 , -u 1 , 1 ) = -u 1 ) |
3 |
2
|
oveq1d |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( if ( A < 0 , -u 1 , 1 ) x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) = ( -u 1 x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) ) |
4 |
|
oveq2 |
|- ( if ( N < 0 , -u 1 , 1 ) = -u 1 -> ( -u 1 x. if ( N < 0 , -u 1 , 1 ) ) = ( -u 1 x. -u 1 ) ) |
5 |
|
neg1mulneg1e1 |
|- ( -u 1 x. -u 1 ) = 1 |
6 |
4 5
|
eqtrdi |
|- ( if ( N < 0 , -u 1 , 1 ) = -u 1 -> ( -u 1 x. if ( N < 0 , -u 1 , 1 ) ) = 1 ) |
7 |
|
oveq2 |
|- ( if ( N < 0 , -u 1 , 1 ) = 1 -> ( -u 1 x. if ( N < 0 , -u 1 , 1 ) ) = ( -u 1 x. 1 ) ) |
8 |
|
ax-1cn |
|- 1 e. CC |
9 |
8
|
mulm1i |
|- ( -u 1 x. 1 ) = -u 1 |
10 |
7 9
|
eqtrdi |
|- ( if ( N < 0 , -u 1 , 1 ) = 1 -> ( -u 1 x. if ( N < 0 , -u 1 , 1 ) ) = -u 1 ) |
11 |
6 10
|
ifsb |
|- ( -u 1 x. if ( N < 0 , -u 1 , 1 ) ) = if ( N < 0 , 1 , -u 1 ) |
12 |
|
simpr |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> A < 0 ) |
13 |
12
|
biantrud |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( N < 0 <-> ( N < 0 /\ A < 0 ) ) ) |
14 |
13
|
ifbid |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> if ( N < 0 , -u 1 , 1 ) = if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) |
15 |
14
|
oveq2d |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( -u 1 x. if ( N < 0 , -u 1 , 1 ) ) = ( -u 1 x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) ) |
16 |
|
simpl3 |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> N =/= 0 ) |
17 |
16
|
necomd |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> 0 =/= N ) |
18 |
|
simpl2 |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> N e. ZZ ) |
19 |
18
|
zred |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> N e. RR ) |
20 |
|
0re |
|- 0 e. RR |
21 |
|
ltlen |
|- ( ( N e. RR /\ 0 e. RR ) -> ( N < 0 <-> ( N <_ 0 /\ 0 =/= N ) ) ) |
22 |
19 20 21
|
sylancl |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( N < 0 <-> ( N <_ 0 /\ 0 =/= N ) ) ) |
23 |
17 22
|
mpbiran2d |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( N < 0 <-> N <_ 0 ) ) |
24 |
19
|
le0neg1d |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( N <_ 0 <-> 0 <_ -u N ) ) |
25 |
19
|
renegcld |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> -u N e. RR ) |
26 |
|
lenlt |
|- ( ( 0 e. RR /\ -u N e. RR ) -> ( 0 <_ -u N <-> -. -u N < 0 ) ) |
27 |
20 25 26
|
sylancr |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( 0 <_ -u N <-> -. -u N < 0 ) ) |
28 |
23 24 27
|
3bitrd |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( N < 0 <-> -. -u N < 0 ) ) |
29 |
28
|
ifbid |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> if ( N < 0 , 1 , -u 1 ) = if ( -. -u N < 0 , 1 , -u 1 ) ) |
30 |
|
ifnot |
|- if ( -. -u N < 0 , 1 , -u 1 ) = if ( -u N < 0 , -u 1 , 1 ) |
31 |
29 30
|
eqtrdi |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> if ( N < 0 , 1 , -u 1 ) = if ( -u N < 0 , -u 1 , 1 ) ) |
32 |
11 15 31
|
3eqtr3a |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( -u 1 x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) = if ( -u N < 0 , -u 1 , 1 ) ) |
33 |
12
|
biantrud |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( -u N < 0 <-> ( -u N < 0 /\ A < 0 ) ) ) |
34 |
33
|
ifbid |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> if ( -u N < 0 , -u 1 , 1 ) = if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) ) |
35 |
3 32 34
|
3eqtrd |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ A < 0 ) -> ( if ( A < 0 , -u 1 , 1 ) x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) = if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) ) |
36 |
|
1t1e1 |
|- ( 1 x. 1 ) = 1 |
37 |
|
iffalse |
|- ( -. A < 0 -> if ( A < 0 , -u 1 , 1 ) = 1 ) |
38 |
37
|
adantl |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ -. A < 0 ) -> if ( A < 0 , -u 1 , 1 ) = 1 ) |
39 |
|
simpr |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ -. A < 0 ) -> -. A < 0 ) |
40 |
39
|
intnand |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ -. A < 0 ) -> -. ( N < 0 /\ A < 0 ) ) |
41 |
40
|
iffalsed |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ -. A < 0 ) -> if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) = 1 ) |
42 |
38 41
|
oveq12d |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ -. A < 0 ) -> ( if ( A < 0 , -u 1 , 1 ) x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) = ( 1 x. 1 ) ) |
43 |
39
|
intnand |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ -. A < 0 ) -> -. ( -u N < 0 /\ A < 0 ) ) |
44 |
43
|
iffalsed |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ -. A < 0 ) -> if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) = 1 ) |
45 |
36 42 44
|
3eqtr4a |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ -. A < 0 ) -> ( if ( A < 0 , -u 1 , 1 ) x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) = if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) ) |
46 |
35 45
|
pm2.61dan |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( if ( A < 0 , -u 1 , 1 ) x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) = if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) ) |
47 |
46
|
eqcomd |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) = ( if ( A < 0 , -u 1 , 1 ) x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) ) |
48 |
|
simpr |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. Prime ) -> n e. Prime ) |
49 |
|
simpl2 |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. Prime ) -> N e. ZZ ) |
50 |
|
zq |
|- ( N e. ZZ -> N e. QQ ) |
51 |
49 50
|
syl |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. Prime ) -> N e. QQ ) |
52 |
|
pcneg |
|- ( ( n e. Prime /\ N e. QQ ) -> ( n pCnt -u N ) = ( n pCnt N ) ) |
53 |
48 51 52
|
syl2anc |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. Prime ) -> ( n pCnt -u N ) = ( n pCnt N ) ) |
54 |
53
|
oveq2d |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ n e. Prime ) -> ( ( A /L n ) ^ ( n pCnt -u N ) ) = ( ( A /L n ) ^ ( n pCnt N ) ) ) |
55 |
54
|
ifeq1da |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) = if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) |
56 |
55
|
mpteq2dv |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) |
57 |
56
|
seqeq3d |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) ) ) = seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ) |
58 |
|
zcn |
|- ( N e. ZZ -> N e. CC ) |
59 |
58
|
3ad2ant2 |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> N e. CC ) |
60 |
59
|
absnegd |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( abs ` -u N ) = ( abs ` N ) ) |
61 |
57 60
|
fveq12d |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) ) ) ` ( abs ` -u N ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` N ) ) ) |
62 |
47 61
|
oveq12d |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) ) ) ` ( abs ` -u N ) ) ) = ( ( if ( A < 0 , -u 1 , 1 ) x. 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 ) ) ) ) |
63 |
|
neg1cn |
|- -u 1 e. CC |
64 |
63 8
|
ifcli |
|- if ( A < 0 , -u 1 , 1 ) e. CC |
65 |
64
|
a1i |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> if ( A < 0 , -u 1 , 1 ) e. CC ) |
66 |
63 8
|
ifcli |
|- if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) e. CC |
67 |
66
|
a1i |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) e. CC ) |
68 |
|
nnabscl |
|- ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN ) |
69 |
68
|
3adant1 |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN ) |
70 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
71 |
69 70
|
eleqtrdi |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. ( ZZ>= ` 1 ) ) |
72 |
|
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 ) ) |
73 |
72
|
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 ) |
74 |
|
elfznn |
|- ( x e. ( 1 ... ( abs ` N ) ) -> x e. NN ) |
75 |
|
ffvelrn |
|- ( ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) : NN --> ZZ /\ x e. NN ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ` x ) e. ZZ ) |
76 |
73 74 75
|
syl2an |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ x e. ( 1 ... ( abs ` N ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ` x ) e. ZZ ) |
77 |
|
zmulcl |
|- ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ ) |
78 |
77
|
adantl |
|- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x x. y ) e. ZZ ) |
79 |
71 76 78
|
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. ZZ ) |
80 |
79
|
zcnd |
|- ( ( 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 ) |
81 |
65 67 80
|
mulassd |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( ( if ( A < 0 , -u 1 , 1 ) x. 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 ) ) ) = ( if ( A < 0 , -u 1 , 1 ) x. ( 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 ) ) ) ) ) |
82 |
62 81
|
eqtrd |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) ) ) ` ( abs ` -u N ) ) ) = ( if ( A < 0 , -u 1 , 1 ) x. ( 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 ) ) ) ) ) |
83 |
|
simp1 |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> A e. ZZ ) |
84 |
|
znegcl |
|- ( N e. ZZ -> -u N e. ZZ ) |
85 |
84
|
3ad2ant2 |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> -u N e. ZZ ) |
86 |
|
simp3 |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> N =/= 0 ) |
87 |
59 86
|
negne0d |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> -u N =/= 0 ) |
88 |
|
eqid |
|- ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) ) |
89 |
88
|
lgsval4 |
|- ( ( A e. ZZ /\ -u N e. ZZ /\ -u N =/= 0 ) -> ( A /L -u N ) = ( if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) ) ) ` ( abs ` -u N ) ) ) ) |
90 |
83 85 87 89
|
syl3anc |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( A /L -u N ) = ( if ( ( -u N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt -u N ) ) , 1 ) ) ) ` ( abs ` -u N ) ) ) ) |
91 |
72
|
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 ) ) ) ) |
92 |
91
|
oveq2d |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( if ( A < 0 , -u 1 , 1 ) x. ( A /L N ) ) = ( if ( A < 0 , -u 1 , 1 ) x. ( 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 ) ) ) ) ) |
93 |
82 90 92
|
3eqtr4d |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( A /L -u N ) = ( if ( A < 0 , -u 1 , 1 ) x. ( A /L N ) ) ) |