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 / L 2 = A / L 2 ⁢ B / L 2

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 ax-1cn ⊢ 1 ∈ ℂ
3 neg1cn ⊢ − 1 ∈ ℂ
4 2 3 ifcli ⊢ if B mod 8 ∈ 1 7 1 − 1 ∈ ℂ
5 1 4 ifcli ⊢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 ∈ ℂ
6 5 mul02i ⊢ 0 ⋅ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = 0
7 iftrue ⊢ 2 ∥ A → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 = 0
8 7 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ 2 ∥ A → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 = 0
9 8 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ 2 ∥ A → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⁢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = 0 ⋅ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 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 → if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1 = 0
15 6 9 14 3eqtr4a ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ 2 ∥ A → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⁢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1
16 2 3 ifcli ⊢ if A mod 8 ∈ 1 7 1 − 1 ∈ ℂ
17 1 16 ifcli ⊢ if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ∈ ℂ
18 17 mul01i ⊢ if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⋅ 0 = 0
19 iftrue ⊢ 2 ∥ B → if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = 0
20 19 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ 2 ∥ B → if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = 0
21 20 oveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ 2 ∥ B → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⁢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 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 → if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1 = 0
26 18 21 25 3eqtr4a ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ 2 ∥ B → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⁢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1
27 4 mullidi ⊢ 1 ⁢ if B mod 8 ∈ 1 7 1 − 1 = if B mod 8 ∈ 1 7 1 − 1
28 iftrue ⊢ A mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 = 1
29 28 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ A mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 = 1
30 29 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ A mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 1 = 1 ⁢ if B mod 8 ∈ 1 7 1 − 1
31 lgsdir2lem4 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ A mod 8 ∈ 1 7 → A ⁢ B mod 8 ∈ 1 7 ↔ B mod 8 ∈ 1 7
32 31 adantlr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ A mod 8 ∈ 1 7 → A ⁢ B mod 8 ∈ 1 7 ↔ B mod 8 ∈ 1 7
33 32 ifbid ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ A mod 8 ∈ 1 7 → if A ⁢ B mod 8 ∈ 1 7 1 − 1 = if B mod 8 ∈ 1 7 1 − 1
34 27 30 33 3eqtr4a ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ A mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 1 = if A ⁢ B mod 8 ∈ 1 7 1 − 1
35 16 mulridi ⊢ if A mod 8 ∈ 1 7 1 − 1 ⋅ 1 = if A mod 8 ∈ 1 7 1 − 1
36 iftrue ⊢ B mod 8 ∈ 1 7 → if B mod 8 ∈ 1 7 1 − 1 = 1
37 36 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ B mod 8 ∈ 1 7 → if B mod 8 ∈ 1 7 1 − 1 = 1
38 37 oveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ B mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 1 = if A mod 8 ∈ 1 7 1 − 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 ∧ B mod 8 ∈ 1 7 → A ⁢ B = B ⁢ A
44 43 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ B mod 8 ∈ 1 7 → A ⁢ B mod 8 = B ⁢ A mod 8
45 44 eleq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ B mod 8 ∈ 1 7 → A ⁢ B mod 8 ∈ 1 7 ↔ B ⁢ A mod 8 ∈ 1 7
46 lgsdir2lem4 ⊢ B ∈ ℤ ∧ A ∈ ℤ ∧ B mod 8 ∈ 1 7 → B ⁢ A mod 8 ∈ 1 7 ↔ A mod 8 ∈ 1 7
47 46 ancom1s ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B mod 8 ∈ 1 7 → B ⁢ A mod 8 ∈ 1 7 ↔ A mod 8 ∈ 1 7
48 47 adantlr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ B mod 8 ∈ 1 7 → B ⁢ A mod 8 ∈ 1 7 ↔ A mod 8 ∈ 1 7
49 45 48 bitrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ B mod 8 ∈ 1 7 → A ⁢ B mod 8 ∈ 1 7 ↔ A mod 8 ∈ 1 7
50 49 ifbid ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ B mod 8 ∈ 1 7 → if A ⁢ B mod 8 ∈ 1 7 1 − 1 = if A mod 8 ∈ 1 7 1 − 1
51 35 38 50 3eqtr4a ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ B mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 1 = if A ⁢ B mod 8 ∈ 1 7 1 − 1
52 neg1mulneg1e1 ⊢ -1 ⁢ -1 = 1
53 iffalse ⊢ ¬ A mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 = − 1
54 iffalse ⊢ ¬ B mod 8 ∈ 1 7 → if B mod 8 ∈ 1 7 1 − 1 = − 1
55 53 54 oveqan12d ⊢ ¬ A mod 8 ∈ 1 7 ∧ ¬ B mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 1 = -1 ⁢ -1
56 55 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ ¬ A mod 8 ∈ 1 7 ∧ ¬ B mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 1 = -1 ⁢ -1
57 lgsdir2lem3 ⊢ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 1 7 ∪ 3 5
58 57 ad2ant2r ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → A mod 8 ∈ 1 7 ∪ 3 5
59 elun ⊢ A mod 8 ∈ 1 7 ∪ 3 5 ↔ A mod 8 ∈ 1 7 ∨ A mod 8 ∈ 3 5
60 58 59 sylib ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → A mod 8 ∈ 1 7 ∨ A mod 8 ∈ 3 5
61 60 orcanai ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ ¬ A mod 8 ∈ 1 7 → A mod 8 ∈ 3 5
62 lgsdir2lem3 ⊢ B ∈ ℤ ∧ ¬ 2 ∥ B → B mod 8 ∈ 1 7 ∪ 3 5
63 62 ad2ant2l ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → B mod 8 ∈ 1 7 ∪ 3 5
64 elun ⊢ B mod 8 ∈ 1 7 ∪ 3 5 ↔ B mod 8 ∈ 1 7 ∨ B mod 8 ∈ 3 5
65 63 64 sylib ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → B mod 8 ∈ 1 7 ∨ B mod 8 ∈ 3 5
66 65 orcanai ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ ¬ B mod 8 ∈ 1 7 → B mod 8 ∈ 3 5
67 61 66 anim12dan ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ ¬ A mod 8 ∈ 1 7 ∧ ¬ B mod 8 ∈ 1 7 → A mod 8 ∈ 3 5 ∧ B mod 8 ∈ 3 5
68 lgsdir2lem5 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ A mod 8 ∈ 3 5 ∧ B mod 8 ∈ 3 5 → A ⁢ B mod 8 ∈ 1 7
69 68 adantlr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ A mod 8 ∈ 3 5 ∧ B mod 8 ∈ 3 5 → A ⁢ B mod 8 ∈ 1 7
70 67 69 syldan ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ ¬ A mod 8 ∈ 1 7 ∧ ¬ B mod 8 ∈ 1 7 → A ⁢ B mod 8 ∈ 1 7
71 70 iftrued ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ ¬ A mod 8 ∈ 1 7 ∧ ¬ B mod 8 ∈ 1 7 → if A ⁢ B mod 8 ∈ 1 7 1 − 1 = 1
72 52 56 71 3eqtr4a ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B ∧ ¬ A mod 8 ∈ 1 7 ∧ ¬ B mod 8 ∈ 1 7 → if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 1 = if A ⁢ B mod 8 ∈ 1 7 1 − 1
73 34 51 72 pm2.61ddan ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 1 = if A ⁢ B mod 8 ∈ 1 7 1 − 1
74 iffalse ⊢ ¬ 2 ∥ A → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 = if A mod 8 ∈ 1 7 1 − 1
75 iffalse ⊢ ¬ 2 ∥ B → if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = if B mod 8 ∈ 1 7 1 − 1
76 74 75 oveqan12d ⊢ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⁢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 1
77 76 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⁢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = if A mod 8 ∈ 1 7 1 − 1 ⁢ if B mod 8 ∈ 1 7 1 − 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 → if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1 = if A ⁢ B mod 8 ∈ 1 7 1 − 1
86 84 85 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1 = if A ⁢ B mod 8 ∈ 1 7 1 − 1
87 73 77 86 3eqtr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ 2 ∥ A ∧ ¬ 2 ∥ B → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⁢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1
88 15 26 87 pm2.61ddan ⊢ A ∈ ℤ ∧ B ∈ ℤ → if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⁢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1 = if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1
89 lgs2 ⊢ A ∈ ℤ → A / L 2 = if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1
90 lgs2 ⊢ B ∈ ℤ → B / L 2 = if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1
91 89 90 oveqan12d ⊢ A ∈ ℤ ∧ B ∈ ℤ → A / L 2 ⁢ B / L 2 = if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 ⁢ if 2 ∥ B 0 if B mod 8 ∈ 1 7 1 − 1
92 zmulcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ⁢ B ∈ ℤ
93 lgs2 ⊢ A ⁢ B ∈ ℤ → A ⁢ B / L 2 = if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1
94 92 93 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ⁢ B / L 2 = if 2 ∥ A ⁢ B 0 if A ⁢ B mod 8 ∈ 1 7 1 − 1
95 88 91 94 3eqtr4rd ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ⁢ B / L 2 = A / L 2 ⁢ B / L 2