Metamath Proof Explorer

Theorem lgsdir2lem4

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

Ref Expression
Assertion lgsdir2lem4 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) ∈ { 1 , 7 } ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )

Proof

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