Step | Hyp | Ref
| Expression |
1 | | 2lgslem1a 26742 |
. . 3
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ {๐ฅ โ โค โฃ
โ๐ โ
(1...((๐ โ 1) /
2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐))} = {๐ฅ โ โค โฃ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2)}) |
2 | 1 | fveq2d 6847 |
. 2
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(โฏโ{๐ฅ โ
โค โฃ โ๐
โ (1...((๐ โ 1)
/ 2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐))}) = (โฏโ{๐ฅ โ โค โฃ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2)})) |
3 | | ovex 7391 |
. . 3
โข
(((โโ(๐
/ 4)) + 1)...((๐ โ 1)
/ 2)) โ V |
4 | 3 | mptex 7174 |
. . . . 5
โข (๐ฆ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โฆ (๐ฆ ยท 2)) โ
V |
5 | | f1oeq1 6773 |
. . . . 5
โข (๐ = (๐ฆ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โฆ (๐ฆ ยท 2)) โ (๐:(((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))โ1-1-ontoโ{๐ฅ โ โค โฃ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2)} โ (๐ฆ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โฆ (๐ฆ ยท
2)):(((โโ(๐ /
4)) + 1)...((๐ โ 1) /
2))โ1-1-ontoโ{๐ฅ โ โค โฃ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2)})) |
6 | | eqid 2737 |
. . . . . 6
โข
(((โโ(๐
/ 4)) + 1)...((๐ โ 1)
/ 2)) = (((โโ(๐
/ 4)) + 1)...((๐ โ 1)
/ 2)) |
7 | | eqid 2737 |
. . . . . 6
โข (๐ฆ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โฆ (๐ฆ ยท 2)) = (๐ฆ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โฆ (๐ฆ ยท 2)) |
8 | 6, 7 | 2lgslem1b 26743 |
. . . . 5
โข (๐ฆ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2)) โฆ (๐ฆ ยท
2)):(((โโ(๐ /
4)) + 1)...((๐ โ 1) /
2))โ1-1-ontoโ{๐ฅ โ โค โฃ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2)} |
9 | 4, 5, 8 | ceqsexv2d 3498 |
. . . 4
โข
โ๐ ๐:(((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))โ1-1-ontoโ{๐ฅ โ โค โฃ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2)} |
10 | 9 | a1i 11 |
. . 3
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
โ๐ ๐:(((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))โ1-1-ontoโ{๐ฅ โ โค โฃ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2)}) |
11 | | hasheqf1oi 14252 |
. . 3
โข
((((โโ(๐
/ 4)) + 1)...((๐ โ 1)
/ 2)) โ V โ (โ๐ ๐:(((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))โ1-1-ontoโ{๐ฅ โ โค โฃ โ๐ โ (((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))๐ฅ = (๐ ยท 2)} โ
(โฏโ(((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))) = (โฏโ{๐ฅ โ โค โฃ
โ๐ โ
(((โโ(๐ / 4)) +
1)...((๐ โ 1) /
2))๐ฅ = (๐ ยท 2)}))) |
12 | 3, 10, 11 | mpsyl 68 |
. 2
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(โฏโ(((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))) = (โฏโ{๐ฅ โ โค โฃ
โ๐ โ
(((โโ(๐ / 4)) +
1)...((๐ โ 1) /
2))๐ฅ = (๐ ยท 2)})) |
13 | | prmz 16552 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
14 | 13 | zred 12608 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
15 | | 4re 12238 |
. . . . . . . 8
โข 4 โ
โ |
16 | 15 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 4 โ
โ) |
17 | | 4ne0 12262 |
. . . . . . . 8
โข 4 โ
0 |
18 | 17 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 4 โ
0) |
19 | 14, 16, 18 | redivcld 11984 |
. . . . . 6
โข (๐ โ โ โ (๐ / 4) โ
โ) |
20 | 19 | flcld 13704 |
. . . . 5
โข (๐ โ โ โ
(โโ(๐ / 4))
โ โค) |
21 | 20 | adantr 482 |
. . . 4
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(โโ(๐ / 4))
โ โค) |
22 | | oddm1d2 16243 |
. . . . . 6
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ ((๐ โ 1) / 2) โ
โค)) |
23 | 13, 22 | syl 17 |
. . . . 5
โข (๐ โ โ โ (ยฌ 2
โฅ ๐ โ ((๐ โ 1) / 2) โ
โค)) |
24 | 23 | biimpa 478 |
. . . 4
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ((๐ โ 1) / 2) โ
โค) |
25 | | 2lgslem1c 26744 |
. . . 4
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(โโ(๐ / 4))
โค ((๐ โ 1) /
2)) |
26 | | eluz2 12770 |
. . . 4
โข (((๐ โ 1) / 2) โ
(โคโฅโ(โโ(๐ / 4))) โ ((โโ(๐ / 4)) โ โค โง
((๐ โ 1) / 2) โ
โค โง (โโ(๐ / 4)) โค ((๐ โ 1) / 2))) |
27 | 21, 24, 25, 26 | syl3anbrc 1344 |
. . 3
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ((๐ โ 1) / 2) โ
(โคโฅโ(โโ(๐ / 4)))) |
28 | | hashfzp1 14332 |
. . 3
โข (((๐ โ 1) / 2) โ
(โคโฅโ(โโ(๐ / 4))) โ
(โฏโ(((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))) = (((๐ โ 1) / 2) โ
(โโ(๐ /
4)))) |
29 | 27, 28 | syl 17 |
. 2
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(โฏโ(((โโ(๐ / 4)) + 1)...((๐ โ 1) / 2))) = (((๐ โ 1) / 2) โ
(โโ(๐ /
4)))) |
30 | 2, 12, 29 | 3eqtr2d 2783 |
1
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
(โฏโ{๐ฅ โ
โค โฃ โ๐
โ (1...((๐ โ 1)
/ 2))(๐ฅ = (๐ ยท 2) โง (๐ / 2) < (๐ฅ mod ๐))}) = (((๐ โ 1) / 2) โ
(โโ(๐ /
4)))) |