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 e. ZZ /\ B e. ZZ ) -> ( ( A x. B ) /L 2 ) = ( ( A /L 2 ) x. ( B /L 2 ) ) )

Proof

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