Metamath Proof Explorer


Theorem lgsdir2lem5

Description: Lemma for lgsdir2 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsdir2lem5 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) ∈ { 3 , 5 } ∧ ( 𝐵 mod 8 ) ∈ { 3 , 5 } ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { 1 , 7 } )

Proof

Step Hyp Ref Expression
1 ovex ( 𝐴 mod 8 ) ∈ V
2 1 elpr ( ( 𝐴 mod 8 ) ∈ { 3 , 5 } ↔ ( ( 𝐴 mod 8 ) = 3 ∨ ( 𝐴 mod 8 ) = 5 ) )
3 ovex ( 𝐵 mod 8 ) ∈ V
4 3 elpr ( ( 𝐵 mod 8 ) ∈ { 3 , 5 } ↔ ( ( 𝐵 mod 8 ) = 3 ∨ ( 𝐵 mod 8 ) = 5 ) )
5 2 4 anbi12i ( ( ( 𝐴 mod 8 ) ∈ { 3 , 5 } ∧ ( 𝐵 mod 8 ) ∈ { 3 , 5 } ) ↔ ( ( ( 𝐴 mod 8 ) = 3 ∨ ( 𝐴 mod 8 ) = 5 ) ∧ ( ( 𝐵 mod 8 ) = 3 ∨ ( 𝐵 mod 8 ) = 5 ) ) )
6 simpll ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → 𝐴 ∈ ℤ )
7 3z 3 ∈ ℤ
8 7 a1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → 3 ∈ ℤ )
9 simplr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → 𝐵 ∈ ℤ )
10 8re 8 ∈ ℝ
11 8pos 0 < 8
12 10 11 elrpii 8 ∈ ℝ+
13 12 a1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → 8 ∈ ℝ+ )
14 simprl ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( 𝐴 mod 8 ) = 3 )
15 lgsdir2lem1 ( ( ( 1 mod 8 ) = 1 ∧ ( - 1 mod 8 ) = 7 ) ∧ ( ( 3 mod 8 ) = 3 ∧ ( - 3 mod 8 ) = 5 ) )
16 15 simpri ( ( 3 mod 8 ) = 3 ∧ ( - 3 mod 8 ) = 5 )
17 16 simpli ( 3 mod 8 ) = 3
18 14 17 eqtr4di ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( 𝐴 mod 8 ) = ( 3 mod 8 ) )
19 simprr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( 𝐵 mod 8 ) = 3 )
20 19 17 eqtr4di ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( 𝐵 mod 8 ) = ( 3 mod 8 ) )
21 6 8 9 8 13 18 20 modmul12d ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) )
22 21 orcd ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) )
23 22 ex ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 3 ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) ) )
24 simpll ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → 𝐴 ∈ ℤ )
25 znegcl ( 3 ∈ ℤ → - 3 ∈ ℤ )
26 7 25 mp1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → - 3 ∈ ℤ )
27 simplr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → 𝐵 ∈ ℤ )
28 7 a1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → 3 ∈ ℤ )
29 12 a1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → 8 ∈ ℝ+ )
30 simprl ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( 𝐴 mod 8 ) = 5 )
31 16 simpri ( - 3 mod 8 ) = 5
32 30 31 eqtr4di ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( 𝐴 mod 8 ) = ( - 3 mod 8 ) )
33 simprr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( 𝐵 mod 8 ) = 3 )
34 33 17 eqtr4di ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( 𝐵 mod 8 ) = ( 3 mod 8 ) )
35 24 26 27 28 29 32 34 modmul12d ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( - 3 · 3 ) mod 8 ) )
36 3cn 3 ∈ ℂ
37 36 36 mulneg1i ( - 3 · 3 ) = - ( 3 · 3 )
38 37 oveq1i ( ( - 3 · 3 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 )
39 35 38 eqtrdi ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) )
40 39 olcd ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) )
41 40 ex ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 3 ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) ) )
42 simpll ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → 𝐴 ∈ ℤ )
43 7 a1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → 3 ∈ ℤ )
44 simplr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → 𝐵 ∈ ℤ )
45 7 25 mp1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → - 3 ∈ ℤ )
46 12 a1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → 8 ∈ ℝ+ )
47 simprl ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( 𝐴 mod 8 ) = 3 )
48 47 17 eqtr4di ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( 𝐴 mod 8 ) = ( 3 mod 8 ) )
49 simprr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( 𝐵 mod 8 ) = 5 )
50 49 31 eqtr4di ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( 𝐵 mod 8 ) = ( - 3 mod 8 ) )
51 42 43 44 45 46 48 50 modmul12d ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · - 3 ) mod 8 ) )
52 36 36 mulneg2i ( 3 · - 3 ) = - ( 3 · 3 )
53 52 oveq1i ( ( 3 · - 3 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 )
54 51 53 eqtrdi ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) )
55 54 olcd ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) )
56 55 ex ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝐴 mod 8 ) = 3 ∧ ( 𝐵 mod 8 ) = 5 ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) ) )
57 simpll ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → 𝐴 ∈ ℤ )
58 7 25 mp1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → - 3 ∈ ℤ )
59 simplr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → 𝐵 ∈ ℤ )
60 12 a1i ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → 8 ∈ ℝ+ )
61 simprl ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( 𝐴 mod 8 ) = 5 )
62 61 31 eqtr4di ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( 𝐴 mod 8 ) = ( - 3 mod 8 ) )
63 simprr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( 𝐵 mod 8 ) = 5 )
64 63 31 eqtr4di ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( 𝐵 mod 8 ) = ( - 3 mod 8 ) )
65 57 58 59 58 60 62 64 modmul12d ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( - 3 · - 3 ) mod 8 ) )
66 36 36 mul2negi ( - 3 · - 3 ) = ( 3 · 3 )
67 66 oveq1i ( ( - 3 · - 3 ) mod 8 ) = ( ( 3 · 3 ) mod 8 )
68 65 67 eqtrdi ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) )
69 68 orcd ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) )
70 69 ex ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝐴 mod 8 ) = 5 ∧ ( 𝐵 mod 8 ) = 5 ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) ) )
71 23 41 56 70 ccased ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( ( 𝐴 mod 8 ) = 3 ∨ ( 𝐴 mod 8 ) = 5 ) ∧ ( ( 𝐵 mod 8 ) = 3 ∨ ( 𝐵 mod 8 ) = 5 ) ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) ) )
72 5 71 syl5bi ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝐴 mod 8 ) ∈ { 3 , 5 } ∧ ( 𝐵 mod 8 ) ∈ { 3 , 5 } ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) ) )
73 72 imp ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) ∈ { 3 , 5 } ∧ ( 𝐵 mod 8 ) ∈ { 3 , 5 } ) ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) )
74 ovex ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ V
75 74 elpr ( ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { ( ( 3 · 3 ) mod 8 ) , ( - ( 3 · 3 ) mod 8 ) } ↔ ( ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 3 · 3 ) mod 8 ) ∨ ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - ( 3 · 3 ) mod 8 ) ) )
76 73 75 sylibr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) ∈ { 3 , 5 } ∧ ( 𝐵 mod 8 ) ∈ { 3 , 5 } ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { ( ( 3 · 3 ) mod 8 ) , ( - ( 3 · 3 ) mod 8 ) } )
77 df-9 9 = ( 8 + 1 )
78 8cn 8 ∈ ℂ
79 ax-1cn 1 ∈ ℂ
80 78 79 addcomi ( 8 + 1 ) = ( 1 + 8 )
81 77 80 eqtri 9 = ( 1 + 8 )
82 3t3e9 ( 3 · 3 ) = 9
83 78 mulid2i ( 1 · 8 ) = 8
84 83 oveq2i ( 1 + ( 1 · 8 ) ) = ( 1 + 8 )
85 81 82 84 3eqtr4i ( 3 · 3 ) = ( 1 + ( 1 · 8 ) )
86 85 oveq1i ( ( 3 · 3 ) mod 8 ) = ( ( 1 + ( 1 · 8 ) ) mod 8 )
87 1re 1 ∈ ℝ
88 1z 1 ∈ ℤ
89 modcyc ( ( 1 ∈ ℝ ∧ 8 ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( 1 + ( 1 · 8 ) ) mod 8 ) = ( 1 mod 8 ) )
90 87 12 88 89 mp3an ( ( 1 + ( 1 · 8 ) ) mod 8 ) = ( 1 mod 8 )
91 86 90 eqtri ( ( 3 · 3 ) mod 8 ) = ( 1 mod 8 )
92 15 simpli ( ( 1 mod 8 ) = 1 ∧ ( - 1 mod 8 ) = 7 )
93 92 simpli ( 1 mod 8 ) = 1
94 91 93 eqtri ( ( 3 · 3 ) mod 8 ) = 1
95 znegcl ( 1 ∈ ℤ → - 1 ∈ ℤ )
96 88 95 mp1i ( ⊤ → - 1 ∈ ℤ )
97 3nn 3 ∈ ℕ
98 97 97 nnmulcli ( 3 · 3 ) ∈ ℕ
99 98 nnzi ( 3 · 3 ) ∈ ℤ
100 99 a1i ( ⊤ → ( 3 · 3 ) ∈ ℤ )
101 88 a1i ( ⊤ → 1 ∈ ℤ )
102 12 a1i ( ⊤ → 8 ∈ ℝ+ )
103 eqidd ( ⊤ → ( - 1 mod 8 ) = ( - 1 mod 8 ) )
104 91 a1i ( ⊤ → ( ( 3 · 3 ) mod 8 ) = ( 1 mod 8 ) )
105 96 96 100 101 102 103 104 modmul12d ( ⊤ → ( ( - 1 · ( 3 · 3 ) ) mod 8 ) = ( ( - 1 · 1 ) mod 8 ) )
106 105 mptru ( ( - 1 · ( 3 · 3 ) ) mod 8 ) = ( ( - 1 · 1 ) mod 8 )
107 36 36 mulcli ( 3 · 3 ) ∈ ℂ
108 107 mulm1i ( - 1 · ( 3 · 3 ) ) = - ( 3 · 3 )
109 108 oveq1i ( ( - 1 · ( 3 · 3 ) ) mod 8 ) = ( - ( 3 · 3 ) mod 8 )
110 79 mulm1i ( - 1 · 1 ) = - 1
111 110 oveq1i ( ( - 1 · 1 ) mod 8 ) = ( - 1 mod 8 )
112 106 109 111 3eqtr3i ( - ( 3 · 3 ) mod 8 ) = ( - 1 mod 8 )
113 92 simpri ( - 1 mod 8 ) = 7
114 112 113 eqtri ( - ( 3 · 3 ) mod 8 ) = 7
115 94 114 preq12i { ( ( 3 · 3 ) mod 8 ) , ( - ( 3 · 3 ) mod 8 ) } = { 1 , 7 }
116 76 115 eleqtrdi ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) ∈ { 3 , 5 } ∧ ( 𝐵 mod 8 ) ∈ { 3 , 5 } ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { 1 , 7 } )