Step | Hyp | Ref
| Expression |
1 | | prmnn 12110 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
2 | 1 | adantr 276 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ โ) |
3 | | fzo0sn0fzo1 10221 |
. . . . 5
โข (๐ โ โ โ
(0..^๐) = ({0} โช
(1..^๐))) |
4 | 2, 3 | syl 14 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (0..^๐) = ({0} โช (1..^๐))) |
5 | 4 | eleq2d 2247 |
. . 3
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (๐ผ โ (0..^๐) โ ๐ผ โ ({0} โช (1..^๐)))) |
6 | | elun 3277 |
. . . . 5
โข (๐ผ โ ({0} โช (1..^๐)) โ (๐ผ โ {0} โจ ๐ผ โ (1..^๐))) |
7 | | elsni 3611 |
. . . . . . 7
โข (๐ผ โ {0} โ ๐ผ = 0) |
8 | | lbfzo0 10181 |
. . . . . . . . . . . 12
โข (0 โ
(0..^๐) โ ๐ โ
โ) |
9 | 1, 8 | sylibr 134 |
. . . . . . . . . . 11
โข (๐ โ โ โ 0 โ
(0..^๐)) |
10 | | elfzoelz 10147 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1..^๐) โ ๐ โ โค) |
11 | | zcn 9258 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ ๐ โ
โ) |
12 | | mul02 8344 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (0
ยท ๐) =
0) |
13 | 12 | oveq2d 5891 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (0 + (0
ยท ๐)) = (0 +
0)) |
14 | | 00id 8098 |
. . . . . . . . . . . . . . . 16
โข (0 + 0) =
0 |
15 | 13, 14 | eqtrdi 2226 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (0 + (0
ยท ๐)) =
0) |
16 | 10, 11, 15 | 3syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (1..^๐) โ (0 + (0 ยท ๐)) = 0) |
17 | 16 | adantl 277 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (0 + (0 ยท ๐)) = 0) |
18 | 17 | oveq1d 5890 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ((0 + (0 ยท ๐)) mod ๐) = (0 mod ๐)) |
19 | | nnq 9633 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
20 | 1, 19 | syl 14 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
21 | 1 | nngt0d 8963 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 0 <
๐) |
22 | | q0mod 10355 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง 0 <
๐) โ (0 mod ๐) = 0) |
23 | 20, 21, 22 | syl2anc 411 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (0 mod
๐) = 0) |
24 | 23 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (0 mod ๐) = 0) |
25 | 18, 24 | eqtrd 2210 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ((0 + (0 ยท ๐)) mod ๐) = 0) |
26 | | oveq1 5882 |
. . . . . . . . . . . . . . 15
โข (๐ = 0 โ (๐ ยท ๐) = (0 ยท ๐)) |
27 | 26 | oveq2d 5891 |
. . . . . . . . . . . . . 14
โข (๐ = 0 โ (0 + (๐ ยท ๐)) = (0 + (0 ยท ๐))) |
28 | 27 | oveq1d 5890 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ ((0 + (๐ ยท ๐)) mod ๐) = ((0 + (0 ยท ๐)) mod ๐)) |
29 | 28 | eqeq1d 2186 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (((0 + (๐ ยท ๐)) mod ๐) = 0 โ ((0 + (0 ยท ๐)) mod ๐) = 0)) |
30 | 29 | rspcev 2842 |
. . . . . . . . . . 11
โข ((0
โ (0..^๐) โง ((0 +
(0 ยท ๐)) mod ๐) = 0) โ โ๐ โ (0..^๐)((0 + (๐ ยท ๐)) mod ๐) = 0) |
31 | 9, 25, 30 | syl2an2r 595 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((0 + (๐ ยท ๐)) mod ๐) = 0) |
32 | 31 | adantl 277 |
. . . . . . . . 9
โข ((๐ผ = 0 โง (๐ โ โ โง ๐ โ (1..^๐))) โ โ๐ โ (0..^๐)((0 + (๐ ยท ๐)) mod ๐) = 0) |
33 | | oveq1 5882 |
. . . . . . . . . . . . 13
โข (๐ผ = 0 โ (๐ผ + (๐ ยท ๐)) = (0 + (๐ ยท ๐))) |
34 | 33 | oveq1d 5890 |
. . . . . . . . . . . 12
โข (๐ผ = 0 โ ((๐ผ + (๐ ยท ๐)) mod ๐) = ((0 + (๐ ยท ๐)) mod ๐)) |
35 | 34 | eqeq1d 2186 |
. . . . . . . . . . 11
โข (๐ผ = 0 โ (((๐ผ + (๐ ยท ๐)) mod ๐) = 0 โ ((0 + (๐ ยท ๐)) mod ๐) = 0)) |
36 | 35 | adantr 276 |
. . . . . . . . . 10
โข ((๐ผ = 0 โง (๐ โ โ โง ๐ โ (1..^๐))) โ (((๐ผ + (๐ ยท ๐)) mod ๐) = 0 โ ((0 + (๐ ยท ๐)) mod ๐) = 0)) |
37 | 36 | rexbidv 2478 |
. . . . . . . . 9
โข ((๐ผ = 0 โง (๐ โ โ โง ๐ โ (1..^๐))) โ (โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0 โ โ๐ โ (0..^๐)((0 + (๐ ยท ๐)) mod ๐) = 0)) |
38 | 32, 37 | mpbird 167 |
. . . . . . . 8
โข ((๐ผ = 0 โง (๐ โ โ โง ๐ โ (1..^๐))) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |
39 | 38 | ex 115 |
. . . . . . 7
โข (๐ผ = 0 โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
40 | 7, 39 | syl 14 |
. . . . . 6
โข (๐ผ โ {0} โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
41 | | simpl 109 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ โ) |
42 | 41 | adantl 277 |
. . . . . . . 8
โข ((๐ผ โ (1..^๐) โง (๐ โ โ โง ๐ โ (1..^๐))) โ ๐ โ โ) |
43 | | simprr 531 |
. . . . . . . 8
โข ((๐ผ โ (1..^๐) โง (๐ โ โ โง ๐ โ (1..^๐))) โ ๐ โ (1..^๐)) |
44 | | simpl 109 |
. . . . . . . 8
โข ((๐ผ โ (1..^๐) โง (๐ โ โ โง ๐ โ (1..^๐))) โ ๐ผ โ (1..^๐)) |
45 | | modprm0 12254 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |
46 | 42, 43, 44, 45 | syl3anc 1238 |
. . . . . . 7
โข ((๐ผ โ (1..^๐) โง (๐ โ โ โง ๐ โ (1..^๐))) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |
47 | 46 | ex 115 |
. . . . . 6
โข (๐ผ โ (1..^๐) โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
48 | 40, 47 | jaoi 716 |
. . . . 5
โข ((๐ผ โ {0} โจ ๐ผ โ (1..^๐)) โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
49 | 6, 48 | sylbi 121 |
. . . 4
โข (๐ผ โ ({0} โช (1..^๐)) โ ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
50 | 49 | com12 30 |
. . 3
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (๐ผ โ ({0} โช (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
51 | 5, 50 | sylbid 150 |
. 2
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (๐ผ โ (0..^๐) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
52 | 51 | 3impia 1200 |
1
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (0..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |