Metamath Proof Explorer

Theorem lgsdir2

Description: The Legendre symbol is completely multiplicative at 2 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsdir2 ⊢A∈ℤ∧B∈ℤ→A⁢B/L2=A/L2⁢B/L2

Proof

Step Hyp Ref Expression
1 0cn ⊢0∈ℂ
2 ax-1cn ⊢1∈ℂ
3 neg1cn ⊢−1∈ℂ
4 2 3 ifcli ⊢ifBmod8∈171−1∈ℂ
5 1 4 ifcli ⊢if2∥B0ifBmod8∈171−1∈ℂ
6 5 mul02i ⊢0⋅if2∥B0ifBmod8∈171−1=0
7 iftrue ⊢2∥A→if2∥A0ifAmod8∈171−1=0
8 7 adantl ⊢A∈ℤ∧B∈ℤ∧2∥A→if2∥A0ifAmod8∈171−1=0
9 8 oveq1d ⊢A∈ℤ∧B∈ℤ∧2∥A→if2∥A0ifAmod8∈171−1⁢if2∥B0ifBmod8∈171−1=0⋅if2∥B0ifBmod8∈171−1
10 2z ⊢2∈ℤ
11 dvdsmultr1 ⊢2∈ℤ∧A∈ℤ∧B∈ℤ→2∥A→2∥A⁢B
12 10 11 mp3an1 ⊢A∈ℤ∧B∈ℤ→2∥A→2∥A⁢B
13 12 imp ⊢A∈ℤ∧B∈ℤ∧2∥A→2∥A⁢B
14 13 iftrued ⊢A∈ℤ∧B∈ℤ∧2∥A→if2∥A⁢B0ifA⁢Bmod8∈171−1=0
15 6 9 14 3eqtr4a ⊢A∈ℤ∧B∈ℤ∧2∥A→if2∥A0ifAmod8∈171−1⁢if2∥B0ifBmod8∈171−1=if2∥A⁢B0ifA⁢Bmod8∈171−1
16 2 3 ifcli ⊢ifAmod8∈171−1∈ℂ
17 1 16 ifcli ⊢if2∥A0ifAmod8∈171−1∈ℂ
18 17 mul01i ⊢if2∥A0ifAmod8∈171−1⋅0=0
19 iftrue ⊢2∥B→if2∥B0ifBmod8∈171−1=0
20 19 adantl ⊢A∈ℤ∧B∈ℤ∧2∥B→if2∥B0ifBmod8∈171−1=0
21 20 oveq2d ⊢A∈ℤ∧B∈ℤ∧2∥B→if2∥A0ifAmod8∈171−1⁢if2∥B0ifBmod8∈171−1=if2∥A0ifAmod8∈171−1⋅0
22 dvdsmultr2 ⊢2∈ℤ∧A∈ℤ∧B∈ℤ→2∥B→2∥A⁢B
23 10 22 mp3an1 ⊢A∈ℤ∧B∈ℤ→2∥B→2∥A⁢B
24 23 imp ⊢A∈ℤ∧B∈ℤ∧2∥B→2∥A⁢B
25 24 iftrued ⊢A∈ℤ∧B∈ℤ∧2∥B→if2∥A⁢B0ifA⁢Bmod8∈171−1=0
26 18 21 25 3eqtr4a ⊢A∈ℤ∧B∈ℤ∧2∥B→if2∥A0ifAmod8∈171−1⁢if2∥B0ifBmod8∈171−1=if2∥A⁢B0ifA⁢Bmod8∈171−1
27 4 mullidi ⊢1⁢ifBmod8∈171−1=ifBmod8∈171−1
28 iftrue ⊢Amod8∈17→ifAmod8∈171−1=1
29 28 adantl ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Amod8∈17→ifAmod8∈171−1=1
30 29 oveq1d ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Amod8∈17→ifAmod8∈171−1⁢ifBmod8∈171−1=1⁢ifBmod8∈171−1
31 lgsdir2lem4 ⊢A∈ℤ∧B∈ℤ∧Amod8∈17→A⁢Bmod8∈17↔Bmod8∈17
32 31 adantlr ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Amod8∈17→A⁢Bmod8∈17↔Bmod8∈17
33 32 ifbid ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Amod8∈17→ifA⁢Bmod8∈171−1=ifBmod8∈171−1
34 27 30 33 3eqtr4a ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Amod8∈17→ifAmod8∈171−1⁢ifBmod8∈171−1=ifA⁢Bmod8∈171−1
35 16 mulridi ⊢ifAmod8∈171−1⋅1=ifAmod8∈171−1
36 iftrue ⊢Bmod8∈17→ifBmod8∈171−1=1
37 36 adantl ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Bmod8∈17→ifBmod8∈171−1=1
38 37 oveq2d ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Bmod8∈17→ifAmod8∈171−1⁢ifBmod8∈171−1=ifAmod8∈171−1⋅1
39 zcn ⊢A∈ℤ→A∈ℂ
40 zcn ⊢B∈ℤ→B∈ℂ
41 mulcom ⊢A∈ℂ∧B∈ℂ→A⁢B=B⁢A
42 39 40 41 syl2an ⊢A∈ℤ∧B∈ℤ→A⁢B=B⁢A
43 42 ad2antrr ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Bmod8∈17→A⁢B=B⁢A
44 43 oveq1d ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Bmod8∈17→A⁢Bmod8=B⁢Amod8
45 44 eleq1d ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Bmod8∈17→A⁢Bmod8∈17↔B⁢Amod8∈17
46 lgsdir2lem4 ⊢B∈ℤ∧A∈ℤ∧Bmod8∈17→B⁢Amod8∈17↔Amod8∈17
47 46 ancom1s ⊢A∈ℤ∧B∈ℤ∧Bmod8∈17→B⁢Amod8∈17↔Amod8∈17
48 47 adantlr ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Bmod8∈17→B⁢Amod8∈17↔Amod8∈17
49 45 48 bitrd ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Bmod8∈17→A⁢Bmod8∈17↔Amod8∈17
50 49 ifbid ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Bmod8∈17→ifA⁢Bmod8∈171−1=ifAmod8∈171−1
51 35 38 50 3eqtr4a ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Bmod8∈17→ifAmod8∈171−1⁢ifBmod8∈171−1=ifA⁢Bmod8∈171−1
52 neg1mulneg1e1 ⊢-1⁢-1=1
53 iffalse ⊢¬Amod8∈17→ifAmod8∈171−1=−1
54 iffalse ⊢¬Bmod8∈17→ifBmod8∈171−1=−1
55 53 54 oveqan12d ⊢¬Amod8∈17∧¬Bmod8∈17→ifAmod8∈171−1⁢ifBmod8∈171−1=-1⁢-1
56 55 adantl ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧¬Amod8∈17∧¬Bmod8∈17→ifAmod8∈171−1⁢ifBmod8∈171−1=-1⁢-1
57 lgsdir2lem3 ⊢A∈ℤ∧¬2∥A→Amod8∈17∪35
58 57 ad2ant2r ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B→Amod8∈17∪35
59 elun ⊢Amod8∈17∪35↔Amod8∈17∨Amod8∈35
60 58 59 sylib ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B→Amod8∈17∨Amod8∈35
61 60 orcanai ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧¬Amod8∈17→Amod8∈35
62 lgsdir2lem3 ⊢B∈ℤ∧¬2∥B→Bmod8∈17∪35
63 62 ad2ant2l ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B→Bmod8∈17∪35
64 elun ⊢Bmod8∈17∪35↔Bmod8∈17∨Bmod8∈35
65 63 64 sylib ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B→Bmod8∈17∨Bmod8∈35
66 65 orcanai ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧¬Bmod8∈17→Bmod8∈35
67 61 66 anim12dan ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧¬Amod8∈17∧¬Bmod8∈17→Amod8∈35∧Bmod8∈35
68 lgsdir2lem5 ⊢A∈ℤ∧B∈ℤ∧Amod8∈35∧Bmod8∈35→A⁢Bmod8∈17
69 68 adantlr ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧Amod8∈35∧Bmod8∈35→A⁢Bmod8∈17
70 67 69 syldan ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧¬Amod8∈17∧¬Bmod8∈17→A⁢Bmod8∈17
71 70 iftrued ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧¬Amod8∈17∧¬Bmod8∈17→ifA⁢Bmod8∈171−1=1
72 52 56 71 3eqtr4a ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B∧¬Amod8∈17∧¬Bmod8∈17→ifAmod8∈171−1⁢ifBmod8∈171−1=ifA⁢Bmod8∈171−1
73 34 51 72 pm2.61ddan ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B→ifAmod8∈171−1⁢ifBmod8∈171−1=ifA⁢Bmod8∈171−1
74 iffalse ⊢¬2∥A→if2∥A0ifAmod8∈171−1=ifAmod8∈171−1
75 iffalse ⊢¬2∥B→if2∥B0ifBmod8∈171−1=ifBmod8∈171−1
76 74 75 oveqan12d ⊢¬2∥A∧¬2∥B→if2∥A0ifAmod8∈171−1⁢if2∥B0ifBmod8∈171−1=ifAmod8∈171−1⁢ifBmod8∈171−1
77 76 adantl ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B→if2∥A0ifAmod8∈171−1⁢if2∥B0ifBmod8∈171−1=ifAmod8∈171−1⁢ifBmod8∈171−1
78 ioran ⊢¬2∥A∨2∥B↔¬2∥A∧¬2∥B
79 2prm ⊢2∈ℙ
80 euclemma ⊢2∈ℙ∧A∈ℤ∧B∈ℤ→2∥A⁢B↔2∥A∨2∥B
81 79 80 mp3an1 ⊢A∈ℤ∧B∈ℤ→2∥A⁢B↔2∥A∨2∥B
82 81 notbid ⊢A∈ℤ∧B∈ℤ→¬2∥A⁢B↔¬2∥A∨2∥B
83 82 biimpar ⊢A∈ℤ∧B∈ℤ∧¬2∥A∨2∥B→¬2∥A⁢B
84 78 83 sylan2br ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B→¬2∥A⁢B
85 iffalse ⊢¬2∥A⁢B→if2∥A⁢B0ifA⁢Bmod8∈171−1=ifA⁢Bmod8∈171−1
86 84 85 syl ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B→if2∥A⁢B0ifA⁢Bmod8∈171−1=ifA⁢Bmod8∈171−1
87 73 77 86 3eqtr4d ⊢A∈ℤ∧B∈ℤ∧¬2∥A∧¬2∥B→if2∥A0ifAmod8∈171−1⁢if2∥B0ifBmod8∈171−1=if2∥A⁢B0ifA⁢Bmod8∈171−1
88 15 26 87 pm2.61ddan ⊢A∈ℤ∧B∈ℤ→if2∥A0ifAmod8∈171−1⁢if2∥B0ifBmod8∈171−1=if2∥A⁢B0ifA⁢Bmod8∈171−1
89 lgs2 ⊢A∈ℤ→A/L2=if2∥A0ifAmod8∈171−1
90 lgs2 ⊢B∈ℤ→B/L2=if2∥B0ifBmod8∈171−1
91 89 90 oveqan12d ⊢A∈ℤ∧B∈ℤ→A/L2⁢B/L2=if2∥A0ifAmod8∈171−1⁢if2∥B0ifBmod8∈171−1
92 zmulcl ⊢A∈ℤ∧B∈ℤ→A⁢B∈ℤ
93 lgs2 ⊢A⁢B∈ℤ→A⁢B/L2=if2∥A⁢B0ifA⁢Bmod8∈171−1
94 92 93 syl ⊢A∈ℤ∧B∈ℤ→A⁢B/L2=if2∥A⁢B0ifA⁢Bmod8∈171−1
95 88 91 94 3eqtr4rd ⊢A∈ℤ∧B∈ℤ→A⁢B/L2=A/L2⁢B/L2