Metamath Proof Explorer

Theorem lgsdi

Description: The Legendre symbol is completely multiplicative in its right argument. Generalization of theorem 9.9(b) in ApostolNT p. 188 (which assumes that M and N are odd positive integers). (Contributed by Mario Carneiro, 5-Feb-2015)

Ref Expression
Assertion lgsdi 
|- ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( A /L ( M x. N ) ) = ( ( A /L M ) x. ( A /L N ) ) )

Proof

Step Hyp Ref Expression
1 3anrot 
 |-  ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) <-> ( M e. ZZ /\ N e. ZZ /\ A e. ZZ ) )
2 lgsdilem 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ A e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> if ( ( A < 0 /\ ( M x. N ) < 0 ) , -u 1 , 1 ) = ( if ( ( A < 0 /\ M < 0 ) , -u 1 , 1 ) x. if ( ( A < 0 /\ N < 0 ) , -u 1 , 1 ) ) )
3 1 2 sylanb 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> if ( ( A < 0 /\ ( M x. N ) < 0 ) , -u 1 , 1 ) = ( if ( ( A < 0 /\ M < 0 ) , -u 1 , 1 ) x. if ( ( A < 0 /\ N < 0 ) , -u 1 , 1 ) ) )
4 ancom 
 |-  ( ( ( M x. N ) < 0 /\ A < 0 ) <-> ( A < 0 /\ ( M x. N ) < 0 ) )
5 ifbi 
 |-  ( ( ( ( M x. N ) < 0 /\ A < 0 ) <-> ( A < 0 /\ ( M x. N ) < 0 ) ) -> if ( ( ( M x. N ) < 0 /\ A < 0 ) , -u 1 , 1 ) = if ( ( A < 0 /\ ( M x. N ) < 0 ) , -u 1 , 1 ) )
6 4 5 ax-mp 
 |-  if ( ( ( M x. N ) < 0 /\ A < 0 ) , -u 1 , 1 ) = if ( ( A < 0 /\ ( M x. N ) < 0 ) , -u 1 , 1 )
7 ancom 
 |-  ( ( M < 0 /\ A < 0 ) <-> ( A < 0 /\ M < 0 ) )
8 ifbi 
 |-  ( ( ( M < 0 /\ A < 0 ) <-> ( A < 0 /\ M < 0 ) ) -> if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) = if ( ( A < 0 /\ M < 0 ) , -u 1 , 1 ) )
9 7 8 ax-mp 
 |-  if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) = if ( ( A < 0 /\ M < 0 ) , -u 1 , 1 )
10 ancom 
 |-  ( ( N < 0 /\ A < 0 ) <-> ( A < 0 /\ N < 0 ) )
11 ifbi 
 |-  ( ( ( N < 0 /\ A < 0 ) <-> ( A < 0 /\ N < 0 ) ) -> if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) = if ( ( A < 0 /\ N < 0 ) , -u 1 , 1 ) )
12 10 11 ax-mp 
 |-  if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) = if ( ( A < 0 /\ N < 0 ) , -u 1 , 1 )
13 9 12 oveq12i 
 |-  ( if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) = ( if ( ( A < 0 /\ M < 0 ) , -u 1 , 1 ) x. if ( ( A < 0 /\ N < 0 ) , -u 1 , 1 ) )
14 3 6 13 3eqtr4g 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> if ( ( ( M x. N ) < 0 /\ A < 0 ) , -u 1 , 1 ) = ( if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) x. if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) ) )
15 simpl2 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> M e. ZZ )
16 simpl3 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> N e. ZZ )
17 15 16 zmulcld 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( M x. N ) e. ZZ )
18 15 zcnd 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> M e. CC )
19 16 zcnd 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> N e. CC )
20 simprl 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> M =/= 0 )
21 simprr 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> N =/= 0 )
22 18 19 20 21 mulne0d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( M x. N ) =/= 0 )
23 nnabscl 
 |-  ( ( ( M x. N ) e. ZZ /\ ( M x. N ) =/= 0 ) -> ( abs ` ( M x. N ) ) e. NN )
24 17 22 23 syl2anc 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( abs ` ( M x. N ) ) e. NN )
25 nnuz 
 |-  NN = ( ZZ>= ` 1 )
26 24 25 eleqtrdi 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( abs ` ( M x. N ) ) e. ( ZZ>= ` 1 ) )
27 simpl1 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> A e. ZZ )
28 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) )
29 28 lgsfcl3 
 |-  ( ( A e. ZZ /\ M e. ZZ /\ M =/= 0 ) -> ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) : NN --> ZZ )
30 27 15 20 29 syl3anc 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) : NN --> ZZ )
31 elfznn 
 |-  ( k e. ( 1 ... ( abs ` ( M x. N ) ) ) -> k e. NN )
32 ffvelrn 
 |-  ( ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) : NN --> ZZ /\ k e. NN ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ` k ) e. ZZ )
33 30 31 32 syl2an 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ` k ) e. ZZ )
34 33 zcnd 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ` k ) e. CC )
35 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 ) )
36 35 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 )
37 27 16 21 36 syl3anc 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) : NN --> ZZ )
38 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 )
39 37 31 38 syl2an 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ` k ) e. ZZ )
40 39 zcnd 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ` k ) e. CC )
41 simpr 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> k e. Prime )
42 15 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> M e. ZZ )
43 20 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> M =/= 0 )
44 16 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> N e. ZZ )
45 21 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> N =/= 0 )
46 pcmul 
 |-  ( ( k e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( k pCnt ( M x. N ) ) = ( ( k pCnt M ) + ( k pCnt N ) ) )
47 41 42 43 44 45 46 syl122anc 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( k pCnt ( M x. N ) ) = ( ( k pCnt M ) + ( k pCnt N ) ) )
48 47 oveq2d 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) = ( ( A /L k ) ^ ( ( k pCnt M ) + ( k pCnt N ) ) ) )
49 27 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> A e. ZZ )
50 prmz 
 |-  ( k e. Prime -> k e. ZZ )
51 50 adantl 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> k e. ZZ )
52 lgscl 
 |-  ( ( A e. ZZ /\ k e. ZZ ) -> ( A /L k ) e. ZZ )
53 49 51 52 syl2anc 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( A /L k ) e. ZZ )
54 53 zcnd 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( A /L k ) e. CC )
55 pczcl 
 |-  ( ( k e. Prime /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( k pCnt N ) e. NN0 )
56 41 44 45 55 syl12anc 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( k pCnt N ) e. NN0 )
57 pczcl 
 |-  ( ( k e. Prime /\ ( M e. ZZ /\ M =/= 0 ) ) -> ( k pCnt M ) e. NN0 )
58 41 42 43 57 syl12anc 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( k pCnt M ) e. NN0 )
59 54 56 58 expaddd 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( ( A /L k ) ^ ( ( k pCnt M ) + ( k pCnt N ) ) ) = ( ( ( A /L k ) ^ ( k pCnt M ) ) x. ( ( A /L k ) ^ ( k pCnt N ) ) ) )
60 48 59 eqtrd 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) = ( ( ( A /L k ) ^ ( k pCnt M ) ) x. ( ( A /L k ) ^ ( k pCnt N ) ) ) )
61 iftrue 
 |-  ( k e. Prime -> if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) = ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) )
62 61 adantl 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) = ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) )
63 iftrue 
 |-  ( k e. Prime -> if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) = ( ( A /L k ) ^ ( k pCnt M ) ) )
64 iftrue 
 |-  ( k e. Prime -> if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) = ( ( A /L k ) ^ ( k pCnt N ) ) )
65 63 64 oveq12d 
 |-  ( k e. Prime -> ( if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) x. if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) ) = ( ( ( A /L k ) ^ ( k pCnt M ) ) x. ( ( A /L k ) ^ ( k pCnt N ) ) ) )
66 65 adantl 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) x. if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) ) = ( ( ( A /L k ) ^ ( k pCnt M ) ) x. ( ( A /L k ) ^ ( k pCnt N ) ) ) )
67 60 62 66 3eqtr4rd 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ k e. Prime ) -> ( if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) x. if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) )
68 1t1e1 
 |-  ( 1 x. 1 ) = 1
69 iffalse 
 |-  ( -. k e. Prime -> if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) = 1 )
70 iffalse 
 |-  ( -. k e. Prime -> if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) = 1 )
71 69 70 oveq12d 
 |-  ( -. k e. Prime -> ( if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) x. if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) ) = ( 1 x. 1 ) )
72 iffalse 
 |-  ( -. k e. Prime -> if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) = 1 )
73 68 71 72 3eqtr4a 
 |-  ( -. k e. Prime -> ( if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) x. if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) )
74 73 adantl 
 |-  ( ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) /\ -. k e. Prime ) -> ( if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) x. if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) )
75 67 74 pm2.61dan 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) -> ( if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) x. if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) )
76 31 adantl 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) -> k e. NN )
77 eleq1w 
 |-  ( n = k -> ( n e. Prime <-> k e. Prime ) )
78 oveq2 
 |-  ( n = k -> ( A /L n ) = ( A /L k ) )
79 oveq1 
 |-  ( n = k -> ( n pCnt M ) = ( k pCnt M ) )
80 78 79 oveq12d 
 |-  ( n = k -> ( ( A /L n ) ^ ( n pCnt M ) ) = ( ( A /L k ) ^ ( k pCnt M ) ) )
81 77 80 ifbieq1d 
 |-  ( n = k -> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) )
82 ovex 
 |-  ( ( A /L k ) ^ ( k pCnt M ) ) e. _V
83 1ex 
 |-  1 e. _V
84 82 83 ifex 
 |-  if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) e. _V
85 81 28 84 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ` k ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) )
86 oveq1 
 |-  ( n = k -> ( n pCnt N ) = ( k pCnt N ) )
87 78 86 oveq12d 
 |-  ( n = k -> ( ( A /L n ) ^ ( n pCnt N ) ) = ( ( A /L k ) ^ ( k pCnt N ) ) )
88 77 87 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 ) )
89 ovex 
 |-  ( ( A /L k ) ^ ( k pCnt N ) ) e. _V
90 89 83 ifex 
 |-  if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) e. _V
91 88 35 90 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 ) )
92 85 91 oveq12d 
 |-  ( k e. NN -> ( ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ` k ) x. ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ` k ) ) = ( if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) x. if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) ) )
93 76 92 syl 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) -> ( ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ` k ) x. ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ` k ) ) = ( if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt M ) ) , 1 ) x. if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt N ) ) , 1 ) ) )
94 oveq1 
 |-  ( n = k -> ( n pCnt ( M x. N ) ) = ( k pCnt ( M x. N ) ) )
95 78 94 oveq12d 
 |-  ( n = k -> ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) = ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) )
96 77 95 ifbieq1d 
 |-  ( n = k -> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) )
97 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) )
98 ovex 
 |-  ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) e. _V
99 98 83 ifex 
 |-  if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) e. _V
100 96 97 99 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) ) ` k ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) )
101 76 100 syl 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) ) ` k ) = if ( k e. Prime , ( ( A /L k ) ^ ( k pCnt ( M x. N ) ) ) , 1 ) )
102 75 93 101 3eqtr4rd 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` ( M x. N ) ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) ) ` k ) = ( ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ` k ) x. ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ` k ) ) )
103 26 34 40 102 prodfmul 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) = ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) ) )
104 27 15 16 20 21 28 lgsdilem2 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` M ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) )
105 27 16 15 21 20 35 lgsdilem2 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` N ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` ( N x. M ) ) ) )
106 18 19 mulcomd 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( M x. N ) = ( N x. M ) )
107 106 fveq2d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( abs ` ( M x. N ) ) = ( abs ` ( N x. M ) ) )
108 107 fveq2d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` ( N x. M ) ) ) )
109 105 108 eqtr4d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` N ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) )
110 104 109 oveq12d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` M ) ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` N ) ) ) = ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) ) )
111 103 110 eqtr4d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) = ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` M ) ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` N ) ) ) )
112 14 111 oveq12d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( if ( ( ( M x. N ) < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) ) = ( ( if ( ( M < 0 /\ 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 M ) ) , 1 ) ) ) ` ( abs ` M ) ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` N ) ) ) ) )
113 97 lgsval4 
 |-  ( ( A e. ZZ /\ ( M x. N ) e. ZZ /\ ( M x. N ) =/= 0 ) -> ( A /L ( M x. N ) ) = ( if ( ( ( M x. N ) < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) ) )
114 27 17 22 113 syl3anc 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( A /L ( M x. N ) ) = ( if ( ( ( M x. N ) < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt ( M x. N ) ) ) , 1 ) ) ) ` ( abs ` ( M x. N ) ) ) ) )
115 28 lgsval4 
 |-  ( ( A e. ZZ /\ M e. ZZ /\ M =/= 0 ) -> ( A /L M ) = ( if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` M ) ) ) )
116 27 15 20 115 syl3anc 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( A /L M ) = ( if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` M ) ) ) )
117 35 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 ) ) ) )
118 27 16 21 117 syl3anc 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ 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 ) ) ) )
119 116 118 oveq12d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( ( A /L M ) x. ( A /L N ) ) = ( ( if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` M ) ) ) 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 ) ) ) ) )
120 neg1cn 
 |-  -u 1 e. CC
121 ax-1cn 
 |-  1 e. CC
122 120 121 ifcli 
 |-  if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) e. CC
123 122 a1i 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) e. CC )
124 nnabscl 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( abs ` M ) e. NN )
125 15 20 124 syl2anc 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( abs ` M ) e. NN )
126 125 25 eleqtrdi 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( abs ` M ) e. ( ZZ>= ` 1 ) )
127 elfznn 
 |-  ( k e. ( 1 ... ( abs ` M ) ) -> k e. NN )
128 30 127 32 syl2an 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` M ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ` k ) e. ZZ )
129 128 zcnd 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` M ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ` k ) e. CC )
130 mulcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
131 130 adantl 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
132 126 129 131 seqcl 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` M ) ) e. CC )
133 120 121 ifcli 
 |-  if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) e. CC
134 133 a1i 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) e. CC )
135 nnabscl 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN )
136 16 21 135 syl2anc 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( abs ` N ) e. NN )
137 136 25 eleqtrdi 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( abs ` N ) e. ( ZZ>= ` 1 ) )
138 elfznn 
 |-  ( k e. ( 1 ... ( abs ` N ) ) -> k e. NN )
139 37 138 38 syl2an 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` N ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ` k ) e. ZZ )
140 139 zcnd 
 |-  ( ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) /\ k e. ( 1 ... ( abs ` N ) ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ` k ) e. CC )
141 137 140 131 seqcl 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` N ) ) e. CC )
142 123 132 134 141 mul4d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( ( if ( ( M < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt M ) ) , 1 ) ) ) ` ( abs ` M ) ) ) 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 ( ( M < 0 /\ 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 M ) ) , 1 ) ) ) ` ( abs ` M ) ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` N ) ) ) ) )
143 119 142 eqtrd 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( ( A /L M ) x. ( A /L N ) ) = ( ( if ( ( M < 0 /\ 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 M ) ) , 1 ) ) ) ` ( abs ` M ) ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` ( abs ` N ) ) ) ) )
144 112 114 143 3eqtr4d 
 |-  ( ( ( A e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( A /L ( M x. N ) ) = ( ( A /L M ) x. ( A /L N ) ) )