Step | Hyp | Ref
| Expression |
1 | | snmlff.f |
. 2
โข ๐น = (๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐)) |
2 | | fzfid 13938 |
. . . . . . 7
โข (๐ โ โ โ
(1...๐) โ
Fin) |
3 | | ssrab2 4078 |
. . . . . . 7
โข {๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โ (1...๐) |
4 | | ssfi 9173 |
. . . . . . 7
โข
(((1...๐) โ Fin
โง {๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โ (1...๐)) โ {๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โ Fin) |
5 | 2, 3, 4 | sylancl 587 |
. . . . . 6
โข (๐ โ โ โ {๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โ Fin) |
6 | | hashcl 14316 |
. . . . . 6
โข ({๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โ Fin โ (โฏโ{๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต}) โ
โ0) |
7 | 5, 6 | syl 17 |
. . . . 5
โข (๐ โ โ โ
(โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) โ
โ0) |
8 | 7 | nn0red 12533 |
. . . 4
โข (๐ โ โ โ
(โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) โ โ) |
9 | | nndivre 12253 |
. . . 4
โข
(((โฏโ{๐
โ (1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) โ โ โง ๐ โ โ) โ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โ โ) |
10 | 8, 9 | mpancom 687 |
. . 3
โข (๐ โ โ โ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โ โ) |
11 | 7 | nn0ge0d 12535 |
. . . 4
โข (๐ โ โ โ 0 โค
(โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต})) |
12 | | nnre 12219 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ) |
13 | | nngt0 12243 |
. . . 4
โข (๐ โ โ โ 0 <
๐) |
14 | | divge0 12083 |
. . . 4
โข
((((โฏโ{๐
โ (1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) โ โ โง 0 โค
(โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต})) โง (๐ โ โ โง 0 < ๐)) โ 0 โค
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐)) |
15 | 8, 11, 12, 13, 14 | syl22anc 838 |
. . 3
โข (๐ โ โ โ 0 โค
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐)) |
16 | | ssdomg 8996 |
. . . . . . . 8
โข
((1...๐) โ Fin
โ ({๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต} โ (1...๐) โ {๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โผ (1...๐))) |
17 | 2, 3, 16 | mpisyl 21 |
. . . . . . 7
โข (๐ โ โ โ {๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โผ (1...๐)) |
18 | | hashdom 14339 |
. . . . . . . 8
โข (({๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โ Fin โง (1...๐) โ Fin) โ ((โฏโ{๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต}) โค (โฏโ(1...๐)) โ {๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โผ (1...๐))) |
19 | 5, 2, 18 | syl2anc 585 |
. . . . . . 7
โข (๐ โ โ โ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) โค (โฏโ(1...๐)) โ {๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต} โผ (1...๐))) |
20 | 17, 19 | mpbird 257 |
. . . . . 6
โข (๐ โ โ โ
(โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) โค (โฏโ(1...๐))) |
21 | | nnnn0 12479 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ0) |
22 | | hashfz1 14306 |
. . . . . . 7
โข (๐ โ โ0
โ (โฏโ(1...๐)) = ๐) |
23 | 21, 22 | syl 17 |
. . . . . 6
โข (๐ โ โ โ
(โฏโ(1...๐)) =
๐) |
24 | 20, 23 | breqtrd 5175 |
. . . . 5
โข (๐ โ โ โ
(โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) โค ๐) |
25 | | nncn 12220 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
26 | 25 | mulridd 11231 |
. . . . 5
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
27 | 24, 26 | breqtrrd 5177 |
. . . 4
โข (๐ โ โ โ
(โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) โค (๐ ยท 1)) |
28 | | 1red 11215 |
. . . . 5
โข (๐ โ โ โ 1 โ
โ) |
29 | | ledivmul 12090 |
. . . . 5
โข
(((โฏโ{๐
โ (1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) โ โ โง 1 โ โ
โง (๐ โ โ
โง 0 < ๐)) โ
(((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โค 1 โ (โฏโ{๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต}) โค (๐ ยท 1))) |
30 | 8, 28, 12, 13, 29 | syl112anc 1375 |
. . . 4
โข (๐ โ โ โ
(((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โค 1 โ (โฏโ{๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต}) โค (๐ ยท 1))) |
31 | 27, 30 | mpbird 257 |
. . 3
โข (๐ โ โ โ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โค 1) |
32 | | elicc01 13443 |
. . 3
โข
(((โฏโ{๐
โ (1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โ (0[,]1) โ
(((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โ โ โง 0 โค
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โง ((โฏโ{๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โค 1)) |
33 | 10, 15, 31, 32 | syl3anbrc 1344 |
. 2
โข (๐ โ โ โ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐ต}) / ๐) โ (0[,]1)) |
34 | 1, 33 | fmpti 7112 |
1
โข ๐น:โโถ(0[,]1) |