Proof of Theorem lgsdir2lem1
| Step | Hyp | Ref
| Expression |
| 1 | | 1re 11261 |
. . . 4
⊢ 1 ∈
ℝ |
| 2 | | 8re 12362 |
. . . . 5
⊢ 8 ∈
ℝ |
| 3 | | 8pos 12378 |
. . . . 5
⊢ 0 <
8 |
| 4 | 2, 3 | elrpii 13037 |
. . . 4
⊢ 8 ∈
ℝ+ |
| 5 | | 0le1 11786 |
. . . 4
⊢ 0 ≤
1 |
| 6 | | 1lt8 12464 |
. . . 4
⊢ 1 <
8 |
| 7 | | modid 13936 |
. . . 4
⊢ (((1
∈ ℝ ∧ 8 ∈ ℝ+) ∧ (0 ≤ 1 ∧ 1 <
8)) → (1 mod 8) = 1) |
| 8 | 1, 4, 5, 6, 7 | mp4an 693 |
. . 3
⊢ (1 mod 8)
= 1 |
| 9 | | 8cn 12363 |
. . . . . . . 8
⊢ 8 ∈
ℂ |
| 10 | 9 | mullidi 11266 |
. . . . . . 7
⊢ (1
· 8) = 8 |
| 11 | 10 | oveq2i 7442 |
. . . . . 6
⊢ (-1 + (1
· 8)) = (-1 + 8) |
| 12 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 13 | 12 | negcli 11577 |
. . . . . . 7
⊢ -1 ∈
ℂ |
| 14 | 9, 12 | negsubi 11587 |
. . . . . . . 8
⊢ (8 + -1)
= (8 − 1) |
| 15 | | 8m1e7 12399 |
. . . . . . . 8
⊢ (8
− 1) = 7 |
| 16 | 14, 15 | eqtri 2765 |
. . . . . . 7
⊢ (8 + -1)
= 7 |
| 17 | 9, 13, 16 | addcomli 11453 |
. . . . . 6
⊢ (-1 + 8)
= 7 |
| 18 | 11, 17 | eqtri 2765 |
. . . . 5
⊢ (-1 + (1
· 8)) = 7 |
| 19 | 18 | oveq1i 7441 |
. . . 4
⊢ ((-1 + (1
· 8)) mod 8) = (7 mod 8) |
| 20 | 1 | renegcli 11570 |
. . . . 5
⊢ -1 ∈
ℝ |
| 21 | | 1z 12647 |
. . . . 5
⊢ 1 ∈
ℤ |
| 22 | | modcyc 13946 |
. . . . 5
⊢ ((-1
∈ ℝ ∧ 8 ∈ ℝ+ ∧ 1 ∈ ℤ)
→ ((-1 + (1 · 8)) mod 8) = (-1 mod 8)) |
| 23 | 20, 4, 21, 22 | mp3an 1463 |
. . . 4
⊢ ((-1 + (1
· 8)) mod 8) = (-1 mod 8) |
| 24 | | 7re 12359 |
. . . . 5
⊢ 7 ∈
ℝ |
| 25 | | 0re 11263 |
. . . . . 6
⊢ 0 ∈
ℝ |
| 26 | | 7pos 12377 |
. . . . . 6
⊢ 0 <
7 |
| 27 | 25, 24, 26 | ltleii 11384 |
. . . . 5
⊢ 0 ≤
7 |
| 28 | | 7lt8 12458 |
. . . . 5
⊢ 7 <
8 |
| 29 | | modid 13936 |
. . . . 5
⊢ (((7
∈ ℝ ∧ 8 ∈ ℝ+) ∧ (0 ≤ 7 ∧ 7 <
8)) → (7 mod 8) = 7) |
| 30 | 24, 4, 27, 28, 29 | mp4an 693 |
. . . 4
⊢ (7 mod 8)
= 7 |
| 31 | 19, 23, 30 | 3eqtr3i 2773 |
. . 3
⊢ (-1 mod
8) = 7 |
| 32 | 8, 31 | pm3.2i 470 |
. 2
⊢ ((1 mod
8) = 1 ∧ (-1 mod 8) = 7) |
| 33 | | 3re 12346 |
. . . 4
⊢ 3 ∈
ℝ |
| 34 | | 3pos 12371 |
. . . . 5
⊢ 0 <
3 |
| 35 | 25, 33, 34 | ltleii 11384 |
. . . 4
⊢ 0 ≤
3 |
| 36 | | 3lt8 12462 |
. . . 4
⊢ 3 <
8 |
| 37 | | modid 13936 |
. . . 4
⊢ (((3
∈ ℝ ∧ 8 ∈ ℝ+) ∧ (0 ≤ 3 ∧ 3 <
8)) → (3 mod 8) = 3) |
| 38 | 33, 4, 35, 36, 37 | mp4an 693 |
. . 3
⊢ (3 mod 8)
= 3 |
| 39 | 10 | oveq2i 7442 |
. . . . . 6
⊢ (-3 + (1
· 8)) = (-3 + 8) |
| 40 | | 3cn 12347 |
. . . . . . . 8
⊢ 3 ∈
ℂ |
| 41 | 40 | negcli 11577 |
. . . . . . 7
⊢ -3 ∈
ℂ |
| 42 | 9, 40 | negsubi 11587 |
. . . . . . . 8
⊢ (8 + -3)
= (8 − 3) |
| 43 | | 5cn 12354 |
. . . . . . . . 9
⊢ 5 ∈
ℂ |
| 44 | | 5p3e8 12423 |
. . . . . . . . . 10
⊢ (5 + 3) =
8 |
| 45 | 43, 40, 44 | addcomli 11453 |
. . . . . . . . 9
⊢ (3 + 5) =
8 |
| 46 | 9, 40, 43, 45 | subaddrii 11598 |
. . . . . . . 8
⊢ (8
− 3) = 5 |
| 47 | 42, 46 | eqtri 2765 |
. . . . . . 7
⊢ (8 + -3)
= 5 |
| 48 | 9, 41, 47 | addcomli 11453 |
. . . . . 6
⊢ (-3 + 8)
= 5 |
| 49 | 39, 48 | eqtri 2765 |
. . . . 5
⊢ (-3 + (1
· 8)) = 5 |
| 50 | 49 | oveq1i 7441 |
. . . 4
⊢ ((-3 + (1
· 8)) mod 8) = (5 mod 8) |
| 51 | 33 | renegcli 11570 |
. . . . 5
⊢ -3 ∈
ℝ |
| 52 | | modcyc 13946 |
. . . . 5
⊢ ((-3
∈ ℝ ∧ 8 ∈ ℝ+ ∧ 1 ∈ ℤ)
→ ((-3 + (1 · 8)) mod 8) = (-3 mod 8)) |
| 53 | 51, 4, 21, 52 | mp3an 1463 |
. . . 4
⊢ ((-3 + (1
· 8)) mod 8) = (-3 mod 8) |
| 54 | | 5re 12353 |
. . . . 5
⊢ 5 ∈
ℝ |
| 55 | | 5pos 12375 |
. . . . . 6
⊢ 0 <
5 |
| 56 | 25, 54, 55 | ltleii 11384 |
. . . . 5
⊢ 0 ≤
5 |
| 57 | | 5lt8 12460 |
. . . . 5
⊢ 5 <
8 |
| 58 | | modid 13936 |
. . . . 5
⊢ (((5
∈ ℝ ∧ 8 ∈ ℝ+) ∧ (0 ≤ 5 ∧ 5 <
8)) → (5 mod 8) = 5) |
| 59 | 54, 4, 56, 57, 58 | mp4an 693 |
. . . 4
⊢ (5 mod 8)
= 5 |
| 60 | 50, 53, 59 | 3eqtr3i 2773 |
. . 3
⊢ (-3 mod
8) = 5 |
| 61 | 38, 60 | pm3.2i 470 |
. 2
⊢ ((3 mod
8) = 3 ∧ (-3 mod 8) = 5) |
| 62 | 32, 61 | pm3.2i 470 |
1
⊢ (((1 mod
8) = 1 ∧ (-1 mod 8) = 7) ∧ ((3 mod 8) = 3 ∧ (-3 mod 8) =
5)) |