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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) /L 2 ) = ( ( 𝐴 /L 2 ) · ( 𝐵 /L 2 ) ) )

Proof

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