Metamath Proof Explorer

Theorem lgsdir2lem5

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

Ref Expression
Assertion lgsdir2lem5 ⊢A∈ℤ∧B∈ℤ∧Amod8∈35∧Bmod8∈35→A⁢Bmod8∈17

Proof

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