Metamath Proof Explorer

Theorem lgsdir2lem4

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

Ref Expression
Assertion lgsdir2lem4 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ A mod 8 ∈ 1 7 → A ⁢ B mod 8 ∈ 1 7 ↔ B mod 8 ∈ 1 7

Proof

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