Metamath Proof Explorer

Theorem lgsdir2lem4

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

Ref Expression
Assertion lgsdir2lem4 ⊢A∈ℤ∧B∈ℤ∧Amod8∈17→A⁢Bmod8∈17↔Bmod8∈17

Proof

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