Step | Hyp | Ref
| Expression |
1 | | oveq1 7357 |
. . . . . . . . 9
โข (๐ = ๐
โ (๐ โ 1) = (๐
โ 1)) |
2 | 1 | oveq2d 7366 |
. . . . . . . 8
โข (๐ = ๐
โ (0...(๐ โ 1)) = (0...(๐
โ 1))) |
3 | | oveq1 7357 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐
โ (๐โ๐) = (๐
โ๐)) |
4 | 3 | oveq2d 7366 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐
โ (๐ฅ ยท (๐โ๐)) = (๐ฅ ยท (๐
โ๐))) |
5 | | id 22 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐
โ ๐ = ๐
) |
6 | 4, 5 | oveq12d 7368 |
. . . . . . . . . . . . . 14
โข (๐ = ๐
โ ((๐ฅ ยท (๐โ๐)) mod ๐) = ((๐ฅ ยท (๐
โ๐)) mod ๐
)) |
7 | 6 | fveqeq2d 6846 |
. . . . . . . . . . . . 13
โข (๐ = ๐
โ ((โโ((๐ฅ ยท (๐โ๐)) mod ๐)) = ๐ โ (โโ((๐ฅ ยท (๐
โ๐)) mod ๐
)) = ๐)) |
8 | 7 | rabbidv 3414 |
. . . . . . . . . . . 12
โข (๐ = ๐
โ {๐ โ (1...๐) โฃ (โโ((๐ฅ ยท (๐โ๐)) mod ๐)) = ๐} = {๐ โ (1...๐) โฃ (โโ((๐ฅ ยท (๐
โ๐)) mod ๐
)) = ๐}) |
9 | 8 | fveq2d 6842 |
. . . . . . . . . . 11
โข (๐ = ๐
โ (โฏโ{๐ โ (1...๐) โฃ (โโ((๐ฅ ยท (๐โ๐)) mod ๐)) = ๐}) = (โฏโ{๐ โ (1...๐) โฃ (โโ((๐ฅ ยท (๐
โ๐)) mod ๐
)) = ๐})) |
10 | 9 | oveq1d 7365 |
. . . . . . . . . 10
โข (๐ = ๐
โ ((โฏโ{๐ โ (1...๐) โฃ (โโ((๐ฅ ยท (๐โ๐)) mod ๐)) = ๐}) / ๐) = ((โฏโ{๐ โ (1...๐) โฃ (โโ((๐ฅ ยท (๐
โ๐)) mod ๐
)) = ๐}) / ๐)) |
11 | 10 | mpteq2dv 5206 |
. . . . . . . . 9
โข (๐ = ๐
โ (๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐โ๐)) mod ๐)) = ๐}) / ๐)) = (๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐))) |
12 | | oveq2 7358 |
. . . . . . . . 9
โข (๐ = ๐
โ (1 / ๐) = (1 / ๐
)) |
13 | 11, 12 | breq12d 5117 |
. . . . . . . 8
โข (๐ = ๐
โ ((๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐โ๐)) mod ๐)) = ๐}) / ๐)) โ (1 / ๐) โ (๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
))) |
14 | 2, 13 | raleqbidv 3318 |
. . . . . . 7
โข (๐ = ๐
โ (โ๐ โ (0...(๐ โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐โ๐)) mod ๐)) = ๐}) / ๐)) โ (1 / ๐) โ โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
))) |
15 | 14 | rabbidv 3414 |
. . . . . 6
โข (๐ = ๐
โ {๐ฅ โ โ โฃ โ๐ โ (0...(๐ โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐โ๐)) mod ๐)) = ๐}) / ๐)) โ (1 / ๐)} = {๐ฅ โ โ โฃ โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
)}) |
16 | | snml.s |
. . . . . 6
โข ๐ = (๐ โ (โคโฅโ2)
โฆ {๐ฅ โ โ
โฃ โ๐ โ
(0...(๐ โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐โ๐)) mod ๐)) = ๐}) / ๐)) โ (1 / ๐)}) |
17 | | reex 11076 |
. . . . . . 7
โข โ
โ V |
18 | 17 | rabex 5288 |
. . . . . 6
โข {๐ฅ โ โ โฃ
โ๐ โ
(0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
)} โ V |
19 | 15, 16, 18 | fvmpt 6944 |
. . . . 5
โข (๐
โ
(โคโฅโ2) โ (๐โ๐
) = {๐ฅ โ โ โฃ โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
)}) |
20 | 19 | eleq2d 2824 |
. . . 4
โข (๐
โ
(โคโฅโ2) โ (๐ด โ (๐โ๐
) โ ๐ด โ {๐ฅ โ โ โฃ โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
)})) |
21 | | oveq1 7357 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ด โ (๐ฅ ยท (๐
โ๐)) = (๐ด ยท (๐
โ๐))) |
22 | 21 | fvoveq1d 7372 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ด โ (โโ((๐ฅ ยท (๐
โ๐)) mod ๐
)) = (โโ((๐ด ยท (๐
โ๐)) mod ๐
))) |
23 | 22 | eqeq1d 2740 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ด โ ((โโ((๐ฅ ยท (๐
โ๐)) mod ๐
)) = ๐ โ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐)) |
24 | 23 | rabbidv 3414 |
. . . . . . . . . 10
โข (๐ฅ = ๐ด โ {๐ โ (1...๐) โฃ (โโ((๐ฅ ยท (๐
โ๐)) mod ๐
)) = ๐} = {๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐}) |
25 | 24 | fveq2d 6842 |
. . . . . . . . 9
โข (๐ฅ = ๐ด โ (โฏโ{๐ โ (1...๐) โฃ (โโ((๐ฅ ยท (๐
โ๐)) mod ๐
)) = ๐}) = (โฏโ{๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐})) |
26 | 25 | oveq1d 7365 |
. . . . . . . 8
โข (๐ฅ = ๐ด โ ((โฏโ{๐ โ (1...๐) โฃ (โโ((๐ฅ ยท (๐
โ๐)) mod ๐
)) = ๐}) / ๐) = ((โฏโ{๐ โ (1...๐) โฃ (โโ((๐ด ยท (๐
โ๐)) mod ๐
)) = ๐}) / ๐)) |
27 | 26 | mpteq2dv 5206 |
. . . . . . 7
โข (๐ฅ = ๐ด โ (๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) = (๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐))) |
28 | 27 | breq1d 5114 |
. . . . . 6
โข (๐ฅ = ๐ด โ ((๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
) โ (๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
))) |
29 | 28 | ralbidv 3173 |
. . . . 5
โข (๐ฅ = ๐ด โ (โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
) โ โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
))) |
30 | 29 | elrab 3644 |
. . . 4
โข (๐ด โ {๐ฅ โ โ โฃ โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ฅ ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
)} โ (๐ด โ โ โง โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
))) |
31 | 20, 30 | bitrdi 287 |
. . 3
โข (๐
โ
(โคโฅโ2) โ (๐ด โ (๐โ๐
) โ (๐ด โ โ โง โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
)))) |
32 | 31 | pm5.32i 576 |
. 2
โข ((๐
โ
(โคโฅโ2) โง ๐ด โ (๐โ๐
)) โ (๐
โ (โคโฅโ2)
โง (๐ด โ โ
โง โ๐ โ
(0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
)))) |
33 | 16 | dmmptss 6190 |
. . . 4
โข dom ๐ โ
(โคโฅโ2) |
34 | | elfvdm 6875 |
. . . 4
โข (๐ด โ (๐โ๐
) โ ๐
โ dom ๐) |
35 | 33, 34 | sselid 3941 |
. . 3
โข (๐ด โ (๐โ๐
) โ ๐
โ
(โคโฅโ2)) |
36 | 35 | pm4.71ri 562 |
. 2
โข (๐ด โ (๐โ๐
) โ (๐
โ (โคโฅโ2)
โง ๐ด โ (๐โ๐
))) |
37 | | 3anass 1096 |
. 2
โข ((๐
โ
(โคโฅโ2) โง ๐ด โ โ โง โ๐ โ (0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
)) โ (๐
โ (โคโฅโ2)
โง (๐ด โ โ
โง โ๐ โ
(0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
)))) |
38 | 32, 36, 37 | 3bitr4i 303 |
1
โข (๐ด โ (๐โ๐
) โ (๐
โ (โคโฅโ2)
โง ๐ด โ โ
โง โ๐ โ
(0...(๐
โ 1))(๐ โ โ โฆ
((โฏโ{๐ โ
(1...๐) โฃ
(โโ((๐ด ยท
(๐
โ๐)) mod ๐
)) = ๐}) / ๐)) โ (1 / ๐
))) |