Step | Hyp | Ref
| Expression |
1 | | ovex 7442 |
. . 3
โข (๐ด mod 8) โ
V |
2 | 1 | elpr 4652 |
. 2
โข ((๐ด mod 8) โ {1, 7} โ
((๐ด mod 8) = 1 โจ (๐ด mod 8) = 7)) |
3 | | zre 12562 |
. . . . . . 7
โข (๐ด โ โค โ ๐ด โ
โ) |
4 | 3 | ad2antrr 725 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ ๐ด โ
โ) |
5 | | 1red 11215 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ 1 โ
โ) |
6 | | simplr 768 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ ๐ต โ
โค) |
7 | | 8re 12308 |
. . . . . . . 8
โข 8 โ
โ |
8 | | 8pos 12324 |
. . . . . . . 8
โข 0 <
8 |
9 | 7, 8 | elrpii 12977 |
. . . . . . 7
โข 8 โ
โ+ |
10 | 9 | a1i 11 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ 8 โ
โ+) |
11 | | simpr 486 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ (๐ด mod 8) = 1) |
12 | | lgsdir2lem1 26828 |
. . . . . . . . 9
โข (((1 mod
8) = 1 โง (-1 mod 8) = 7) โง ((3 mod 8) = 3 โง (-3 mod 8) =
5)) |
13 | 12 | simpli 485 |
. . . . . . . 8
โข ((1 mod
8) = 1 โง (-1 mod 8) = 7) |
14 | 13 | simpli 485 |
. . . . . . 7
โข (1 mod 8)
= 1 |
15 | 11, 14 | eqtr4di 2791 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ (๐ด mod 8) = (1 mod
8)) |
16 | | modmul1 13889 |
. . . . . 6
โข (((๐ด โ โ โง 1 โ
โ) โง (๐ต โ
โค โง 8 โ โ+) โง (๐ด mod 8) = (1 mod 8)) โ ((๐ด ยท ๐ต) mod 8) = ((1 ยท ๐ต) mod 8)) |
17 | 4, 5, 6, 10, 15, 16 | syl221anc 1382 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ ((๐ด ยท ๐ต) mod 8) = ((1 ยท ๐ต) mod 8)) |
18 | | zcn 12563 |
. . . . . . . 8
โข (๐ต โ โค โ ๐ต โ
โ) |
19 | 18 | ad2antlr 726 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ ๐ต โ
โ) |
20 | 19 | mullidd 11232 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ (1 ยท
๐ต) = ๐ต) |
21 | 20 | oveq1d 7424 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ ((1 ยท
๐ต) mod 8) = (๐ต mod 8)) |
22 | 17, 21 | eqtrd 2773 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ ((๐ด ยท ๐ต) mod 8) = (๐ต mod 8)) |
23 | 22 | eleq1d 2819 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 1) โ (((๐ด ยท ๐ต) mod 8) โ {1, 7} โ (๐ต mod 8) โ {1,
7})) |
24 | 3 | ad2antrr 725 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ ๐ด โ
โ) |
25 | | neg1rr 12327 |
. . . . . . . 8
โข -1 โ
โ |
26 | 25 | a1i 11 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ -1 โ
โ) |
27 | | simplr 768 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ ๐ต โ
โค) |
28 | 9 | a1i 11 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ 8 โ
โ+) |
29 | | simpr 486 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ (๐ด mod 8) = 7) |
30 | 13 | simpri 487 |
. . . . . . . 8
โข (-1 mod
8) = 7 |
31 | 29, 30 | eqtr4di 2791 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ (๐ด mod 8) = (-1 mod
8)) |
32 | | modmul1 13889 |
. . . . . . 7
โข (((๐ด โ โ โง -1 โ
โ) โง (๐ต โ
โค โง 8 โ โ+) โง (๐ด mod 8) = (-1 mod 8)) โ ((๐ด ยท ๐ต) mod 8) = ((-1 ยท ๐ต) mod 8)) |
33 | 24, 26, 27, 28, 31, 32 | syl221anc 1382 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ ((๐ด ยท ๐ต) mod 8) = ((-1 ยท ๐ต) mod 8)) |
34 | 18 | ad2antlr 726 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ ๐ต โ
โ) |
35 | 34 | mulm1d 11666 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ (-1 ยท
๐ต) = -๐ต) |
36 | 35 | oveq1d 7424 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ ((-1
ยท ๐ต) mod 8) =
(-๐ต mod
8)) |
37 | 33, 36 | eqtrd 2773 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ ((๐ด ยท ๐ต) mod 8) = (-๐ต mod 8)) |
38 | 37 | eleq1d 2819 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ (((๐ด ยท ๐ต) mod 8) โ {1, 7} โ (-๐ต mod 8) โ {1,
7})) |
39 | | znegcl 12597 |
. . . . . . . 8
โข (๐ต โ โค โ -๐ต โ
โค) |
40 | | oveq1 7416 |
. . . . . . . . . . 11
โข (๐ฅ = -๐ต โ (๐ฅ mod 8) = (-๐ต mod 8)) |
41 | 40 | eleq1d 2819 |
. . . . . . . . . 10
โข (๐ฅ = -๐ต โ ((๐ฅ mod 8) โ {1, 7} โ (-๐ต mod 8) โ {1,
7})) |
42 | | negeq 11452 |
. . . . . . . . . . . 12
โข (๐ฅ = -๐ต โ -๐ฅ = --๐ต) |
43 | 42 | oveq1d 7424 |
. . . . . . . . . . 11
โข (๐ฅ = -๐ต โ (-๐ฅ mod 8) = (--๐ต mod 8)) |
44 | 43 | eleq1d 2819 |
. . . . . . . . . 10
โข (๐ฅ = -๐ต โ ((-๐ฅ mod 8) โ {1, 7} โ (--๐ต mod 8) โ {1,
7})) |
45 | 41, 44 | imbi12d 345 |
. . . . . . . . 9
โข (๐ฅ = -๐ต โ (((๐ฅ mod 8) โ {1, 7} โ (-๐ฅ mod 8) โ {1, 7}) โ
((-๐ต mod 8) โ {1, 7}
โ (--๐ต mod 8) โ
{1, 7}))) |
46 | | zcn 12563 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
47 | | neg1cn 12326 |
. . . . . . . . . . . . . . . . . . 19
โข -1 โ
โ |
48 | | mulcom 11196 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฅ โ โ โง -1 โ
โ) โ (๐ฅ ยท
-1) = (-1 ยท ๐ฅ)) |
49 | 47, 48 | mpan2 690 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ (๐ฅ ยท -1) = (-1 ยท
๐ฅ)) |
50 | | mulm1 11655 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ (-1
ยท ๐ฅ) = -๐ฅ) |
51 | 49, 50 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โ โ (๐ฅ ยท -1) = -๐ฅ) |
52 | 46, 51 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ (๐ฅ ยท -1) = -๐ฅ) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ (๐ฅ ยท -1) = -๐ฅ) |
54 | 53 | oveq1d 7424 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ ((๐ฅ ยท -1) mod 8) = (-๐ฅ mod 8)) |
55 | | zre 12562 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ ๐ฅ โ
โ) |
57 | | 1red 11215 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ 1 โ
โ) |
58 | | neg1z 12598 |
. . . . . . . . . . . . . . . 16
โข -1 โ
โค |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ -1 โ
โค) |
60 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ 8 โ
โ+) |
61 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ (๐ฅ mod 8) = 1) |
62 | 61, 14 | eqtr4di 2791 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ (๐ฅ mod 8) = (1 mod
8)) |
63 | | modmul1 13889 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ โ โง 1 โ
โ) โง (-1 โ โค โง 8 โ โ+) โง
(๐ฅ mod 8) = (1 mod 8))
โ ((๐ฅ ยท -1) mod
8) = ((1 ยท -1) mod 8)) |
64 | 56, 57, 59, 60, 62, 63 | syl221anc 1382 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ ((๐ฅ ยท -1) mod 8) = ((1
ยท -1) mod 8)) |
65 | 54, 64 | eqtr3d 2775 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ (-๐ฅ mod 8) = ((1 ยท -1) mod
8)) |
66 | 47 | mullidi 11219 |
. . . . . . . . . . . . . . 15
โข (1
ยท -1) = -1 |
67 | 66 | oveq1i 7419 |
. . . . . . . . . . . . . 14
โข ((1
ยท -1) mod 8) = (-1 mod 8) |
68 | 67, 30 | eqtri 2761 |
. . . . . . . . . . . . 13
โข ((1
ยท -1) mod 8) = 7 |
69 | 65, 68 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 1) โ (-๐ฅ mod 8) = 7) |
70 | 69 | ex 414 |
. . . . . . . . . . 11
โข (๐ฅ โ โค โ ((๐ฅ mod 8) = 1 โ (-๐ฅ mod 8) = 7)) |
71 | 52 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ (๐ฅ ยท -1) = -๐ฅ) |
72 | 71 | oveq1d 7424 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ ((๐ฅ ยท -1) mod 8) = (-๐ฅ mod 8)) |
73 | 55 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ ๐ฅ โ
โ) |
74 | 25 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ -1 โ
โ) |
75 | 58 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ -1 โ
โค) |
76 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ 8 โ
โ+) |
77 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ (๐ฅ mod 8) = 7) |
78 | 77, 30 | eqtr4di 2791 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ (๐ฅ mod 8) = (-1 mod
8)) |
79 | | modmul1 13889 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ โ โง -1 โ
โ) โง (-1 โ โค โง 8 โ โ+) โง
(๐ฅ mod 8) = (-1 mod 8))
โ ((๐ฅ ยท -1) mod
8) = ((-1 ยท -1) mod 8)) |
80 | 73, 74, 75, 76, 78, 79 | syl221anc 1382 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ ((๐ฅ ยท -1) mod 8) = ((-1
ยท -1) mod 8)) |
81 | 72, 80 | eqtr3d 2775 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ (-๐ฅ mod 8) = ((-1 ยท -1) mod
8)) |
82 | | neg1mulneg1e1 12425 |
. . . . . . . . . . . . . . 15
โข (-1
ยท -1) = 1 |
83 | 82 | oveq1i 7419 |
. . . . . . . . . . . . . 14
โข ((-1
ยท -1) mod 8) = (1 mod 8) |
84 | 83, 14 | eqtri 2761 |
. . . . . . . . . . . . 13
โข ((-1
ยท -1) mod 8) = 1 |
85 | 81, 84 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โค โง (๐ฅ mod 8) = 7) โ (-๐ฅ mod 8) = 1) |
86 | 85 | ex 414 |
. . . . . . . . . . 11
โข (๐ฅ โ โค โ ((๐ฅ mod 8) = 7 โ (-๐ฅ mod 8) = 1)) |
87 | 70, 86 | orim12d 964 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ (((๐ฅ mod 8) = 1 โจ (๐ฅ mod 8) = 7) โ ((-๐ฅ mod 8) = 7 โจ (-๐ฅ mod 8) = 1))) |
88 | | ovex 7442 |
. . . . . . . . . . 11
โข (๐ฅ mod 8) โ
V |
89 | 88 | elpr 4652 |
. . . . . . . . . 10
โข ((๐ฅ mod 8) โ {1, 7} โ
((๐ฅ mod 8) = 1 โจ (๐ฅ mod 8) = 7)) |
90 | | ovex 7442 |
. . . . . . . . . . . 12
โข (-๐ฅ mod 8) โ
V |
91 | 90 | elpr 4652 |
. . . . . . . . . . 11
โข ((-๐ฅ mod 8) โ {1, 7} โ
((-๐ฅ mod 8) = 1 โจ
(-๐ฅ mod 8) =
7)) |
92 | | orcom 869 |
. . . . . . . . . . 11
โข (((-๐ฅ mod 8) = 1 โจ (-๐ฅ mod 8) = 7) โ ((-๐ฅ mod 8) = 7 โจ (-๐ฅ mod 8) = 1)) |
93 | 91, 92 | bitri 275 |
. . . . . . . . . 10
โข ((-๐ฅ mod 8) โ {1, 7} โ
((-๐ฅ mod 8) = 7 โจ
(-๐ฅ mod 8) =
1)) |
94 | 87, 89, 93 | 3imtr4g 296 |
. . . . . . . . 9
โข (๐ฅ โ โค โ ((๐ฅ mod 8) โ {1, 7} โ
(-๐ฅ mod 8) โ {1,
7})) |
95 | 45, 94 | vtoclga 3566 |
. . . . . . . 8
โข (-๐ต โ โค โ ((-๐ต mod 8) โ {1, 7} โ
(--๐ต mod 8) โ {1,
7})) |
96 | 39, 95 | syl 17 |
. . . . . . 7
โข (๐ต โ โค โ ((-๐ต mod 8) โ {1, 7} โ
(--๐ต mod 8) โ {1,
7})) |
97 | 18 | negnegd 11562 |
. . . . . . . . 9
โข (๐ต โ โค โ --๐ต = ๐ต) |
98 | 97 | oveq1d 7424 |
. . . . . . . 8
โข (๐ต โ โค โ (--๐ต mod 8) = (๐ต mod 8)) |
99 | 98 | eleq1d 2819 |
. . . . . . 7
โข (๐ต โ โค โ ((--๐ต mod 8) โ {1, 7} โ
(๐ต mod 8) โ {1,
7})) |
100 | 96, 99 | sylibd 238 |
. . . . . 6
โข (๐ต โ โค โ ((-๐ต mod 8) โ {1, 7} โ
(๐ต mod 8) โ {1,
7})) |
101 | | oveq1 7416 |
. . . . . . . . 9
โข (๐ฅ = ๐ต โ (๐ฅ mod 8) = (๐ต mod 8)) |
102 | 101 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = ๐ต โ ((๐ฅ mod 8) โ {1, 7} โ (๐ต mod 8) โ {1,
7})) |
103 | | negeq 11452 |
. . . . . . . . . 10
โข (๐ฅ = ๐ต โ -๐ฅ = -๐ต) |
104 | 103 | oveq1d 7424 |
. . . . . . . . 9
โข (๐ฅ = ๐ต โ (-๐ฅ mod 8) = (-๐ต mod 8)) |
105 | 104 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = ๐ต โ ((-๐ฅ mod 8) โ {1, 7} โ (-๐ต mod 8) โ {1,
7})) |
106 | 102, 105 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = ๐ต โ (((๐ฅ mod 8) โ {1, 7} โ (-๐ฅ mod 8) โ {1, 7}) โ
((๐ต mod 8) โ {1, 7}
โ (-๐ต mod 8) โ
{1, 7}))) |
107 | 106, 94 | vtoclga 3566 |
. . . . . 6
โข (๐ต โ โค โ ((๐ต mod 8) โ {1, 7} โ
(-๐ต mod 8) โ {1,
7})) |
108 | 100, 107 | impbid 211 |
. . . . 5
โข (๐ต โ โค โ ((-๐ต mod 8) โ {1, 7} โ
(๐ต mod 8) โ {1,
7})) |
109 | 108 | ad2antlr 726 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ ((-๐ต mod 8) โ {1, 7} โ
(๐ต mod 8) โ {1,
7})) |
110 | 38, 109 | bitrd 279 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) = 7) โ (((๐ด ยท ๐ต) mod 8) โ {1, 7} โ (๐ต mod 8) โ {1,
7})) |
111 | 23, 110 | jaodan 957 |
. 2
โข (((๐ด โ โค โง ๐ต โ โค) โง ((๐ด mod 8) = 1 โจ (๐ด mod 8) = 7)) โ (((๐ด ยท ๐ต) mod 8) โ {1, 7} โ (๐ต mod 8) โ {1,
7})) |
112 | 2, 111 | sylan2b 595 |
1
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ด mod 8) โ {1, 7}) โ
(((๐ด ยท ๐ต) mod 8) โ {1, 7} โ
(๐ต mod 8) โ {1,
7})) |