Step | Hyp | Ref
| Expression |
1 | | prmnn 16613 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
2 | 1 | adantr 481 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ โ) |
3 | | fzo0sn0fzo1 13723 |
. . . . 5
โข (๐ โ โ โ
(0..^๐) = ({0} โช
(1..^๐))) |
4 | 2, 3 | syl 17 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (0..^๐) = ({0} โช (1..^๐))) |
5 | 4 | eleq2d 2819 |
. . 3
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (๐ผ โ (0..^๐) โ ๐ผ โ ({0} โช (1..^๐)))) |
6 | | elun 4148 |
. . . . 5
โข (๐ผ โ ({0} โช (1..^๐)) โ (๐ผ โ {0} โจ ๐ผ โ (1..^๐))) |
7 | | elsni 4645 |
. . . . . . 7
โข (๐ผ โ {0} โ ๐ผ = 0) |
8 | | lbfzo0 13674 |
. . . . . . . . . . . 12
โข (0 โ
(0..^๐) โ ๐ โ
โ) |
9 | 1, 8 | sylibr 233 |
. . . . . . . . . . 11
โข (๐ โ โ โ 0 โ
(0..^๐)) |
10 | | elfzoelz 13634 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1..^๐) โ ๐ โ โค) |
11 | | zcn 12565 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ ๐ โ
โ) |
12 | | mul02 11394 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (0
ยท ๐) =
0) |
13 | 12 | oveq2d 7427 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (0 + (0
ยท ๐)) = (0 +
0)) |
14 | | 00id 11391 |
. . . . . . . . . . . . . . . 16
โข (0 + 0) =
0 |
15 | 13, 14 | eqtrdi 2788 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (0 + (0
ยท ๐)) =
0) |
16 | 10, 11, 15 | 3syl 18 |
. . . . . . . . . . . . . 14
โข (๐ โ (1..^๐) โ (0 + (0 ยท ๐)) = 0) |
17 | 16 | adantl 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (0 + (0 ยท ๐)) = 0) |
18 | 17 | oveq1d 7426 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ((0 + (0 ยท ๐)) mod ๐) = (0 mod ๐)) |
19 | | nnrp 12987 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ+) |
20 | | 0mod 13869 |
. . . . . . . . . . . . . 14
โข (๐ โ โ+
โ (0 mod ๐) =
0) |
21 | 1, 19, 20 | 3syl 18 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (0 mod
๐) = 0) |
22 | 21 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (0 mod ๐) = 0) |
23 | 18, 22 | eqtrd 2772 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ((0 + (0 ยท ๐)) mod ๐) = 0) |
24 | | oveq1 7418 |
. . . . . . . . . . . . . . 15
โข (๐ = 0 โ (๐ ยท ๐) = (0 ยท ๐)) |
25 | 24 | oveq2d 7427 |
. . . . . . . . . . . . . 14
โข (๐ = 0 โ (0 + (๐ ยท ๐)) = (0 + (0 ยท ๐))) |
26 | 25 | oveq1d 7426 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ ((0 + (๐ ยท ๐)) mod ๐) = ((0 + (0 ยท ๐)) mod ๐)) |
27 | 26 | eqeq1d 2734 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (((0 + (๐ ยท ๐)) mod ๐) = 0 โ ((0 + (0 ยท ๐)) mod ๐) = 0)) |
28 | 27 | rspcev 3612 |
. . . . . . . . . . 11
โข ((0
โ (0..^๐) โง ((0 +
(0 ยท ๐)) mod ๐) = 0) โ โ๐ โ (0..^๐)((0 + (๐ ยท ๐)) mod ๐) = 0) |
29 | 9, 23, 28 | syl2an2r 683 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((0 + (๐ ยท ๐)) mod ๐) = 0) |
30 | 29 | adantl 482 |
. . . . . . . . 9
โข ((๐ผ = 0 โง (๐ โ โ โง ๐ โ (1..^๐))) โ โ๐ โ (0..^๐)((0 + (๐ ยท ๐)) mod ๐) = 0) |
31 | | oveq1 7418 |
. . . . . . . . . . . . 13
โข (๐ผ = 0 โ (๐ผ + (๐ ยท ๐)) = (0 + (๐ ยท ๐))) |
32 | 31 | oveq1d 7426 |
. . . . . . . . . . . 12
โข (๐ผ = 0 โ ((๐ผ + (๐ ยท ๐)) mod ๐) = ((0 + (๐ ยท ๐)) mod ๐)) |
33 | 32 | eqeq1d 2734 |
. . . . . . . . . . 11
โข (๐ผ = 0 โ (((๐ผ + (๐ ยท ๐)) mod ๐) = 0 โ ((0 + (๐ ยท ๐)) mod ๐) = 0)) |
34 | 33 | adantr 481 |
. . . . . . . . . 10
โข ((๐ผ = 0 โง (๐ โ โ โง ๐ โ (1..^๐))) โ (((๐ผ + (๐ ยท ๐)) mod ๐) = 0 โ ((0 + (๐ ยท ๐)) mod ๐) = 0)) |
35 | 34 | rexbidv 3178 |
. . . . . . . . 9
โข ((๐ผ = 0 โง (๐ โ โ โง ๐ โ (1..^๐))) โ (โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0 โ โ๐ โ (0..^๐)((0 + (๐ ยท ๐)) mod ๐) = 0)) |
36 | 30, 35 | mpbird 256 |
. . . . . . . 8
โข ((๐ผ = 0 โง (๐ โ โ โง ๐ โ (1..^๐))) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |
37 | 36 | ex 413 |
. . . . . . 7
โข (๐ผ = 0 โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
38 | 7, 37 | syl 17 |
. . . . . 6
โข (๐ผ โ {0} โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
39 | | simpl 483 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ โ) |
40 | 39 | adantl 482 |
. . . . . . . 8
โข ((๐ผ โ (1..^๐) โง (๐ โ โ โง ๐ โ (1..^๐))) โ ๐ โ โ) |
41 | | simprr 771 |
. . . . . . . 8
โข ((๐ผ โ (1..^๐) โง (๐ โ โ โง ๐ โ (1..^๐))) โ ๐ โ (1..^๐)) |
42 | | simpl 483 |
. . . . . . . 8
โข ((๐ผ โ (1..^๐) โง (๐ โ โ โง ๐ โ (1..^๐))) โ ๐ผ โ (1..^๐)) |
43 | | modprm0 16740 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |
44 | 40, 41, 42, 43 | syl3anc 1371 |
. . . . . . 7
โข ((๐ผ โ (1..^๐) โง (๐ โ โ โง ๐ โ (1..^๐))) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |
45 | 44 | ex 413 |
. . . . . 6
โข (๐ผ โ (1..^๐) โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
46 | 38, 45 | jaoi 855 |
. . . . 5
โข ((๐ผ โ {0} โจ ๐ผ โ (1..^๐)) โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
47 | 6, 46 | sylbi 216 |
. . . 4
โข (๐ผ โ ({0} โช (1..^๐)) โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
48 | 47 | com12 32 |
. . 3
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (๐ผ โ ({0} โช (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
49 | 5, 48 | sylbid 239 |
. 2
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (๐ผ โ (0..^๐) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
50 | 49 | 3impia 1117 |
1
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (0..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |