Step | Hyp | Ref
| Expression |
1 | | prmnn 16551 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
2 | 1 | nnnn0d 12474 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
3 | 2 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ ๐ โ
โ0) |
4 | | 4nn 12237 |
. . . . . . . 8
โข 4 โ
โ |
5 | 3, 4 | jctir 522 |
. . . . . . 7
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ (๐ โ โ0
โง 4 โ โ)) |
6 | | fldivnn0 13728 |
. . . . . . 7
โข ((๐ โ โ0
โง 4 โ โ) โ (โโ(๐ / 4)) โ
โ0) |
7 | | nn0p1nn 12453 |
. . . . . . 7
โข
((โโ(๐ /
4)) โ โ0 โ ((โโ(๐ / 4)) + 1) โ โ) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . 6
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ
((โโ(๐ / 4)) +
1) โ โ) |
9 | | elnnuz 12808 |
. . . . . 6
โข
(((โโ(๐
/ 4)) + 1) โ โ โ ((โโ(๐ / 4)) + 1) โ
(โคโฅโ1)) |
10 | 8, 9 | sylib 217 |
. . . . 5
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ
((โโ(๐ / 4)) +
1) โ (โคโฅโ1)) |
11 | | fzss1 13481 |
. . . . 5
โข
(((โโ(๐
/ 4)) + 1) โ (โคโฅโ1) โ
(((โโ(๐ / 4)) +
1)...((๐ โ 1) / 2))
โ (1...((๐ โ 1)
/ 2))) |
12 | | rexss 4016 |
. . . . 5
โข
((((โโ(๐
/ 4)) + 1)...((๐ โ 1)
/ 2)) โ (1...((๐
โ 1) / 2)) โ (โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2) โ โ๐ โ (1...((๐ โ 1) / 2))(๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โง ๐ฅ = (๐ ยท 2)))) |
13 | 10, 11, 12 | 3syl 18 |
. . . 4
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ
(โ๐ โ
(((โโ(๐ / 4)) +
1)...((๐ โ 1) /
2))๐ฅ = (๐ ยท 2) โ โ๐ โ (1...((๐ โ 1) / 2))(๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โง ๐ฅ = (๐ ยท 2)))) |
14 | | ancom 462 |
. . . . . 6
โข ((๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โง ๐ฅ = (๐ ยท 2)) โ (๐ฅ = (๐ ยท 2) โง ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)))) |
15 | 2, 4 | jctir 522 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐ โ โ0
โง 4 โ โ)) |
16 | 15, 6 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(โโ(๐ / 4))
โ โ0) |
17 | 16 | nn0zd 12526 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
(โโ(๐ / 4))
โ โค) |
18 | 17 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ
(โโ(๐ / 4))
โ โค) |
19 | | elfzelz 13442 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...((๐ โ 1) / 2)) โ ๐ โ โค) |
20 | | zltp1le 12554 |
. . . . . . . . . . . . . 14
โข
(((โโ(๐
/ 4)) โ โค โง ๐ โ โค) โ
((โโ(๐ / 4))
< ๐ โ
((โโ(๐ / 4)) +
1) โค ๐)) |
21 | 18, 19, 20 | syl2an 597 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ
((โโ(๐ / 4))
< ๐ โ
((โโ(๐ / 4)) +
1) โค ๐)) |
22 | 21 | bicomd 222 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ
(((โโ(๐ / 4)) +
1) โค ๐ โ
(โโ(๐ / 4))
< ๐)) |
23 | 22 | anbi1d 631 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ
((((โโ(๐ / 4))
+ 1) โค ๐ โง ๐ โค ((๐ โ 1) / 2)) โ
((โโ(๐ / 4))
< ๐ โง ๐ โค ((๐ โ 1) / 2)))) |
24 | 19 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ ๐ โ โค) |
25 | 17 | peano2zd 12611 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
((โโ(๐ / 4)) +
1) โ โค) |
26 | 25 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
((โโ(๐ / 4)) +
1) โ โค) |
27 | 26 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ
((โโ(๐ / 4)) +
1) โ โค) |
28 | | prmz 16552 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โค) |
29 | | oddm1d2 16243 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ ((๐ โ 1) / 2) โ
โค)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (ยฌ 2
โฅ ๐ โ ((๐ โ 1) / 2) โ
โค)) |
31 | 30 | biimpa 478 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ((๐ โ 1) / 2) โ
โค) |
32 | 31 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ ((๐ โ 1) / 2) โ
โค) |
33 | | elfz 13431 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง
((โโ(๐ / 4)) +
1) โ โค โง ((๐
โ 1) / 2) โ โค) โ (๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โ
(((โโ(๐ / 4)) +
1) โค ๐ โง ๐ โค ((๐ โ 1) / 2)))) |
34 | 24, 27, 32, 33 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ (๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โ
(((โโ(๐ / 4)) +
1) โค ๐ โง ๐ โค ((๐ โ 1) / 2)))) |
35 | | elfzle2 13446 |
. . . . . . . . . . . . 13
โข (๐ โ (1...((๐ โ 1) / 2)) โ ๐ โค ((๐ โ 1) / 2)) |
36 | 35 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ ๐ โค ((๐ โ 1) / 2)) |
37 | 36 | biantrud 533 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ
((โโ(๐ / 4))
< ๐ โ
((โโ(๐ / 4))
< ๐ โง ๐ โค ((๐ โ 1) / 2)))) |
38 | 23, 34, 37 | 3bitr4d 311 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ (๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โ
(โโ(๐ / 4))
< ๐)) |
39 | 28 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ ๐ โ
โค) |
40 | | 2lgslem1a2 26741 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ
((โโ(๐ / 4))
< ๐ โ (๐ / 2) < (๐ ยท 2))) |
41 | 39, 19, 40 | syl2an 597 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ
((โโ(๐ / 4))
< ๐ โ (๐ / 2) < (๐ ยท 2))) |
42 | 38, 41 | bitrd 279 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ (๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โ (๐ / 2) < (๐ ยท 2))) |
43 | | 2lgslem1a1 26740 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
โ๐ โ
(1...((๐ โ 1) /
2))(๐ ยท 2) = ((๐ ยท 2) mod ๐)) |
44 | 1, 43 | sylan 581 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
โ๐ โ
(1...((๐ โ 1) /
2))(๐ ยท 2) = ((๐ ยท 2) mod ๐)) |
45 | 44 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ
โ๐ โ
(1...((๐ โ 1) /
2))(๐ ยท 2) = ((๐ ยท 2) mod ๐)) |
46 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ ยท 2) = (๐ ยท 2)) |
47 | 46 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐ ยท 2) mod ๐) = ((๐ ยท 2) mod ๐)) |
48 | 46, 47 | eqeq12d 2753 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ ยท 2) = ((๐ ยท 2) mod ๐) โ (๐ ยท 2) = ((๐ ยท 2) mod ๐))) |
49 | 48 | rspccva 3581 |
. . . . . . . . . . 11
โข
((โ๐ โ
(1...((๐ โ 1) /
2))(๐ ยท 2) = ((๐ ยท 2) mod ๐) โง ๐ โ (1...((๐ โ 1) / 2))) โ (๐ ยท 2) = ((๐ ยท 2) mod ๐)) |
50 | 45, 49 | sylan 581 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ (๐ ยท 2) = ((๐ ยท 2) mod ๐)) |
51 | 50 | breq2d 5118 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ ((๐ / 2) < (๐ ยท 2) โ (๐ / 2) < ((๐ ยท 2) mod ๐))) |
52 | 42, 51 | bitrd 279 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ (๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โ (๐ / 2) < ((๐ ยท 2) mod ๐))) |
53 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ฅ = (๐ ยท 2) โ (๐ฅ mod ๐) = ((๐ ยท 2) mod ๐)) |
54 | 53 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ฅ = (๐ ยท 2) โ ((๐ ยท 2) mod ๐) = (๐ฅ mod ๐)) |
55 | 54 | breq2d 5118 |
. . . . . . . 8
โข (๐ฅ = (๐ ยท 2) โ ((๐ / 2) < ((๐ ยท 2) mod ๐) โ (๐ / 2) < (๐ฅ mod ๐))) |
56 | 52, 55 | sylan9bb 511 |
. . . . . . 7
โข
(((((๐ โ
โ โง ยฌ 2 โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โง ๐ฅ = (๐ ยท 2)) โ (๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โ (๐ / 2) < (๐ฅ mod ๐))) |
57 | 56 | pm5.32da 580 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ ((๐ฅ = (๐ ยท 2) โง ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))) โ (๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐)))) |
58 | 14, 57 | bitrid 283 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โง ๐ โ (1...((๐ โ 1) / 2))) โ ((๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โง ๐ฅ = (๐ ยท 2)) โ (๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐)))) |
59 | 58 | rexbidva 3174 |
. . . 4
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ
(โ๐ โ
(1...((๐ โ 1) /
2))(๐ โ
(((โโ(๐ / 4)) +
1)...((๐ โ 1) / 2))
โง ๐ฅ = (๐ ยท 2)) โ
โ๐ โ
(1...((๐ โ 1) /
2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐)))) |
60 | 13, 59 | bitrd 279 |
. . 3
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ
(โ๐ โ
(((โโ(๐ / 4)) +
1)...((๐ โ 1) /
2))๐ฅ = (๐ ยท 2) โ โ๐ โ (1...((๐ โ 1) / 2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐)))) |
61 | 60 | bicomd 222 |
. 2
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ โค) โ
(โ๐ โ
(1...((๐ โ 1) /
2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐)) โ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2))) |
62 | 61 | rabbidva 3415 |
1
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ {๐ฅ โ โค โฃ
โ๐ โ
(1...((๐ โ 1) /
2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐))} = {๐ฅ โ โค โฃ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2)}) |