Step | Hyp | Ref
| Expression |
1 | | lgsdir2lem3 26678 |
. . 3
โข ((๐ โ โค โง ยฌ 2
โฅ ๐) โ (๐ mod 8) โ ({1, 7} โช {3,
5})) |
2 | | eleq1 2826 |
. . . . 5
โข ((๐ mod 8) = ๐
โ ((๐ mod 8) โ ({1, 7} โช {3, 5}) โ
๐
โ ({1, 7} โช {3,
5}))) |
3 | 2 | eqcoms 2745 |
. . . 4
โข (๐
= (๐ mod 8) โ ((๐ mod 8) โ ({1, 7} โช {3, 5}) โ
๐
โ ({1, 7} โช {3,
5}))) |
4 | | elun 4109 |
. . . . . 6
โข (๐
โ ({1, 7} โช {3, 5})
โ (๐
โ {1, 7}
โจ ๐
โ {3,
5})) |
5 | | elpri 4609 |
. . . . . . . 8
โข (๐
โ {3, 5} โ (๐
= 3 โจ ๐
= 5)) |
6 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐
= 3 โ (๐
โ2) = (3โ2)) |
7 | 6 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐
= 3 โ ((๐
โ2) โ 1) = ((3โ2) โ
1)) |
8 | 7 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐
= 3 โ (((๐
โ2) โ 1) / 8) = (((3โ2)
โ 1) / 8)) |
9 | | 2lgsoddprmlem3b 26762 |
. . . . . . . . . . . 12
โข
(((3โ2) โ 1) / 8) = 1 |
10 | 8, 9 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐
= 3 โ (((๐
โ2) โ 1) / 8) =
1) |
11 | 10 | breq2d 5118 |
. . . . . . . . . 10
โข (๐
= 3 โ (2 โฅ (((๐
โ2) โ 1) / 8) โ
2 โฅ 1)) |
12 | | n2dvds1 16251 |
. . . . . . . . . . 11
โข ยฌ 2
โฅ 1 |
13 | 12 | pm2.21i 119 |
. . . . . . . . . 10
โข (2
โฅ 1 โ ๐
โ
{1, 7}) |
14 | 11, 13 | syl6bi 253 |
. . . . . . . . 9
โข (๐
= 3 โ (2 โฅ (((๐
โ2) โ 1) / 8) โ
๐
โ {1,
7})) |
15 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐
= 5 โ (๐
โ2) = (5โ2)) |
16 | 15 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐
= 5 โ ((๐
โ2) โ 1) = ((5โ2) โ
1)) |
17 | 16 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐
= 5 โ (((๐
โ2) โ 1) / 8) = (((5โ2)
โ 1) / 8)) |
18 | 17 | breq2d 5118 |
. . . . . . . . . . 11
โข (๐
= 5 โ (2 โฅ (((๐
โ2) โ 1) / 8) โ
2 โฅ (((5โ2) โ 1) / 8))) |
19 | | 2lgsoddprmlem3c 26763 |
. . . . . . . . . . . 12
โข
(((5โ2) โ 1) / 8) = 3 |
20 | 19 | breq2i 5114 |
. . . . . . . . . . 11
โข (2
โฅ (((5โ2) โ 1) / 8) โ 2 โฅ 3) |
21 | 18, 20 | bitrdi 287 |
. . . . . . . . . 10
โข (๐
= 5 โ (2 โฅ (((๐
โ2) โ 1) / 8) โ
2 โฅ 3)) |
22 | | n2dvds3 16254 |
. . . . . . . . . . 11
โข ยฌ 2
โฅ 3 |
23 | 22 | pm2.21i 119 |
. . . . . . . . . 10
โข (2
โฅ 3 โ ๐
โ
{1, 7}) |
24 | 21, 23 | syl6bi 253 |
. . . . . . . . 9
โข (๐
= 5 โ (2 โฅ (((๐
โ2) โ 1) / 8) โ
๐
โ {1,
7})) |
25 | 14, 24 | jaoi 856 |
. . . . . . . 8
โข ((๐
= 3 โจ ๐
= 5) โ (2 โฅ (((๐
โ2) โ 1) / 8) โ ๐
โ {1,
7})) |
26 | 5, 25 | syl 17 |
. . . . . . 7
โข (๐
โ {3, 5} โ (2 โฅ
(((๐
โ2) โ 1) /
8) โ ๐
โ {1,
7})) |
27 | 26 | jao1i 857 |
. . . . . 6
โข ((๐
โ {1, 7} โจ ๐
โ {3, 5}) โ (2
โฅ (((๐
โ2)
โ 1) / 8) โ ๐
โ {1, 7})) |
28 | 4, 27 | sylbi 216 |
. . . . 5
โข (๐
โ ({1, 7} โช {3, 5})
โ (2 โฅ (((๐
โ2) โ 1) / 8) โ ๐
โ {1,
7})) |
29 | | elpri 4609 |
. . . . . 6
โข (๐
โ {1, 7} โ (๐
= 1 โจ ๐
= 7)) |
30 | | z0even 16250 |
. . . . . . . 8
โข 2 โฅ
0 |
31 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐
= 1 โ (๐
โ2) = (1โ2)) |
32 | 31 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐
= 1 โ ((๐
โ2) โ 1) = ((1โ2) โ
1)) |
33 | 32 | oveq1d 7373 |
. . . . . . . . 9
โข (๐
= 1 โ (((๐
โ2) โ 1) / 8) = (((1โ2)
โ 1) / 8)) |
34 | | 2lgsoddprmlem3a 26761 |
. . . . . . . . 9
โข
(((1โ2) โ 1) / 8) = 0 |
35 | 33, 34 | eqtrdi 2793 |
. . . . . . . 8
โข (๐
= 1 โ (((๐
โ2) โ 1) / 8) =
0) |
36 | 30, 35 | breqtrrid 5144 |
. . . . . . 7
โข (๐
= 1 โ 2 โฅ (((๐
โ2) โ 1) /
8)) |
37 | | 2z 12536 |
. . . . . . . . 9
โข 2 โ
โค |
38 | | 3z 12537 |
. . . . . . . . 9
โข 3 โ
โค |
39 | | dvdsmul1 16161 |
. . . . . . . . 9
โข ((2
โ โค โง 3 โ โค) โ 2 โฅ (2 ยท
3)) |
40 | 37, 38, 39 | mp2an 691 |
. . . . . . . 8
โข 2 โฅ
(2 ยท 3) |
41 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐
= 7 โ (๐
โ2) = (7โ2)) |
42 | 41 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐
= 7 โ ((๐
โ2) โ 1) = ((7โ2) โ
1)) |
43 | 42 | oveq1d 7373 |
. . . . . . . . 9
โข (๐
= 7 โ (((๐
โ2) โ 1) / 8) = (((7โ2)
โ 1) / 8)) |
44 | | 2lgsoddprmlem3d 26764 |
. . . . . . . . 9
โข
(((7โ2) โ 1) / 8) = (2 ยท 3) |
45 | 43, 44 | eqtrdi 2793 |
. . . . . . . 8
โข (๐
= 7 โ (((๐
โ2) โ 1) / 8) = (2 ยท
3)) |
46 | 40, 45 | breqtrrid 5144 |
. . . . . . 7
โข (๐
= 7 โ 2 โฅ (((๐
โ2) โ 1) /
8)) |
47 | 36, 46 | jaoi 856 |
. . . . . 6
โข ((๐
= 1 โจ ๐
= 7) โ 2 โฅ (((๐
โ2) โ 1) / 8)) |
48 | 29, 47 | syl 17 |
. . . . 5
โข (๐
โ {1, 7} โ 2 โฅ
(((๐
โ2) โ 1) /
8)) |
49 | 28, 48 | impbid1 224 |
. . . 4
โข (๐
โ ({1, 7} โช {3, 5})
โ (2 โฅ (((๐
โ2) โ 1) / 8) โ ๐
โ {1,
7})) |
50 | 3, 49 | syl6bi 253 |
. . 3
โข (๐
= (๐ mod 8) โ ((๐ mod 8) โ ({1, 7} โช {3, 5}) โ
(2 โฅ (((๐
โ2)
โ 1) / 8) โ ๐
โ {1, 7}))) |
51 | 1, 50 | syl5com 31 |
. 2
โข ((๐ โ โค โง ยฌ 2
โฅ ๐) โ (๐
= (๐ mod 8) โ (2 โฅ (((๐
โ2) โ 1) / 8) โ
๐
โ {1,
7}))) |
52 | 51 | 3impia 1118 |
1
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (2 โฅ (((๐
โ2) โ 1) / 8) โ
๐
โ {1,
7})) |