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 AMNM0N0A/L M N=A/LMA/LN

Proof

Step Hyp Ref Expression
1 3anrot AMNMNA
2 lgsdilem MNAM0N0ifA<0 M N<011=ifA<0M<011ifA<0N<011
3 1 2 sylanb AMNM0N0ifA<0 M N<011=ifA<0M<011ifA<0N<011
4 ancom M N<0A<0A<0 M N<0
5 ifbi M N<0A<0A<0 M N<0if M N<0A<011=ifA<0 M N<011
6 4 5 ax-mp if M N<0A<011=ifA<0 M N<011
7 ancom M<0A<0A<0M<0
8 ifbi M<0A<0A<0M<0ifM<0A<011=ifA<0M<011
9 7 8 ax-mp ifM<0A<011=ifA<0M<011
10 ancom N<0A<0A<0N<0
11 ifbi N<0A<0A<0N<0ifN<0A<011=ifA<0N<011
12 10 11 ax-mp ifN<0A<011=ifA<0N<011
13 9 12 oveq12i ifM<0A<011ifN<0A<011=ifA<0M<011ifA<0N<011
14 3 6 13 3eqtr4g AMNM0N0if M N<0A<011=ifM<0A<011ifN<0A<011
15 simpl2 AMNM0N0M
16 simpl3 AMNM0N0N
17 15 16 zmulcld AMNM0N0 M N
18 15 zcnd AMNM0N0M
19 16 zcnd AMNM0N0N
20 simprl AMNM0N0M0
21 simprr AMNM0N0N0
22 18 19 20 21 mulne0d AMNM0N0 M N0
23 nnabscl M N M N0 M N
24 17 22 23 syl2anc AMNM0N0 M N
25 nnuz =1
26 24 25 eleqtrdi AMNM0N0 M N1
27 simpl1 AMNM0N0A
28 eqid nifnA/LnnpCntM1=nifnA/LnnpCntM1
29 28 lgsfcl3 AMM0nifnA/LnnpCntM1:
30 27 15 20 29 syl3anc AMNM0N0nifnA/LnnpCntM1:
31 elfznn k1 M Nk
32 ffvelrn nifnA/LnnpCntM1:knifnA/LnnpCntM1k
33 30 31 32 syl2an AMNM0N0k1 M NnifnA/LnnpCntM1k
34 33 zcnd AMNM0N0k1 M NnifnA/LnnpCntM1k
35 eqid nifnA/LnnpCntN1=nifnA/LnnpCntN1
36 35 lgsfcl3 ANN0nifnA/LnnpCntN1:
37 27 16 21 36 syl3anc AMNM0N0nifnA/LnnpCntN1:
38 ffvelrn nifnA/LnnpCntN1:knifnA/LnnpCntN1k
39 37 31 38 syl2an AMNM0N0k1 M NnifnA/LnnpCntN1k
40 39 zcnd AMNM0N0k1 M NnifnA/LnnpCntN1k
41 simpr AMNM0N0k1 M Nkk
42 15 ad2antrr AMNM0N0k1 M NkM
43 20 ad2antrr AMNM0N0k1 M NkM0
44 16 ad2antrr AMNM0N0k1 M NkN
45 21 ad2antrr AMNM0N0k1 M NkN0
46 pcmul kMM0NN0kpCnt M N=kpCntM+kpCntN
47 41 42 43 44 45 46 syl122anc AMNM0N0k1 M NkkpCnt M N=kpCntM+kpCntN
48 47 oveq2d AMNM0N0k1 M NkA/LkkpCnt M N=A/LkkpCntM+kpCntN
49 27 ad2antrr AMNM0N0k1 M NkA
50 prmz kk
51 50 adantl AMNM0N0k1 M Nkk
52 lgscl AkA/Lk
53 49 51 52 syl2anc AMNM0N0k1 M NkA/Lk
54 53 zcnd AMNM0N0k1 M NkA/Lk
55 pczcl kNN0kpCntN0
56 41 44 45 55 syl12anc AMNM0N0k1 M NkkpCntN0
57 pczcl kMM0kpCntM0
58 41 42 43 57 syl12anc AMNM0N0k1 M NkkpCntM0
59 54 56 58 expaddd AMNM0N0k1 M NkA/LkkpCntM+kpCntN=A/LkkpCntMA/LkkpCntN
60 48 59 eqtrd AMNM0N0k1 M NkA/LkkpCnt M N=A/LkkpCntMA/LkkpCntN
61 iftrue kifkA/LkkpCnt M N1=A/LkkpCnt M N
62 61 adantl AMNM0N0k1 M NkifkA/LkkpCnt M N1=A/LkkpCnt M N
63 iftrue kifkA/LkkpCntM1=A/LkkpCntM
64 iftrue kifkA/LkkpCntN1=A/LkkpCntN
65 63 64 oveq12d kifkA/LkkpCntM1ifkA/LkkpCntN1=A/LkkpCntMA/LkkpCntN
66 65 adantl AMNM0N0k1 M NkifkA/LkkpCntM1ifkA/LkkpCntN1=A/LkkpCntMA/LkkpCntN
67 60 62 66 3eqtr4rd AMNM0N0k1 M NkifkA/LkkpCntM1ifkA/LkkpCntN1=ifkA/LkkpCnt M N1
68 1t1e1 11=1
69 iffalse ¬kifkA/LkkpCntM1=1
70 iffalse ¬kifkA/LkkpCntN1=1
71 69 70 oveq12d ¬kifkA/LkkpCntM1ifkA/LkkpCntN1=11
72 iffalse ¬kifkA/LkkpCnt M N1=1
73 68 71 72 3eqtr4a ¬kifkA/LkkpCntM1ifkA/LkkpCntN1=ifkA/LkkpCnt M N1
74 73 adantl AMNM0N0k1 M N¬kifkA/LkkpCntM1ifkA/LkkpCntN1=ifkA/LkkpCnt M N1
75 67 74 pm2.61dan AMNM0N0k1 M NifkA/LkkpCntM1ifkA/LkkpCntN1=ifkA/LkkpCnt M N1
76 31 adantl AMNM0N0k1 M Nk
77 eleq1w n=knk
78 oveq2 n=kA/Ln=A/Lk
79 oveq1 n=knpCntM=kpCntM
80 78 79 oveq12d n=kA/LnnpCntM=A/LkkpCntM
81 77 80 ifbieq1d n=kifnA/LnnpCntM1=ifkA/LkkpCntM1
82 ovex A/LkkpCntMV
83 1ex 1V
84 82 83 ifex ifkA/LkkpCntM1V
85 81 28 84 fvmpt knifnA/LnnpCntM1k=ifkA/LkkpCntM1
86 oveq1 n=knpCntN=kpCntN
87 78 86 oveq12d n=kA/LnnpCntN=A/LkkpCntN
88 77 87 ifbieq1d n=kifnA/LnnpCntN1=ifkA/LkkpCntN1
89 ovex A/LkkpCntNV
90 89 83 ifex ifkA/LkkpCntN1V
91 88 35 90 fvmpt knifnA/LnnpCntN1k=ifkA/LkkpCntN1
92 85 91 oveq12d knifnA/LnnpCntM1knifnA/LnnpCntN1k=ifkA/LkkpCntM1ifkA/LkkpCntN1
93 76 92 syl AMNM0N0k1 M NnifnA/LnnpCntM1knifnA/LnnpCntN1k=ifkA/LkkpCntM1ifkA/LkkpCntN1
94 oveq1 n=knpCnt M N=kpCnt M N
95 78 94 oveq12d n=kA/LnnpCnt M N=A/LkkpCnt M N
96 77 95 ifbieq1d n=kifnA/LnnpCnt M N1=ifkA/LkkpCnt M N1
97 eqid nifnA/LnnpCnt M N1=nifnA/LnnpCnt M N1
98 ovex A/LkkpCnt M NV
99 98 83 ifex ifkA/LkkpCnt M N1V
100 96 97 99 fvmpt knifnA/LnnpCnt M N1k=ifkA/LkkpCnt M N1
101 76 100 syl AMNM0N0k1 M NnifnA/LnnpCnt M N1k=ifkA/LkkpCnt M N1
102 75 93 101 3eqtr4rd AMNM0N0k1 M NnifnA/LnnpCnt M N1k=nifnA/LnnpCntM1knifnA/LnnpCntN1k
103 26 34 40 102 prodfmul AMNM0N0seq1×nifnA/LnnpCnt M N1 M N=seq1×nifnA/LnnpCntM1 M Nseq1×nifnA/LnnpCntN1 M N
104 27 15 16 20 21 28 lgsdilem2 AMNM0N0seq1×nifnA/LnnpCntM1M=seq1×nifnA/LnnpCntM1 M N
105 27 16 15 21 20 35 lgsdilem2 AMNM0N0seq1×nifnA/LnnpCntN1N=seq1×nifnA/LnnpCntN1 N M
106 18 19 mulcomd AMNM0N0 M N= N M
107 106 fveq2d AMNM0N0 M N= N M
108 107 fveq2d AMNM0N0seq1×nifnA/LnnpCntN1 M N=seq1×nifnA/LnnpCntN1 N M
109 105 108 eqtr4d AMNM0N0seq1×nifnA/LnnpCntN1N=seq1×nifnA/LnnpCntN1 M N
110 104 109 oveq12d AMNM0N0seq1×nifnA/LnnpCntM1Mseq1×nifnA/LnnpCntN1N=seq1×nifnA/LnnpCntM1 M Nseq1×nifnA/LnnpCntN1 M N
111 103 110 eqtr4d AMNM0N0seq1×nifnA/LnnpCnt M N1 M N=seq1×nifnA/LnnpCntM1Mseq1×nifnA/LnnpCntN1N
112 14 111 oveq12d AMNM0N0if M N<0A<011seq1×nifnA/LnnpCnt M N1 M N=ifM<0A<011ifN<0A<011seq1×nifnA/LnnpCntM1Mseq1×nifnA/LnnpCntN1N
113 97 lgsval4 A M N M N0A/L M N=if M N<0A<011seq1×nifnA/LnnpCnt M N1 M N
114 27 17 22 113 syl3anc AMNM0N0A/L M N=if M N<0A<011seq1×nifnA/LnnpCnt M N1 M N
115 28 lgsval4 AMM0A/LM=ifM<0A<011seq1×nifnA/LnnpCntM1M
116 27 15 20 115 syl3anc AMNM0N0A/LM=ifM<0A<011seq1×nifnA/LnnpCntM1M
117 35 lgsval4 ANN0A/LN=ifN<0A<011seq1×nifnA/LnnpCntN1N
118 27 16 21 117 syl3anc AMNM0N0A/LN=ifN<0A<011seq1×nifnA/LnnpCntN1N
119 116 118 oveq12d AMNM0N0A/LMA/LN=ifM<0A<011seq1×nifnA/LnnpCntM1MifN<0A<011seq1×nifnA/LnnpCntN1N
120 neg1cn 1
121 ax-1cn 1
122 120 121 ifcli ifM<0A<011
123 122 a1i AMNM0N0ifM<0A<011
124 nnabscl MM0M
125 15 20 124 syl2anc AMNM0N0M
126 125 25 eleqtrdi AMNM0N0M1
127 elfznn k1Mk
128 30 127 32 syl2an AMNM0N0k1MnifnA/LnnpCntM1k
129 128 zcnd AMNM0N0k1MnifnA/LnnpCntM1k
130 mulcl kxkx
131 130 adantl AMNM0N0kxkx
132 126 129 131 seqcl AMNM0N0seq1×nifnA/LnnpCntM1M
133 120 121 ifcli ifN<0A<011
134 133 a1i AMNM0N0ifN<0A<011
135 nnabscl NN0N
136 16 21 135 syl2anc AMNM0N0N
137 136 25 eleqtrdi AMNM0N0N1
138 elfznn k1Nk
139 37 138 38 syl2an AMNM0N0k1NnifnA/LnnpCntN1k
140 139 zcnd AMNM0N0k1NnifnA/LnnpCntN1k
141 137 140 131 seqcl AMNM0N0seq1×nifnA/LnnpCntN1N
142 123 132 134 141 mul4d AMNM0N0ifM<0A<011seq1×nifnA/LnnpCntM1MifN<0A<011seq1×nifnA/LnnpCntN1N=ifM<0A<011ifN<0A<011seq1×nifnA/LnnpCntM1Mseq1×nifnA/LnnpCntN1N
143 119 142 eqtrd AMNM0N0A/LMA/LN=ifM<0A<011ifN<0A<011seq1×nifnA/LnnpCntM1Mseq1×nifnA/LnnpCntN1N
144 112 114 143 3eqtr4d AMNM0N0A/L M N=A/LMA/LN