Proof of Theorem lgsdir2lem1
Step | Hyp | Ref
| Expression |
1 | | 1re 9918 |
. . . 4
⊢ 1 ∈
ℝ |
2 | | 8re 10982 |
. . . . 5
⊢ 8 ∈
ℝ |
3 | | 8pos 10998 |
. . . . 5
⊢ 0 <
8 |
4 | 2, 3 | elrpii 11711 |
. . . 4
⊢ 8 ∈
ℝ+ |
5 | | 0le1 10430 |
. . . 4
⊢ 0 ≤
1 |
6 | | 1lt8 11098 |
. . . 4
⊢ 1 <
8 |
7 | | modid 12557 |
. . . 4
⊢ (((1
∈ ℝ ∧ 8 ∈ ℝ+) ∧ (0 ≤ 1 ∧ 1 <
8)) → (1 mod 8) = 1) |
8 | 1, 4, 5, 6, 7 | mp4an 705 |
. . 3
⊢ (1 mod 8)
= 1 |
9 | | 8cn 10983 |
. . . . . . . 8
⊢ 8 ∈
ℂ |
10 | 9 | mulid2i 9922 |
. . . . . . 7
⊢ (1
· 8) = 8 |
11 | 10 | oveq2i 6560 |
. . . . . 6
⊢ (-1 + (1
· 8)) = (-1 + 8) |
12 | | ax-1cn 9873 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
13 | 12 | negcli 10228 |
. . . . . . 7
⊢ -1 ∈
ℂ |
14 | 9, 12 | negsubi 10238 |
. . . . . . . 8
⊢ (8 + -1)
= (8 − 1) |
15 | | 7cn 10981 |
. . . . . . . . 9
⊢ 7 ∈
ℂ |
16 | 12, 15 | addcomi 10106 |
. . . . . . . . . 10
⊢ (1 + 7) =
(7 + 1) |
17 | | df-8 10962 |
. . . . . . . . . 10
⊢ 8 = (7 +
1) |
18 | 16, 17 | eqtr4i 2635 |
. . . . . . . . 9
⊢ (1 + 7) =
8 |
19 | 9, 12, 15, 18 | subaddrii 10249 |
. . . . . . . 8
⊢ (8
− 1) = 7 |
20 | 14, 19 | eqtri 2632 |
. . . . . . 7
⊢ (8 + -1)
= 7 |
21 | 9, 13, 20 | addcomli 10107 |
. . . . . 6
⊢ (-1 + 8)
= 7 |
22 | 11, 21 | eqtri 2632 |
. . . . 5
⊢ (-1 + (1
· 8)) = 7 |
23 | 22 | oveq1i 6559 |
. . . 4
⊢ ((-1 + (1
· 8)) mod 8) = (7 mod 8) |
24 | 1 | renegcli 10221 |
. . . . 5
⊢ -1 ∈
ℝ |
25 | | 1z 11284 |
. . . . 5
⊢ 1 ∈
ℤ |
26 | | modcyc 12567 |
. . . . 5
⊢ ((-1
∈ ℝ ∧ 8 ∈ ℝ+ ∧ 1 ∈ ℤ)
→ ((-1 + (1 · 8)) mod 8) = (-1 mod 8)) |
27 | 24, 4, 25, 26 | mp3an 1416 |
. . . 4
⊢ ((-1 + (1
· 8)) mod 8) = (-1 mod 8) |
28 | | 7re 10980 |
. . . . 5
⊢ 7 ∈
ℝ |
29 | | 0re 9919 |
. . . . . 6
⊢ 0 ∈
ℝ |
30 | | 7pos 10997 |
. . . . . 6
⊢ 0 <
7 |
31 | 29, 28, 30 | ltleii 10039 |
. . . . 5
⊢ 0 ≤
7 |
32 | | 7lt8 11092 |
. . . . 5
⊢ 7 <
8 |
33 | | modid 12557 |
. . . . 5
⊢ (((7
∈ ℝ ∧ 8 ∈ ℝ+) ∧ (0 ≤ 7 ∧ 7 <
8)) → (7 mod 8) = 7) |
34 | 28, 4, 31, 32, 33 | mp4an 705 |
. . . 4
⊢ (7 mod 8)
= 7 |
35 | 23, 27, 34 | 3eqtr3i 2640 |
. . 3
⊢ (-1 mod
8) = 7 |
36 | 8, 35 | pm3.2i 470 |
. 2
⊢ ((1 mod
8) = 1 ∧ (-1 mod 8) = 7) |
37 | | 3re 10971 |
. . . 4
⊢ 3 ∈
ℝ |
38 | | 3pos 10991 |
. . . . 5
⊢ 0 <
3 |
39 | 29, 37, 38 | ltleii 10039 |
. . . 4
⊢ 0 ≤
3 |
40 | | 3lt8 11096 |
. . . 4
⊢ 3 <
8 |
41 | | modid 12557 |
. . . 4
⊢ (((3
∈ ℝ ∧ 8 ∈ ℝ+) ∧ (0 ≤ 3 ∧ 3 <
8)) → (3 mod 8) = 3) |
42 | 37, 4, 39, 40, 41 | mp4an 705 |
. . 3
⊢ (3 mod 8)
= 3 |
43 | 10 | oveq2i 6560 |
. . . . . 6
⊢ (-3 + (1
· 8)) = (-3 + 8) |
44 | | 3cn 10972 |
. . . . . . . 8
⊢ 3 ∈
ℂ |
45 | 44 | negcli 10228 |
. . . . . . 7
⊢ -3 ∈
ℂ |
46 | 9, 44 | negsubi 10238 |
. . . . . . . 8
⊢ (8 + -3)
= (8 − 3) |
47 | | 5cn 10977 |
. . . . . . . . 9
⊢ 5 ∈
ℂ |
48 | | 5p3e8 11043 |
. . . . . . . . . 10
⊢ (5 + 3) =
8 |
49 | 47, 44, 48 | addcomli 10107 |
. . . . . . . . 9
⊢ (3 + 5) =
8 |
50 | 9, 44, 47, 49 | subaddrii 10249 |
. . . . . . . 8
⊢ (8
− 3) = 5 |
51 | 46, 50 | eqtri 2632 |
. . . . . . 7
⊢ (8 + -3)
= 5 |
52 | 9, 45, 51 | addcomli 10107 |
. . . . . 6
⊢ (-3 + 8)
= 5 |
53 | 43, 52 | eqtri 2632 |
. . . . 5
⊢ (-3 + (1
· 8)) = 5 |
54 | 53 | oveq1i 6559 |
. . . 4
⊢ ((-3 + (1
· 8)) mod 8) = (5 mod 8) |
55 | 37 | renegcli 10221 |
. . . . 5
⊢ -3 ∈
ℝ |
56 | | modcyc 12567 |
. . . . 5
⊢ ((-3
∈ ℝ ∧ 8 ∈ ℝ+ ∧ 1 ∈ ℤ)
→ ((-3 + (1 · 8)) mod 8) = (-3 mod 8)) |
57 | 55, 4, 25, 56 | mp3an 1416 |
. . . 4
⊢ ((-3 + (1
· 8)) mod 8) = (-3 mod 8) |
58 | | 5re 10976 |
. . . . 5
⊢ 5 ∈
ℝ |
59 | | 5pos 10995 |
. . . . . 6
⊢ 0 <
5 |
60 | 29, 58, 59 | ltleii 10039 |
. . . . 5
⊢ 0 ≤
5 |
61 | | 5lt8 11094 |
. . . . 5
⊢ 5 <
8 |
62 | | modid 12557 |
. . . . 5
⊢ (((5
∈ ℝ ∧ 8 ∈ ℝ+) ∧ (0 ≤ 5 ∧ 5 <
8)) → (5 mod 8) = 5) |
63 | 58, 4, 60, 61, 62 | mp4an 705 |
. . . 4
⊢ (5 mod 8)
= 5 |
64 | 54, 57, 63 | 3eqtr3i 2640 |
. . 3
⊢ (-3 mod
8) = 5 |
65 | 42, 64 | pm3.2i 470 |
. 2
⊢ ((3 mod
8) = 3 ∧ (-3 mod 8) = 5) |
66 | 36, 65 | pm3.2i 470 |
1
⊢ (((1 mod
8) = 1 ∧ (-1 mod 8) = 7) ∧ ((3 mod 8) = 3 ∧ (-3 mod 8) =
5)) |