Metamath Proof Explorer

Theorem lgsdir2lem4

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

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

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( A mod 8 ) e. _V
2 1 elpr 
 |-  ( ( A mod 8 ) e. { 1 , 7 } <-> ( ( A mod 8 ) = 1 \/ ( A mod 8 ) = 7 ) )
3 zre 
 |-  ( A e. ZZ -> A e. RR )
4 3 ad2antrr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> A e. RR )
5 1red 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> 1 e. RR )
6 simplr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> B e. ZZ )
7 8re 
 |-  8 e. RR
8 8pos 
 |-  0 < 8
9 7 8 elrpii 
 |-  8 e. RR+
10 9 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> 8 e. RR+ )
11 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> ( A mod 8 ) = 1 )
12 lgsdir2lem1 
 |-  ( ( ( 1 mod 8 ) = 1 /\ ( -u 1 mod 8 ) = 7 ) /\ ( ( 3 mod 8 ) = 3 /\ ( -u 3 mod 8 ) = 5 ) )
13 12 simpli 
 |-  ( ( 1 mod 8 ) = 1 /\ ( -u 1 mod 8 ) = 7 )
14 13 simpli 
 |-  ( 1 mod 8 ) = 1
15 11 14 eqtr4di 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> ( A mod 8 ) = ( 1 mod 8 ) )
16 modmul1 
 |-  ( ( ( A e. RR /\ 1 e. RR ) /\ ( B e. ZZ /\ 8 e. RR+ ) /\ ( A mod 8 ) = ( 1 mod 8 ) ) -> ( ( A x. B ) mod 8 ) = ( ( 1 x. B ) mod 8 ) )
17 4 5 6 10 15 16 syl221anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> ( ( A x. B ) mod 8 ) = ( ( 1 x. B ) mod 8 ) )
18 zcn 
 |-  ( B e. ZZ -> B e. CC )
19 18 ad2antlr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> B e. CC )
20 19 mullidd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> ( 1 x. B ) = B )
21 20 oveq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> ( ( 1 x. B ) mod 8 ) = ( B mod 8 ) )
22 17 21 eqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> ( ( A x. B ) mod 8 ) = ( B mod 8 ) )
23 22 eleq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 1 ) -> ( ( ( A x. B ) mod 8 ) e. { 1 , 7 } <-> ( B mod 8 ) e. { 1 , 7 } ) )
24 3 ad2antrr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> A e. RR )
25 neg1rr 
 |-  -u 1 e. RR
26 25 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> -u 1 e. RR )
27 simplr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> B e. ZZ )
28 9 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> 8 e. RR+ )
29 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> ( A mod 8 ) = 7 )
30 13 simpri 
 |-  ( -u 1 mod 8 ) = 7
31 29 30 eqtr4di 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> ( A mod 8 ) = ( -u 1 mod 8 ) )
32 modmul1 
 |-  ( ( ( A e. RR /\ -u 1 e. RR ) /\ ( B e. ZZ /\ 8 e. RR+ ) /\ ( A mod 8 ) = ( -u 1 mod 8 ) ) -> ( ( A x. B ) mod 8 ) = ( ( -u 1 x. B ) mod 8 ) )
33 24 26 27 28 31 32 syl221anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> ( ( A x. B ) mod 8 ) = ( ( -u 1 x. B ) mod 8 ) )
34 18 ad2antlr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> B e. CC )
35 34 mulm1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> ( -u 1 x. B ) = -u B )
36 35 oveq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> ( ( -u 1 x. B ) mod 8 ) = ( -u B mod 8 ) )
37 33 36 eqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> ( ( A x. B ) mod 8 ) = ( -u B mod 8 ) )
38 37 eleq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> ( ( ( A x. B ) mod 8 ) e. { 1 , 7 } <-> ( -u B mod 8 ) e. { 1 , 7 } ) )
39 znegcl 
 |-  ( B e. ZZ -> -u B e. ZZ )
40 oveq1 
 |-  ( x = -u B -> ( x mod 8 ) = ( -u B mod 8 ) )
41 40 eleq1d 
 |-  ( x = -u B -> ( ( x mod 8 ) e. { 1 , 7 } <-> ( -u B mod 8 ) e. { 1 , 7 } ) )
42 negeq 
 |-  ( x = -u B -> -u x = -u -u B )
43 42 oveq1d 
 |-  ( x = -u B -> ( -u x mod 8 ) = ( -u -u B mod 8 ) )
44 43 eleq1d 
 |-  ( x = -u B -> ( ( -u x mod 8 ) e. { 1 , 7 } <-> ( -u -u B mod 8 ) e. { 1 , 7 } ) )
45 41 44 imbi12d 
 |-  ( x = -u B -> ( ( ( x mod 8 ) e. { 1 , 7 } -> ( -u x mod 8 ) e. { 1 , 7 } ) <-> ( ( -u B mod 8 ) e. { 1 , 7 } -> ( -u -u B mod 8 ) e. { 1 , 7 } ) ) )
46 zcn 
 |-  ( x e. ZZ -> x e. CC )
47 neg1cn 
 |-  -u 1 e. CC
48 mulcom 
 |-  ( ( x e. CC /\ -u 1 e. CC ) -> ( x x. -u 1 ) = ( -u 1 x. x ) )
49 47 48 mpan2 
 |-  ( x e. CC -> ( x x. -u 1 ) = ( -u 1 x. x ) )
50 mulm1 
 |-  ( x e. CC -> ( -u 1 x. x ) = -u x )
51 49 50 eqtrd 
 |-  ( x e. CC -> ( x x. -u 1 ) = -u x )
52 46 51 syl 
 |-  ( x e. ZZ -> ( x x. -u 1 ) = -u x )
53 52 adantr 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> ( x x. -u 1 ) = -u x )
54 53 oveq1d 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> ( ( x x. -u 1 ) mod 8 ) = ( -u x mod 8 ) )
55 zre 
 |-  ( x e. ZZ -> x e. RR )
56 55 adantr 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> x e. RR )
57 1red 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> 1 e. RR )
58 neg1z 
 |-  -u 1 e. ZZ
59 58 a1i 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> -u 1 e. ZZ )
60 9 a1i 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> 8 e. RR+ )
61 simpr 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> ( x mod 8 ) = 1 )
62 61 14 eqtr4di 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> ( x mod 8 ) = ( 1 mod 8 ) )
63 modmul1 
 |-  ( ( ( x e. RR /\ 1 e. RR ) /\ ( -u 1 e. ZZ /\ 8 e. RR+ ) /\ ( x mod 8 ) = ( 1 mod 8 ) ) -> ( ( x x. -u 1 ) mod 8 ) = ( ( 1 x. -u 1 ) mod 8 ) )
64 56 57 59 60 62 63 syl221anc 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> ( ( x x. -u 1 ) mod 8 ) = ( ( 1 x. -u 1 ) mod 8 ) )
65 54 64 eqtr3d 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> ( -u x mod 8 ) = ( ( 1 x. -u 1 ) mod 8 ) )
66 47 mullidi 
 |-  ( 1 x. -u 1 ) = -u 1
67 66 oveq1i 
 |-  ( ( 1 x. -u 1 ) mod 8 ) = ( -u 1 mod 8 )
68 67 30 eqtri 
 |-  ( ( 1 x. -u 1 ) mod 8 ) = 7
69 65 68 eqtrdi 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 1 ) -> ( -u x mod 8 ) = 7 )
70 69 ex 
 |-  ( x e. ZZ -> ( ( x mod 8 ) = 1 -> ( -u x mod 8 ) = 7 ) )
71 52 adantr 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> ( x x. -u 1 ) = -u x )
72 71 oveq1d 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> ( ( x x. -u 1 ) mod 8 ) = ( -u x mod 8 ) )
73 55 adantr 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> x e. RR )
74 25 a1i 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> -u 1 e. RR )
75 58 a1i 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> -u 1 e. ZZ )
76 9 a1i 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> 8 e. RR+ )
77 simpr 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> ( x mod 8 ) = 7 )
78 77 30 eqtr4di 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> ( x mod 8 ) = ( -u 1 mod 8 ) )
79 modmul1 
 |-  ( ( ( x e. RR /\ -u 1 e. RR ) /\ ( -u 1 e. ZZ /\ 8 e. RR+ ) /\ ( x mod 8 ) = ( -u 1 mod 8 ) ) -> ( ( x x. -u 1 ) mod 8 ) = ( ( -u 1 x. -u 1 ) mod 8 ) )
80 73 74 75 76 78 79 syl221anc 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> ( ( x x. -u 1 ) mod 8 ) = ( ( -u 1 x. -u 1 ) mod 8 ) )
81 72 80 eqtr3d 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> ( -u x mod 8 ) = ( ( -u 1 x. -u 1 ) mod 8 ) )
82 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
83 82 oveq1i 
 |-  ( ( -u 1 x. -u 1 ) mod 8 ) = ( 1 mod 8 )
84 83 14 eqtri 
 |-  ( ( -u 1 x. -u 1 ) mod 8 ) = 1
85 81 84 eqtrdi 
 |-  ( ( x e. ZZ /\ ( x mod 8 ) = 7 ) -> ( -u x mod 8 ) = 1 )
86 85 ex 
 |-  ( x e. ZZ -> ( ( x mod 8 ) = 7 -> ( -u x mod 8 ) = 1 ) )
87 70 86 orim12d 
 |-  ( x e. ZZ -> ( ( ( x mod 8 ) = 1 \/ ( x mod 8 ) = 7 ) -> ( ( -u x mod 8 ) = 7 \/ ( -u x mod 8 ) = 1 ) ) )
88 ovex 
 |-  ( x mod 8 ) e. _V
89 88 elpr 
 |-  ( ( x mod 8 ) e. { 1 , 7 } <-> ( ( x mod 8 ) = 1 \/ ( x mod 8 ) = 7 ) )
90 ovex 
 |-  ( -u x mod 8 ) e. _V
91 90 elpr 
 |-  ( ( -u x mod 8 ) e. { 1 , 7 } <-> ( ( -u x mod 8 ) = 1 \/ ( -u x mod 8 ) = 7 ) )
92 orcom 
 |-  ( ( ( -u x mod 8 ) = 1 \/ ( -u x mod 8 ) = 7 ) <-> ( ( -u x mod 8 ) = 7 \/ ( -u x mod 8 ) = 1 ) )
93 91 92 bitri 
 |-  ( ( -u x mod 8 ) e. { 1 , 7 } <-> ( ( -u x mod 8 ) = 7 \/ ( -u x mod 8 ) = 1 ) )
94 87 89 93 3imtr4g 
 |-  ( x e. ZZ -> ( ( x mod 8 ) e. { 1 , 7 } -> ( -u x mod 8 ) e. { 1 , 7 } ) )
95 45 94 vtoclga 
 |-  ( -u B e. ZZ -> ( ( -u B mod 8 ) e. { 1 , 7 } -> ( -u -u B mod 8 ) e. { 1 , 7 } ) )
96 39 95 syl 
 |-  ( B e. ZZ -> ( ( -u B mod 8 ) e. { 1 , 7 } -> ( -u -u B mod 8 ) e. { 1 , 7 } ) )
97 18 negnegd 
 |-  ( B e. ZZ -> -u -u B = B )
98 97 oveq1d 
 |-  ( B e. ZZ -> ( -u -u B mod 8 ) = ( B mod 8 ) )
99 98 eleq1d 
 |-  ( B e. ZZ -> ( ( -u -u B mod 8 ) e. { 1 , 7 } <-> ( B mod 8 ) e. { 1 , 7 } ) )
100 96 99 sylibd 
 |-  ( B e. ZZ -> ( ( -u B mod 8 ) e. { 1 , 7 } -> ( B mod 8 ) e. { 1 , 7 } ) )
101 oveq1 
 |-  ( x = B -> ( x mod 8 ) = ( B mod 8 ) )
102 101 eleq1d 
 |-  ( x = B -> ( ( x mod 8 ) e. { 1 , 7 } <-> ( B mod 8 ) e. { 1 , 7 } ) )
103 negeq 
 |-  ( x = B -> -u x = -u B )
104 103 oveq1d 
 |-  ( x = B -> ( -u x mod 8 ) = ( -u B mod 8 ) )
105 104 eleq1d 
 |-  ( x = B -> ( ( -u x mod 8 ) e. { 1 , 7 } <-> ( -u B mod 8 ) e. { 1 , 7 } ) )
106 102 105 imbi12d 
 |-  ( x = B -> ( ( ( x mod 8 ) e. { 1 , 7 } -> ( -u x mod 8 ) e. { 1 , 7 } ) <-> ( ( B mod 8 ) e. { 1 , 7 } -> ( -u B mod 8 ) e. { 1 , 7 } ) ) )
107 106 94 vtoclga 
 |-  ( B e. ZZ -> ( ( B mod 8 ) e. { 1 , 7 } -> ( -u B mod 8 ) e. { 1 , 7 } ) )
108 100 107 impbid 
 |-  ( B e. ZZ -> ( ( -u B mod 8 ) e. { 1 , 7 } <-> ( B mod 8 ) e. { 1 , 7 } ) )
109 108 ad2antlr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> ( ( -u B mod 8 ) e. { 1 , 7 } <-> ( B mod 8 ) e. { 1 , 7 } ) )
110 38 109 bitrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( A mod 8 ) = 7 ) -> ( ( ( A x. B ) mod 8 ) e. { 1 , 7 } <-> ( B mod 8 ) e. { 1 , 7 } ) )
111 23 110 jaodan 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( ( A mod 8 ) = 1 \/ ( A mod 8 ) = 7 ) ) -> ( ( ( A x. B ) mod 8 ) e. { 1 , 7 } <-> ( B mod 8 ) e. { 1 , 7 } ) )
112 2 111 sylan2b 
 |-  ( ( ( 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 } ) )