Metamath Proof Explorer

Theorem lgsdir2lem1

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

Ref Expression
Assertion lgsdir2lem1 ⊢ 1 mod 8 = 1 ∧ -1 mod 8 = 7 ∧ 3 mod 8 = 3 ∧ -3 mod 8 = 5

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 8re ⊢ 8 ∈ ℝ
3 8pos ⊢ 0 < 8
4 2 3 elrpii ⊢ 8 ∈ ℝ +
5 0le1 ⊢ 0 ≤ 1
6 1lt8 ⊢ 1 < 8
7 modid ⊢ 1 ∈ ℝ ∧ 8 ∈ ℝ + ∧ 0 ≤ 1 ∧ 1 < 8 → 1 mod 8 = 1
8 1 4 5 6 7 mp4an ⊢ 1 mod 8 = 1
9 8cn ⊢ 8 ∈ ℂ
10 9 mulid2i ⊢ 1 ⋅ 8 = 8
11 10 oveq2i ⊢ - 1 + 1 ⋅ 8 = - 1 + 8
12 ax-1cn ⊢ 1 ∈ ℂ
13 12 negcli ⊢ − 1 ∈ ℂ
14 9 12 negsubi ⊢ 8 + -1 = 8 − 1
15 8m1e7 ⊢ 8 − 1 = 7
16 14 15 eqtri ⊢ 8 + -1 = 7
17 9 13 16 addcomli ⊢ - 1 + 8 = 7
18 11 17 eqtri ⊢ - 1 + 1 ⋅ 8 = 7
19 18 oveq1i ⊢ - 1 + 1 ⋅ 8 mod 8 = 7 mod 8
20 1 renegcli ⊢ − 1 ∈ ℝ
21 1z ⊢ 1 ∈ ℤ
22 modcyc ⊢ − 1 ∈ ℝ ∧ 8 ∈ ℝ + ∧ 1 ∈ ℤ → - 1 + 1 ⋅ 8 mod 8 = -1 mod 8
23 20 4 21 22 mp3an ⊢ - 1 + 1 ⋅ 8 mod 8 = -1 mod 8
24 7re ⊢ 7 ∈ ℝ
25 0re ⊢ 0 ∈ ℝ
26 7pos ⊢ 0 < 7
27 25 24 26 ltleii ⊢ 0 ≤ 7
28 7lt8 ⊢ 7 < 8
29 modid ⊢ 7 ∈ ℝ ∧ 8 ∈ ℝ + ∧ 0 ≤ 7 ∧ 7 < 8 → 7 mod 8 = 7
30 24 4 27 28 29 mp4an ⊢ 7 mod 8 = 7
31 19 23 30 3eqtr3i ⊢ -1 mod 8 = 7
32 8 31 pm3.2i ⊢ 1 mod 8 = 1 ∧ -1 mod 8 = 7
33 3re ⊢ 3 ∈ ℝ
34 3pos ⊢ 0 < 3
35 25 33 34 ltleii ⊢ 0 ≤ 3
36 3lt8 ⊢ 3 < 8
37 modid ⊢ 3 ∈ ℝ ∧ 8 ∈ ℝ + ∧ 0 ≤ 3 ∧ 3 < 8 → 3 mod 8 = 3
38 33 4 35 36 37 mp4an ⊢ 3 mod 8 = 3
39 10 oveq2i ⊢ - 3 + 1 ⋅ 8 = - 3 + 8
40 3cn ⊢ 3 ∈ ℂ
41 40 negcli ⊢ − 3 ∈ ℂ
42 9 40 negsubi ⊢ 8 + -3 = 8 − 3
43 5cn ⊢ 5 ∈ ℂ
44 5p3e8 ⊢ 5 + 3 = 8
45 43 40 44 addcomli ⊢ 3 + 5 = 8
46 9 40 43 45 subaddrii ⊢ 8 − 3 = 5
47 42 46 eqtri ⊢ 8 + -3 = 5
48 9 41 47 addcomli ⊢ - 3 + 8 = 5
49 39 48 eqtri ⊢ - 3 + 1 ⋅ 8 = 5
50 49 oveq1i ⊢ - 3 + 1 ⋅ 8 mod 8 = 5 mod 8
51 33 renegcli ⊢ − 3 ∈ ℝ
52 modcyc ⊢ − 3 ∈ ℝ ∧ 8 ∈ ℝ + ∧ 1 ∈ ℤ → - 3 + 1 ⋅ 8 mod 8 = -3 mod 8
53 51 4 21 52 mp3an ⊢ - 3 + 1 ⋅ 8 mod 8 = -3 mod 8
54 5re ⊢ 5 ∈ ℝ
55 5pos ⊢ 0 < 5
56 25 54 55 ltleii ⊢ 0 ≤ 5
57 5lt8 ⊢ 5 < 8
58 modid ⊢ 5 ∈ ℝ ∧ 8 ∈ ℝ + ∧ 0 ≤ 5 ∧ 5 < 8 → 5 mod 8 = 5
59 54 4 56 57 58 mp4an ⊢ 5 mod 8 = 5
60 50 53 59 3eqtr3i ⊢ -3 mod 8 = 5
61 38 60 pm3.2i ⊢ 3 mod 8 = 3 ∧ -3 mod 8 = 5
62 32 61 pm3.2i ⊢ 1 mod 8 = 1 ∧ -1 mod 8 = 7 ∧ 3 mod 8 = 3 ∧ -3 mod 8 = 5