# 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 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}{B}{/}_{L}2=\left({A}{/}_{L}2\right)\left({B}{/}_{L}2\right)$

### Proof

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