Metamath Proof Explorer


Theorem lgsdir

Description: The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in ApostolNT p. 188 (which assumes that A and B are odd positive integers). Together with lgsqr this implies that the product of two quadratic residues or nonresidues is a residue, and the product of a residue and a nonresidue is a nonresidue. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsdir ABNA0B0AB/LN=A/LNB/LN

Proof

Step Hyp Ref Expression
1 ax-1cn 1
2 0cn 0
3 1 2 ifcli ifB2=110
4 3 mulid2i 1ifB2=110=ifB2=110
5 iftrue A2=1ifA2=110=1
6 5 adantl ABNA0B0N=0A2=1ifA2=110=1
7 6 oveq1d ABNA0B0N=0A2=1ifA2=110ifB2=110=1ifB2=110
8 simpl1 ABNA0B0A
9 8 zcnd ABNA0B0A
10 9 ad2antrr ABNA0B0N=0A2=1A
11 simpl2 ABNA0B0B
12 11 zcnd ABNA0B0B
13 12 ad2antrr ABNA0B0N=0A2=1B
14 10 13 sqmuld ABNA0B0N=0A2=1AB2=A2B2
15 simpr ABNA0B0N=0A2=1A2=1
16 15 oveq1d ABNA0B0N=0A2=1A2B2=1B2
17 12 sqcld ABNA0B0B2
18 17 ad2antrr ABNA0B0N=0A2=1B2
19 18 mulid2d ABNA0B0N=0A2=11B2=B2
20 14 16 19 3eqtrd ABNA0B0N=0A2=1AB2=B2
21 20 eqeq1d ABNA0B0N=0A2=1AB2=1B2=1
22 21 ifbid ABNA0B0N=0A2=1ifAB2=110=ifB2=110
23 4 7 22 3eqtr4a ABNA0B0N=0A2=1ifA2=110ifB2=110=ifAB2=110
24 3 mul02i 0ifB2=110=0
25 iffalse ¬A2=1ifA2=110=0
26 25 adantl ABNA0B0N=0¬A2=1ifA2=110=0
27 26 oveq1d ABNA0B0N=0¬A2=1ifA2=110ifB2=110=0ifB2=110
28 dvdsmul1 ABAAB
29 8 11 28 syl2anc ABNA0B0AAB
30 8 11 zmulcld ABNA0B0AB
31 dvdssq AABAABA2AB2
32 8 30 31 syl2anc ABNA0B0AABA2AB2
33 29 32 mpbid ABNA0B0A2AB2
34 33 adantr ABNA0B0N=0A2AB2
35 breq2 AB2=1A2AB2A21
36 34 35 syl5ibcom ABNA0B0N=0AB2=1A21
37 simprl ABNA0B0A0
38 37 neneqd ABNA0B0¬A=0
39 sqeq0 AA2=0A=0
40 9 39 syl ABNA0B0A2=0A=0
41 38 40 mtbird ABNA0B0¬A2=0
42 zsqcl2 AA20
43 8 42 syl ABNA0B0A20
44 elnn0 A20A2A2=0
45 43 44 sylib ABNA0B0A2A2=0
46 45 ord ABNA0B0¬A2A2=0
47 41 46 mt3d ABNA0B0A2
48 47 adantr ABNA0B0N=0A2
49 48 nnzd ABNA0B0N=0A2
50 1nn 1
51 dvdsle A21A21A21
52 49 50 51 sylancl ABNA0B0N=0A21A21
53 48 nnge1d ABNA0B0N=01A2
54 52 53 jctird ABNA0B0N=0A21A211A2
55 48 nnred ABNA0B0N=0A2
56 1re 1
57 letri3 A21A2=1A211A2
58 55 56 57 sylancl ABNA0B0N=0A2=1A211A2
59 54 58 sylibrd ABNA0B0N=0A21A2=1
60 36 59 syld ABNA0B0N=0AB2=1A2=1
61 60 con3dimp ABNA0B0N=0¬A2=1¬AB2=1
62 61 iffalsed ABNA0B0N=0¬A2=1ifAB2=110=0
63 24 27 62 3eqtr4a ABNA0B0N=0¬A2=1ifA2=110ifB2=110=ifAB2=110
64 23 63 pm2.61dan ABNA0B0N=0ifA2=110ifB2=110=ifAB2=110
65 oveq2 N=0A/LN=A/L0
66 lgs0 AA/L0=ifA2=110
67 8 66 syl ABNA0B0A/L0=ifA2=110
68 65 67 sylan9eqr ABNA0B0N=0A/LN=ifA2=110
69 oveq2 N=0B/LN=B/L0
70 lgs0 BB/L0=ifB2=110
71 11 70 syl ABNA0B0B/L0=ifB2=110
72 69 71 sylan9eqr ABNA0B0N=0B/LN=ifB2=110
73 68 72 oveq12d ABNA0B0N=0A/LNB/LN=ifA2=110ifB2=110
74 oveq2 N=0AB/LN=AB/L0
75 lgs0 ABAB/L0=ifAB2=110
76 30 75 syl ABNA0B0AB/L0=ifAB2=110
77 74 76 sylan9eqr ABNA0B0N=0AB/LN=ifAB2=110
78 64 73 77 3eqtr4rd ABNA0B0N=0AB/LN=A/LNB/LN
79 lgsdilem ABNA0B0ifN<0AB<011=ifN<0A<011ifN<0B<011
80 79 adantr ABNA0B0N0ifN<0AB<011=ifN<0A<011ifN<0B<011
81 simpl3 ABNA0B0N
82 nnabscl NN0N
83 81 82 sylan ABNA0B0N0N
84 nnuz =1
85 83 84 eleqtrdi ABNA0B0N0N1
86 simpll1 ABNA0B0N0A
87 simpll3 ABNA0B0N0N
88 simpr ABNA0B0N0N0
89 eqid nifnA/LnnpCntN1=nifnA/LnnpCntN1
90 89 lgsfcl3 ANN0nifnA/LnnpCntN1:
91 86 87 88 90 syl3anc ABNA0B0N0nifnA/LnnpCntN1:
92 elfznn k1Nk
93 ffvelrn nifnA/LnnpCntN1:knifnA/LnnpCntN1k
94 91 92 93 syl2an ABNA0B0N0k1NnifnA/LnnpCntN1k
95 94 zcnd ABNA0B0N0k1NnifnA/LnnpCntN1k
96 simpll2 ABNA0B0N0B
97 eqid nifnB/LnnpCntN1=nifnB/LnnpCntN1
98 97 lgsfcl3 BNN0nifnB/LnnpCntN1:
99 96 87 88 98 syl3anc ABNA0B0N0nifnB/LnnpCntN1:
100 ffvelrn nifnB/LnnpCntN1:knifnB/LnnpCntN1k
101 99 92 100 syl2an ABNA0B0N0k1NnifnB/LnnpCntN1k
102 101 zcnd ABNA0B0N0k1NnifnB/LnnpCntN1k
103 86 adantr ABNA0B0N0kA
104 96 adantr ABNA0B0N0kB
105 simpr ABNA0B0N0kk
106 lgsdirprm ABkAB/Lk=A/LkB/Lk
107 103 104 105 106 syl3anc ABNA0B0N0kAB/Lk=A/LkB/Lk
108 107 oveq1d ABNA0B0N0kAB/LkkpCntN=A/LkB/LkkpCntN
109 prmz kk
110 lgscl AkA/Lk
111 86 109 110 syl2an ABNA0B0N0kA/Lk
112 111 zcnd ABNA0B0N0kA/Lk
113 lgscl BkB/Lk
114 96 109 113 syl2an ABNA0B0N0kB/Lk
115 114 zcnd ABNA0B0N0kB/Lk
116 87 adantr ABNA0B0N0kN
117 88 adantr ABNA0B0N0kN0
118 pczcl kNN0kpCntN0
119 105 116 117 118 syl12anc ABNA0B0N0kkpCntN0
120 112 115 119 mulexpd ABNA0B0N0kA/LkB/LkkpCntN=A/LkkpCntNB/LkkpCntN
121 108 120 eqtrd ABNA0B0N0kAB/LkkpCntN=A/LkkpCntNB/LkkpCntN
122 iftrue kifkAB/LkkpCntN1=AB/LkkpCntN
123 122 adantl ABNA0B0N0kifkAB/LkkpCntN1=AB/LkkpCntN
124 iftrue kifkA/LkkpCntN1=A/LkkpCntN
125 iftrue kifkB/LkkpCntN1=B/LkkpCntN
126 124 125 oveq12d kifkA/LkkpCntN1ifkB/LkkpCntN1=A/LkkpCntNB/LkkpCntN
127 126 adantl ABNA0B0N0kifkA/LkkpCntN1ifkB/LkkpCntN1=A/LkkpCntNB/LkkpCntN
128 121 123 127 3eqtr4d ABNA0B0N0kifkAB/LkkpCntN1=ifkA/LkkpCntN1ifkB/LkkpCntN1
129 1t1e1 11=1
130 129 eqcomi 1=11
131 iffalse ¬kifkAB/LkkpCntN1=1
132 iffalse ¬kifkA/LkkpCntN1=1
133 iffalse ¬kifkB/LkkpCntN1=1
134 132 133 oveq12d ¬kifkA/LkkpCntN1ifkB/LkkpCntN1=11
135 130 131 134 3eqtr4a ¬kifkAB/LkkpCntN1=ifkA/LkkpCntN1ifkB/LkkpCntN1
136 135 adantl ABNA0B0N0¬kifkAB/LkkpCntN1=ifkA/LkkpCntN1ifkB/LkkpCntN1
137 128 136 pm2.61dan ABNA0B0N0ifkAB/LkkpCntN1=ifkA/LkkpCntN1ifkB/LkkpCntN1
138 137 adantr ABNA0B0N0k1NifkAB/LkkpCntN1=ifkA/LkkpCntN1ifkB/LkkpCntN1
139 92 adantl ABNA0B0N0k1Nk
140 eleq1w n=knk
141 oveq2 n=kAB/Ln=AB/Lk
142 oveq1 n=knpCntN=kpCntN
143 141 142 oveq12d n=kAB/LnnpCntN=AB/LkkpCntN
144 140 143 ifbieq1d n=kifnAB/LnnpCntN1=ifkAB/LkkpCntN1
145 eqid nifnAB/LnnpCntN1=nifnAB/LnnpCntN1
146 ovex AB/LkkpCntNV
147 1ex 1V
148 146 147 ifex ifkAB/LkkpCntN1V
149 144 145 148 fvmpt knifnAB/LnnpCntN1k=ifkAB/LkkpCntN1
150 139 149 syl ABNA0B0N0k1NnifnAB/LnnpCntN1k=ifkAB/LkkpCntN1
151 oveq2 n=kA/Ln=A/Lk
152 151 142 oveq12d n=kA/LnnpCntN=A/LkkpCntN
153 140 152 ifbieq1d n=kifnA/LnnpCntN1=ifkA/LkkpCntN1
154 ovex A/LkkpCntNV
155 154 147 ifex ifkA/LkkpCntN1V
156 153 89 155 fvmpt knifnA/LnnpCntN1k=ifkA/LkkpCntN1
157 139 156 syl ABNA0B0N0k1NnifnA/LnnpCntN1k=ifkA/LkkpCntN1
158 oveq2 n=kB/Ln=B/Lk
159 158 142 oveq12d n=kB/LnnpCntN=B/LkkpCntN
160 140 159 ifbieq1d n=kifnB/LnnpCntN1=ifkB/LkkpCntN1
161 ovex B/LkkpCntNV
162 161 147 ifex ifkB/LkkpCntN1V
163 160 97 162 fvmpt knifnB/LnnpCntN1k=ifkB/LkkpCntN1
164 139 163 syl ABNA0B0N0k1NnifnB/LnnpCntN1k=ifkB/LkkpCntN1
165 157 164 oveq12d ABNA0B0N0k1NnifnA/LnnpCntN1knifnB/LnnpCntN1k=ifkA/LkkpCntN1ifkB/LkkpCntN1
166 138 150 165 3eqtr4d ABNA0B0N0k1NnifnAB/LnnpCntN1k=nifnA/LnnpCntN1knifnB/LnnpCntN1k
167 85 95 102 166 prodfmul ABNA0B0N0seq1×nifnAB/LnnpCntN1N=seq1×nifnA/LnnpCntN1Nseq1×nifnB/LnnpCntN1N
168 80 167 oveq12d ABNA0B0N0ifN<0AB<011seq1×nifnAB/LnnpCntN1N=ifN<0A<011ifN<0B<011seq1×nifnA/LnnpCntN1Nseq1×nifnB/LnnpCntN1N
169 30 adantr ABNA0B0N0AB
170 145 lgsval4 ABNN0AB/LN=ifN<0AB<011seq1×nifnAB/LnnpCntN1N
171 169 87 88 170 syl3anc ABNA0B0N0AB/LN=ifN<0AB<011seq1×nifnAB/LnnpCntN1N
172 89 lgsval4 ANN0A/LN=ifN<0A<011seq1×nifnA/LnnpCntN1N
173 86 87 88 172 syl3anc ABNA0B0N0A/LN=ifN<0A<011seq1×nifnA/LnnpCntN1N
174 97 lgsval4 BNN0B/LN=ifN<0B<011seq1×nifnB/LnnpCntN1N
175 96 87 88 174 syl3anc ABNA0B0N0B/LN=ifN<0B<011seq1×nifnB/LnnpCntN1N
176 173 175 oveq12d ABNA0B0N0A/LNB/LN=ifN<0A<011seq1×nifnA/LnnpCntN1NifN<0B<011seq1×nifnB/LnnpCntN1N
177 neg1cn 1
178 177 1 ifcli ifN<0A<011
179 178 a1i ABNA0B0N0ifN<0A<011
180 mulcl kxkx
181 180 adantl ABNA0B0N0kxkx
182 85 95 181 seqcl ABNA0B0N0seq1×nifnA/LnnpCntN1N
183 177 1 ifcli ifN<0B<011
184 183 a1i ABNA0B0N0ifN<0B<011
185 85 102 181 seqcl ABNA0B0N0seq1×nifnB/LnnpCntN1N
186 179 182 184 185 mul4d ABNA0B0N0ifN<0A<011seq1×nifnA/LnnpCntN1NifN<0B<011seq1×nifnB/LnnpCntN1N=ifN<0A<011ifN<0B<011seq1×nifnA/LnnpCntN1Nseq1×nifnB/LnnpCntN1N
187 176 186 eqtrd ABNA0B0N0A/LNB/LN=ifN<0A<011ifN<0B<011seq1×nifnA/LnnpCntN1Nseq1×nifnB/LnnpCntN1N
188 168 171 187 3eqtr4d ABNA0B0N0AB/LN=A/LNB/LN
189 78 188 pm2.61dane ABNA0B0AB/LN=A/LNB/LN