Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ
(โฏโ๐) โ
โ) |
2 | 1 | adantr 482 |
. . . . . . . 8
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โ (โฏโ๐) โ โ) |
3 | | simp1 1137 |
. . . . . . . . 9
โข ((๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐) โ ๐ฟ โ โค) |
4 | 3 | adantl 483 |
. . . . . . . 8
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โ ๐ฟ โ โค) |
5 | | simpr2 1196 |
. . . . . . . 8
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โ (๐ฟ mod (โฏโ๐)) โ 0) |
6 | 2, 4, 5 | 3jca 1129 |
. . . . . . 7
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โ ((โฏโ๐) โ โ โง ๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0)) |
7 | 6 | adantr 482 |
. . . . . 6
โข ((((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐))) โ ((โฏโ๐) โ โ โง ๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0)) |
8 | | simpr 486 |
. . . . . 6
โข ((((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐))) โ ๐ โ (0..^(โฏโ๐))) |
9 | | modprmn0modprm0 16687 |
. . . . . 6
โข
(((โฏโ๐)
โ โ โง ๐ฟ
โ โค โง (๐ฟ mod
(โฏโ๐)) โ 0)
โ (๐ โ
(0..^(โฏโ๐))
โ โ๐ โ
(0..^(โฏโ๐))((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0)) |
10 | 7, 8, 9 | sylc 65 |
. . . . 5
โข ((((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐))) โ โ๐ โ (0..^(โฏโ๐))((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) |
11 | | oveq1 7368 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ ยท ๐ฟ) = (๐ ยท ๐ฟ)) |
12 | 11 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ + (๐ ยท ๐ฟ)) = (๐ + (๐ ยท ๐ฟ))) |
13 | 12 | fvoveq1d 7383 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)))) |
14 | 13 | eqeq2d 2744 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐โ๐) = (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐))) โ (๐โ๐) = (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐))))) |
15 | | simpl 484 |
. . . . . . . . . . . . 13
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ ๐ โ Word ๐) |
16 | 15, 3 | anim12i 614 |
. . . . . . . . . . . 12
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โ (๐ โ Word ๐ โง ๐ฟ โ โค)) |
17 | 16 | adantr 482 |
. . . . . . . . . . 11
โข ((((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐))) โ (๐ โ Word ๐ โง ๐ฟ โ โค)) |
18 | 17 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โ
(0..^(โฏโ๐))
โง ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) โง (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐)))) โ (๐ โ Word ๐ โง ๐ฟ โ โค)) |
19 | | simpr3 1197 |
. . . . . . . . . . . 12
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โ (๐ cyclShift ๐ฟ) = ๐) |
20 | 19 | anim1i 616 |
. . . . . . . . . . 11
โข ((((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐))) โ ((๐ cyclShift ๐ฟ) = ๐ โง ๐ โ (0..^(โฏโ๐)))) |
21 | 20 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โ
(0..^(โฏโ๐))
โง ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) โง (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐)))) โ ((๐ cyclShift ๐ฟ) = ๐ โง ๐ โ (0..^(โฏโ๐)))) |
22 | | cshweqrep 14718 |
. . . . . . . . . 10
โข ((๐ โ Word ๐ โง ๐ฟ โ โค) โ (((๐ cyclShift ๐ฟ) = ๐ โง ๐ โ (0..^(โฏโ๐))) โ โ๐ โ โ0 (๐โ๐) = (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐))))) |
23 | 18, 21, 22 | sylc 65 |
. . . . . . . . 9
โข (((๐ โ
(0..^(โฏโ๐))
โง ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) โง (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐)))) โ โ๐ โ โ0 (๐โ๐) = (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)))) |
24 | | elfzonn0 13626 |
. . . . . . . . . 10
โข (๐ โ
(0..^(โฏโ๐))
โ ๐ โ
โ0) |
25 | 24 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โ
(0..^(โฏโ๐))
โง ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) โง (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐)))) โ ๐ โ โ0) |
26 | 14, 23, 25 | rspcdva 3584 |
. . . . . . . 8
โข (((๐ โ
(0..^(โฏโ๐))
โง ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) โง (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐)))) โ (๐โ๐) = (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)))) |
27 | | fveq2 6846 |
. . . . . . . . . 10
โข (((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0 โ (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ0)) |
28 | 27 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ
(0..^(โฏโ๐))
โง ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) โ (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ0)) |
29 | 28 | adantr 482 |
. . . . . . . 8
โข (((๐ โ
(0..^(โฏโ๐))
โง ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) โง (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐)))) โ (๐โ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ0)) |
30 | 26, 29 | eqtrd 2773 |
. . . . . . 7
โข (((๐ โ
(0..^(โฏโ๐))
โง ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) โง (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐)))) โ (๐โ๐) = (๐โ0)) |
31 | 30 | ex 414 |
. . . . . 6
โข ((๐ โ
(0..^(โฏโ๐))
โง ((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0) โ ((((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐))) โ (๐โ๐) = (๐โ0))) |
32 | 31 | rexlimiva 3141 |
. . . . 5
โข
(โ๐ โ
(0..^(โฏโ๐))((๐ + (๐ ยท ๐ฟ)) mod (โฏโ๐)) = 0 โ ((((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐))) โ (๐โ๐) = (๐โ0))) |
33 | 10, 32 | mpcom 38 |
. . . 4
โข ((((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โง ๐ โ (0..^(โฏโ๐))) โ (๐โ๐) = (๐โ0)) |
34 | 33 | ralrimiva 3140 |
. . 3
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โ โ๐ โ (0..^(โฏโ๐))(๐โ๐) = (๐โ0)) |
35 | | repswsymballbi 14677 |
. . . 4
โข (๐ โ Word ๐ โ (๐ = ((๐โ0) repeatS (โฏโ๐)) โ โ๐ โ
(0..^(โฏโ๐))(๐โ๐) = (๐โ0))) |
36 | 35 | ad2antrr 725 |
. . 3
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โ (๐ = ((๐โ0) repeatS (โฏโ๐)) โ โ๐ โ
(0..^(โฏโ๐))(๐โ๐) = (๐โ0))) |
37 | 34, 36 | mpbird 257 |
. 2
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง (๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐)) โ ๐ = ((๐โ0) repeatS (โฏโ๐))) |
38 | 37 | ex 414 |
1
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ ((๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐) โ ๐ = ((๐โ0) repeatS (โฏโ๐)))) |