Metamath Proof Explorer

Theorem lgsdir2lem5

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

Ref Expression
Assertion 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 } )

Proof

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