Step | Hyp | Ref
| Expression |
1 | | prm2orodd 16568 |
. 2
โข (๐ โ โ โ (๐ = 2 โจ ยฌ 2 โฅ ๐)) |
2 | | 2lgslem4 26757 |
. . . . . 6
โข ((2
/L 2) = 1 โ (2 mod 8) โ {1, 7}) |
3 | 2 | a1i 11 |
. . . . 5
โข (๐ = 2 โ ((2
/L 2) = 1 โ (2 mod 8) โ {1, 7})) |
4 | | oveq2 7366 |
. . . . . 6
โข (๐ = 2 โ (2
/L ๐) =
(2 /L 2)) |
5 | 4 | eqeq1d 2739 |
. . . . 5
โข (๐ = 2 โ ((2
/L ๐) = 1
โ (2 /L 2) = 1)) |
6 | | oveq1 7365 |
. . . . . 6
โข (๐ = 2 โ (๐ mod 8) = (2 mod 8)) |
7 | 6 | eleq1d 2823 |
. . . . 5
โข (๐ = 2 โ ((๐ mod 8) โ {1, 7} โ (2 mod 8)
โ {1, 7})) |
8 | 3, 5, 7 | 3bitr4d 311 |
. . . 4
โข (๐ = 2 โ ((2
/L ๐) = 1
โ (๐ mod 8) โ {1,
7})) |
9 | 8 | a1d 25 |
. . 3
โข (๐ = 2 โ (๐ โ โ โ ((2
/L ๐) = 1
โ (๐ mod 8) โ {1,
7}))) |
10 | | 2prm 16569 |
. . . . . . . . . 10
โข 2 โ
โ |
11 | | prmnn 16551 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
12 | | dvdsprime 16564 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ) โ (๐
โฅ 2 โ (๐ = 2
โจ ๐ =
1))) |
13 | 10, 11, 12 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โฅ 2 โ (๐ = 2 โจ ๐ = 1))) |
14 | | z2even 16253 |
. . . . . . . . . . . . 13
โข 2 โฅ
2 |
15 | | breq2 5110 |
. . . . . . . . . . . . 13
โข (๐ = 2 โ (2 โฅ ๐ โ 2 โฅ
2)) |
16 | 14, 15 | mpbiri 258 |
. . . . . . . . . . . 12
โข (๐ = 2 โ 2 โฅ ๐) |
17 | 16 | a1d 25 |
. . . . . . . . . . 11
โข (๐ = 2 โ (๐ โ โ โ 2 โฅ ๐)) |
18 | | eleq1 2826 |
. . . . . . . . . . . 12
โข (๐ = 1 โ (๐ โ โ โ 1 โ
โ)) |
19 | | 1nprm 16556 |
. . . . . . . . . . . . 13
โข ยฌ 1
โ โ |
20 | 19 | pm2.21i 119 |
. . . . . . . . . . . 12
โข (1 โ
โ โ 2 โฅ ๐) |
21 | 18, 20 | syl6bi 253 |
. . . . . . . . . . 11
โข (๐ = 1 โ (๐ โ โ โ 2 โฅ ๐)) |
22 | 17, 21 | jaoi 856 |
. . . . . . . . . 10
โข ((๐ = 2 โจ ๐ = 1) โ (๐ โ โ โ 2 โฅ ๐)) |
23 | 22 | com12 32 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ = 2 โจ ๐ = 1) โ 2 โฅ ๐)) |
24 | 13, 23 | sylbid 239 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โฅ 2 โ 2 โฅ
๐)) |
25 | 24 | con3dimp 410 |
. . . . . . 7
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ยฌ
๐ โฅ
2) |
26 | | 2z 12536 |
. . . . . . 7
โข 2 โ
โค |
27 | 25, 26 | jctil 521 |
. . . . . 6
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (2 โ
โค โง ยฌ ๐
โฅ 2)) |
28 | | 2lgslem1 26745 |
. . . . . . 7
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(โฏโ{๐ฅ โ
โค โฃ โ๐
โ (1...((๐ โ 1)
/ 2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐))}) = (((๐ โ 1) / 2) โ
(โโ(๐ /
4)))) |
29 | 28 | eqcomd 2743 |
. . . . . 6
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (((๐ โ 1) / 2) โ
(โโ(๐ / 4))) =
(โฏโ{๐ฅ โ
โค โฃ โ๐
โ (1...((๐ โ 1)
/ 2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐))})) |
30 | | nnoddn2prmb 16686 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ยฌ 2 โฅ ๐)) |
31 | 30 | biimpri 227 |
. . . . . . . . 9
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ๐ โ (โ โ
{2})) |
32 | 31 | 3ad2ant1 1134 |
. . . . . . . 8
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง (2 โ
โค โง ยฌ ๐
โฅ 2) โง (((๐
โ 1) / 2) โ (โโ(๐ / 4))) = (โฏโ{๐ฅ โ โค โฃ โ๐ โ (1...((๐ โ 1) / 2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐))})) โ ๐ โ (โ โ
{2})) |
33 | | eqid 2737 |
. . . . . . . 8
โข ((๐ โ 1) / 2) = ((๐ โ 1) /
2) |
34 | | eqid 2737 |
. . . . . . . 8
โข (๐ฆ โ (1...((๐ โ 1) / 2)) โฆ if((๐ฆ ยท 2) < (๐ / 2), (๐ฆ ยท 2), (๐ โ (๐ฆ ยท 2)))) = (๐ฆ โ (1...((๐ โ 1) / 2)) โฆ if((๐ฆ ยท 2) < (๐ / 2), (๐ฆ ยท 2), (๐ โ (๐ฆ ยท 2)))) |
35 | | eqid 2737 |
. . . . . . . 8
โข
(โโ(๐ /
4)) = (โโ(๐ /
4)) |
36 | | eqid 2737 |
. . . . . . . 8
โข (((๐ โ 1) / 2) โ
(โโ(๐ / 4))) =
(((๐ โ 1) / 2)
โ (โโ(๐ /
4))) |
37 | 32, 33, 34, 35, 36 | gausslemma2d 26725 |
. . . . . . 7
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง (2 โ
โค โง ยฌ ๐
โฅ 2) โง (((๐
โ 1) / 2) โ (โโ(๐ / 4))) = (โฏโ{๐ฅ โ โค โฃ โ๐ โ (1...((๐ โ 1) / 2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐))})) โ (2 /L ๐) = (-1โ(((๐ โ 1) / 2) โ
(โโ(๐ /
4))))) |
38 | 37 | eqeq1d 2739 |
. . . . . 6
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง (2 โ
โค โง ยฌ ๐
โฅ 2) โง (((๐
โ 1) / 2) โ (โโ(๐ / 4))) = (โฏโ{๐ฅ โ โค โฃ โ๐ โ (1...((๐ โ 1) / 2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐))})) โ ((2 /L ๐) = 1 โ (-1โ(((๐ โ 1) / 2) โ
(โโ(๐ / 4)))) =
1)) |
39 | 27, 29, 38 | mpd3an23 1464 |
. . . . 5
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ((2
/L ๐) = 1
โ (-1โ(((๐
โ 1) / 2) โ (โโ(๐ / 4)))) = 1)) |
40 | 36 | 2lgslem2 26746 |
. . . . . 6
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (((๐ โ 1) / 2) โ
(โโ(๐ / 4)))
โ โค) |
41 | | m1exp1 16259 |
. . . . . 6
โข ((((๐ โ 1) / 2) โ
(โโ(๐ / 4)))
โ โค โ ((-1โ(((๐ โ 1) / 2) โ
(โโ(๐ / 4)))) =
1 โ 2 โฅ (((๐
โ 1) / 2) โ (โโ(๐ / 4))))) |
42 | 40, 41 | syl 17 |
. . . . 5
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
((-1โ(((๐ โ 1) /
2) โ (โโ(๐ / 4)))) = 1 โ 2 โฅ (((๐ โ 1) / 2) โ
(โโ(๐ /
4))))) |
43 | | 2nn 12227 |
. . . . . . 7
โข 2 โ
โ |
44 | | dvdsval3 16141 |
. . . . . . 7
โข ((2
โ โ โง (((๐
โ 1) / 2) โ (โโ(๐ / 4))) โ โค) โ (2 โฅ
(((๐ โ 1) / 2)
โ (โโ(๐ /
4))) โ ((((๐ โ
1) / 2) โ (โโ(๐ / 4))) mod 2) = 0)) |
45 | 43, 40, 44 | sylancr 588 |
. . . . . 6
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (2
โฅ (((๐ โ 1) /
2) โ (โโ(๐ / 4))) โ ((((๐ โ 1) / 2) โ
(โโ(๐ / 4)))
mod 2) = 0)) |
46 | 36 | 2lgslem3 26755 |
. . . . . . . 8
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ((((๐ โ 1) / 2) โ
(โโ(๐ / 4)))
mod 2) = if((๐ mod 8)
โ {1, 7}, 0, 1)) |
47 | 11, 46 | sylan 581 |
. . . . . . 7
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ((((๐ โ 1) / 2) โ
(โโ(๐ / 4)))
mod 2) = if((๐ mod 8)
โ {1, 7}, 0, 1)) |
48 | 47 | eqeq1d 2739 |
. . . . . 6
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(((((๐ โ 1) / 2)
โ (โโ(๐ /
4))) mod 2) = 0 โ if((๐ mod 8) โ {1, 7}, 0, 1) =
0)) |
49 | | ax-1 6 |
. . . . . . . . 9
โข ((๐ mod 8) โ {1, 7} โ
(if((๐ mod 8) โ {1,
7}, 0, 1) = 0 โ (๐ mod
8) โ {1, 7})) |
50 | | iffalse 4496 |
. . . . . . . . . . 11
โข (ยฌ
(๐ mod 8) โ {1, 7}
โ if((๐ mod 8) โ
{1, 7}, 0, 1) = 1) |
51 | 50 | eqeq1d 2739 |
. . . . . . . . . 10
โข (ยฌ
(๐ mod 8) โ {1, 7}
โ (if((๐ mod 8) โ
{1, 7}, 0, 1) = 0 โ 1 = 0)) |
52 | | ax-1ne0 11121 |
. . . . . . . . . . 11
โข 1 โ
0 |
53 | | eqneqall 2955 |
. . . . . . . . . . 11
โข (1 = 0
โ (1 โ 0 โ (๐
mod 8) โ {1, 7})) |
54 | 52, 53 | mpi 20 |
. . . . . . . . . 10
โข (1 = 0
โ (๐ mod 8) โ {1,
7}) |
55 | 51, 54 | syl6bi 253 |
. . . . . . . . 9
โข (ยฌ
(๐ mod 8) โ {1, 7}
โ (if((๐ mod 8) โ
{1, 7}, 0, 1) = 0 โ (๐
mod 8) โ {1, 7})) |
56 | 49, 55 | pm2.61i 182 |
. . . . . . . 8
โข
(if((๐ mod 8) โ
{1, 7}, 0, 1) = 0 โ (๐
mod 8) โ {1, 7}) |
57 | | iftrue 4493 |
. . . . . . . 8
โข ((๐ mod 8) โ {1, 7} โ
if((๐ mod 8) โ {1, 7},
0, 1) = 0) |
58 | 56, 57 | impbii 208 |
. . . . . . 7
โข
(if((๐ mod 8) โ
{1, 7}, 0, 1) = 0 โ (๐
mod 8) โ {1, 7}) |
59 | 58 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(if((๐ mod 8) โ {1,
7}, 0, 1) = 0 โ (๐ mod
8) โ {1, 7})) |
60 | 45, 48, 59 | 3bitrd 305 |
. . . . 5
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (2
โฅ (((๐ โ 1) /
2) โ (โโ(๐ / 4))) โ (๐ mod 8) โ {1, 7})) |
61 | 39, 42, 60 | 3bitrd 305 |
. . . 4
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ((2
/L ๐) = 1
โ (๐ mod 8) โ {1,
7})) |
62 | 61 | expcom 415 |
. . 3
โข (ยฌ 2
โฅ ๐ โ (๐ โ โ โ ((2
/L ๐) = 1
โ (๐ mod 8) โ {1,
7}))) |
63 | 9, 62 | jaoi 856 |
. 2
โข ((๐ = 2 โจ ยฌ 2 โฅ ๐) โ (๐ โ โ โ ((2
/L ๐) = 1
โ (๐ mod 8) โ {1,
7}))) |
64 | 1, 63 | mpcom 38 |
1
โข (๐ โ โ โ ((2
/L ๐) = 1
โ (๐ mod 8) โ {1,
7})) |