Step | Hyp | Ref
| Expression |
1 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ฅ = 0 โ (๐ฅ ยท ๐ฟ) = (0 ยท ๐ฟ)) |
2 | 1 | oveq2d 7378 |
. . . . . . . 8
โข (๐ฅ = 0 โ (๐ผ + (๐ฅ ยท ๐ฟ)) = (๐ผ + (0 ยท ๐ฟ))) |
3 | 2 | fvoveq1d 7384 |
. . . . . . 7
โข (๐ฅ = 0 โ (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ((๐ผ + (0 ยท ๐ฟ)) mod (โฏโ๐)))) |
4 | 3 | eqeq2d 2748 |
. . . . . 6
โข (๐ฅ = 0 โ ((๐โ๐ผ) = (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐))) โ (๐โ๐ผ) = (๐โ((๐ผ + (0 ยท ๐ฟ)) mod (โฏโ๐))))) |
5 | 4 | imbi2d 341 |
. . . . 5
โข (๐ฅ = 0 โ ((((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐)))) โ (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (0 ยท ๐ฟ)) mod (โฏโ๐)))))) |
6 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (๐ฅ ยท ๐ฟ) = (๐ฆ ยท ๐ฟ)) |
7 | 6 | oveq2d 7378 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ (๐ผ + (๐ฅ ยท ๐ฟ)) = (๐ผ + (๐ฆ ยท ๐ฟ))) |
8 | 7 | fvoveq1d 7384 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)))) |
9 | 8 | eqeq2d 2748 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ((๐โ๐ผ) = (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))))) |
10 | 9 | imbi2d 341 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐)))) โ (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)))))) |
11 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ฅ = (๐ฆ + 1) โ (๐ฅ ยท ๐ฟ) = ((๐ฆ + 1) ยท ๐ฟ)) |
12 | 11 | oveq2d 7378 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ + 1) โ (๐ผ + (๐ฅ ยท ๐ฟ)) = (๐ผ + ((๐ฆ + 1) ยท ๐ฟ))) |
13 | 12 | fvoveq1d 7384 |
. . . . . . 7
โข (๐ฅ = (๐ฆ + 1) โ (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))) |
14 | 13 | eqeq2d 2748 |
. . . . . 6
โข (๐ฅ = (๐ฆ + 1) โ ((๐โ๐ผ) = (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐))) โ (๐โ๐ผ) = (๐โ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
15 | 14 | imbi2d 341 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ ((((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐)))) โ (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))))) |
16 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (๐ฅ ยท ๐ฟ) = (๐ ยท ๐ฟ)) |
17 | 16 | oveq2d 7378 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ผ + (๐ฅ ยท ๐ฟ)) = (๐ผ + (๐ ยท ๐ฟ))) |
18 | 17 | fvoveq1d 7384 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ((๐ผ + (๐ ยท ๐ฟ)) mod (โฏโ๐)))) |
19 | 18 | eqeq2d 2748 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐โ๐ผ) = (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ ยท ๐ฟ)) mod (โฏโ๐))))) |
20 | 19 | imbi2d 341 |
. . . . 5
โข (๐ฅ = ๐ โ ((((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ฅ ยท ๐ฟ)) mod (โฏโ๐)))) โ (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ ยท ๐ฟ)) mod (โฏโ๐)))))) |
21 | | zcn 12511 |
. . . . . . . . . . . . 13
โข (๐ฟ โ โค โ ๐ฟ โ
โ) |
22 | 21 | mul02d 11360 |
. . . . . . . . . . . 12
โข (๐ฟ โ โค โ (0
ยท ๐ฟ) =
0) |
23 | 22 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ Word ๐ โง ๐ฟ โ โค) โ (0 ยท ๐ฟ) = 0) |
24 | 23 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (0 ยท ๐ฟ) = 0) |
25 | 24 | oveq2d 7378 |
. . . . . . . . 9
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐ผ + (0 ยท ๐ฟ)) = (๐ผ + 0)) |
26 | | elfzoelz 13579 |
. . . . . . . . . . . 12
โข (๐ผ โ
(0..^(โฏโ๐))
โ ๐ผ โ
โค) |
27 | 26 | zcnd 12615 |
. . . . . . . . . . 11
โข (๐ผ โ
(0..^(โฏโ๐))
โ ๐ผ โ
โ) |
28 | 27 | addid1d 11362 |
. . . . . . . . . 10
โข (๐ผ โ
(0..^(โฏโ๐))
โ (๐ผ + 0) = ๐ผ) |
29 | 28 | ad2antll 728 |
. . . . . . . . 9
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐ผ + 0) = ๐ผ) |
30 | 25, 29 | eqtrd 2777 |
. . . . . . . 8
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐ผ + (0 ยท ๐ฟ)) = ๐ผ) |
31 | 30 | oveq1d 7377 |
. . . . . . 7
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ ((๐ผ + (0 ยท ๐ฟ)) mod (โฏโ๐)) = (๐ผ mod (โฏโ๐))) |
32 | | zmodidfzoimp 13813 |
. . . . . . . 8
โข (๐ผ โ
(0..^(โฏโ๐))
โ (๐ผ mod
(โฏโ๐)) = ๐ผ) |
33 | 32 | ad2antll 728 |
. . . . . . 7
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐ผ mod (โฏโ๐)) = ๐ผ) |
34 | 31, 33 | eqtr2d 2778 |
. . . . . 6
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ ๐ผ = ((๐ผ + (0 ยท ๐ฟ)) mod (โฏโ๐))) |
35 | 34 | fveq2d 6851 |
. . . . 5
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (0 ยท ๐ฟ)) mod (โฏโ๐)))) |
36 | | fveq1 6846 |
. . . . . . . . . . . . 13
โข (๐ = (๐ cyclShift ๐ฟ) โ (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) = ((๐ cyclShift ๐ฟ)โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)))) |
37 | 36 | eqcoms 2745 |
. . . . . . . . . . . 12
โข ((๐ cyclShift ๐ฟ) = ๐ โ (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) = ((๐ cyclShift ๐ฟ)โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)))) |
38 | 37 | ad2antrl 727 |
. . . . . . . . . . 11
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) = ((๐ cyclShift ๐ฟ)โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)))) |
39 | 38 | adantl 483 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) = ((๐ cyclShift ๐ฟ)โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)))) |
40 | | simprll 778 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ ๐ โ Word ๐) |
41 | | simprlr 779 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ ๐ฟ โ โค) |
42 | | elfzo0 13620 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ผ โ
(0..^(โฏโ๐))
โ (๐ผ โ
โ0 โง (โฏโ๐) โ โ โง ๐ผ < (โฏโ๐))) |
43 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ผ โ โ0
โ ๐ผ โ
โค) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ผ โ โ0
โง (โฏโ๐)
โ โ) โ ๐ผ
โ โค) |
45 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ โ0
โ ๐ฆ โ
โค) |
46 | | zmulcl 12559 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฆ โ โค โง ๐ฟ โ โค) โ (๐ฆ ยท ๐ฟ) โ โค) |
47 | 45, 46 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฆ โ โ0
โง ๐ฟ โ โค)
โ (๐ฆ ยท ๐ฟ) โ
โค) |
48 | 47 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฟ โ โค โง ๐ฆ โ โ0)
โ (๐ฆ ยท ๐ฟ) โ
โค) |
49 | | zaddcl 12550 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ผ โ โค โง (๐ฆ ยท ๐ฟ) โ โค) โ (๐ผ + (๐ฆ ยท ๐ฟ)) โ โค) |
50 | 44, 48, 49 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ผ โ โ0
โง (โฏโ๐)
โ โ) โง (๐ฟ
โ โค โง ๐ฆ
โ โ0)) โ (๐ผ + (๐ฆ ยท ๐ฟ)) โ โค) |
51 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ผ โ โ0
โง (โฏโ๐)
โ โ) โง (๐ฟ
โ โค โง ๐ฆ
โ โ0)) โ (โฏโ๐) โ โ) |
52 | 50, 51 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ผ โ โ0
โง (โฏโ๐)
โ โ) โง (๐ฟ
โ โค โง ๐ฆ
โ โ0)) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ)) |
53 | 52 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ผ โ โ0
โง (โฏโ๐)
โ โ) โ ((๐ฟ
โ โค โง ๐ฆ
โ โ0) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ))) |
54 | 53 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ผ โ โ0
โง (โฏโ๐)
โ โ โง ๐ผ <
(โฏโ๐)) โ
((๐ฟ โ โค โง
๐ฆ โ
โ0) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ))) |
55 | 42, 54 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
โข (๐ผ โ
(0..^(โฏโ๐))
โ ((๐ฟ โ โค
โง ๐ฆ โ
โ0) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ))) |
56 | 55 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข (((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))) โ ((๐ฟ โ โค โง ๐ฆ โ โ0) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ))) |
57 | 56 | expd 417 |
. . . . . . . . . . . . . . . 16
โข (((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))) โ (๐ฟ โ โค โ (๐ฆ โ โ0 โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ)))) |
58 | 57 | com12 32 |
. . . . . . . . . . . . . . 15
โข (๐ฟ โ โค โ (((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))) โ (๐ฆ โ โ0 โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ)))) |
59 | 58 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โ Word ๐ โง ๐ฟ โ โค) โ (((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))) โ (๐ฆ โ โ0 โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ)))) |
60 | 59 | imp 408 |
. . . . . . . . . . . . 13
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐ฆ โ โ0 โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ))) |
61 | 60 | impcom 409 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ
โ)) |
62 | | zmodfzo 13806 |
. . . . . . . . . . . 12
โข (((๐ผ + (๐ฆ ยท ๐ฟ)) โ โค โง (โฏโ๐) โ โ) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) โ (0..^(โฏโ๐))) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) โ (0..^(โฏโ๐))) |
64 | | cshwidxmod 14698 |
. . . . . . . . . . 11
โข ((๐ โ Word ๐ โง ๐ฟ โ โค โง ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) โ (0..^(โฏโ๐))) โ ((๐ cyclShift ๐ฟ)โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)))) |
65 | 40, 41, 63, 64 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ ((๐ cyclShift ๐ฟ)โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)))) |
66 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ผ โ โ0
โ ๐ผ โ
โ) |
67 | | zre 12510 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฟ โ โค โ ๐ฟ โ
โ) |
68 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ โ0
โ ๐ฆ โ
โ) |
69 | | nnrp 12933 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((โฏโ๐)
โ โ โ (โฏโ๐) โ
โ+) |
70 | | remulcl 11143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ฆ โ โ โง ๐ฟ โ โ) โ (๐ฆ ยท ๐ฟ) โ โ) |
71 | 70 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ (๐ฆ ยท ๐ฟ) โ โ) |
72 | | readdcl 11141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ผ โ โ โง (๐ฆ ยท ๐ฟ) โ โ) โ (๐ผ + (๐ฆ ยท ๐ฟ)) โ โ) |
73 | 71, 72 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ผ โ โ โง (๐ฟ โ โ โง ๐ฆ โ โ)) โ (๐ผ + (๐ฆ ยท ๐ฟ)) โ โ) |
74 | 73 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ) โ (๐ผ + (๐ฆ ยท ๐ฟ)) โ โ) |
75 | 74 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((โฏโ๐)
โ โ+ โง ((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ)) โ (๐ผ + (๐ฆ ยท ๐ฟ)) โ โ) |
76 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((โฏโ๐)
โ โ+ โง ((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ)) โ ๐ฟ โ โ) |
77 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((โฏโ๐)
โ โ+ โง ((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ)) โ
(โฏโ๐) โ
โ+) |
78 | | modaddmod 13822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ผ + (๐ฆ ยท ๐ฟ)) โ โ โง ๐ฟ โ โ โง (โฏโ๐) โ โ+)
โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = (((๐ผ + (๐ฆ ยท ๐ฟ)) + ๐ฟ) mod (โฏโ๐))) |
79 | 75, 76, 77, 78 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((โฏโ๐)
โ โ+ โง ((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ)) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = (((๐ผ + (๐ฆ ยท ๐ฟ)) + ๐ฟ) mod (โฏโ๐))) |
80 | | recn 11148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ผ โ โ โ ๐ผ โ
โ) |
81 | 80 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ) โ ๐ผ โ
โ) |
82 | 70 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ฆ โ โ โง ๐ฟ โ โ) โ (๐ฆ ยท ๐ฟ) โ โ) |
83 | 82 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ (๐ฆ ยท ๐ฟ) โ โ) |
84 | 83 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ) โ (๐ฆ ยท ๐ฟ) โ โ) |
85 | | recn 11148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ฟ โ โ โ ๐ฟ โ
โ) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ ๐ฟ โ
โ) |
87 | 86 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ) โ ๐ฟ โ
โ) |
88 | 81, 84, 87 | addassd 11184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) + ๐ฟ) = (๐ผ + ((๐ฆ ยท ๐ฟ) + ๐ฟ))) |
89 | | recn 11148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
90 | 89 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ ๐ฆ โ
โ) |
91 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ 1 โ
โ) |
92 | 90, 91, 86 | adddird 11187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ ((๐ฆ + 1) ยท ๐ฟ) = ((๐ฆ ยท ๐ฟ) + (1 ยท ๐ฟ))) |
93 | 85 | mulid2d 11180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (๐ฟ โ โ โ (1
ยท ๐ฟ) = ๐ฟ) |
94 | 93 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ (1
ยท ๐ฟ) = ๐ฟ) |
95 | 94 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐ฟ) + (1 ยท ๐ฟ)) = ((๐ฆ ยท ๐ฟ) + ๐ฟ)) |
96 | 92, 95 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐ฟ) + ๐ฟ) = ((๐ฆ + 1) ยท ๐ฟ)) |
97 | 96 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ) โ ((๐ฆ ยท ๐ฟ) + ๐ฟ) = ((๐ฆ + 1) ยท ๐ฟ)) |
98 | 97 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ) โ (๐ผ + ((๐ฆ ยท ๐ฟ) + ๐ฟ)) = (๐ผ + ((๐ฆ + 1) ยท ๐ฟ))) |
99 | 88, 98 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) + ๐ฟ) = (๐ผ + ((๐ฆ + 1) ยท ๐ฟ))) |
100 | 99 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((โฏโ๐)
โ โ+ โง ((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ)) โ ((๐ผ + (๐ฆ ยท ๐ฟ)) + ๐ฟ) = (๐ผ + ((๐ฆ + 1) ยท ๐ฟ))) |
101 | 100 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((โฏโ๐)
โ โ+ โง ((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ)) โ (((๐ผ + (๐ฆ ยท ๐ฟ)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))) |
102 | 79, 101 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((โฏโ๐)
โ โ+ โง ((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ)) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))) |
103 | 102 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((โฏโ๐)
โ โ+ โ (((๐ฟ โ โ โง ๐ฆ โ โ) โง ๐ผ โ โ) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))) |
104 | 69, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
((โฏโ๐)
โ โ โ (((๐ฟ
โ โ โง ๐ฆ
โ โ) โง ๐ผ
โ โ) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))) |
105 | 104 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
((โฏโ๐)
โ โ โ ((๐ฟ
โ โ โง ๐ฆ
โ โ) โ (๐ผ
โ โ โ ((((๐ผ
+ (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
106 | 105 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฟ โ โ โง ๐ฆ โ โ) โ
((โฏโ๐) โ
โ โ (๐ผ โ
โ โ ((((๐ผ +
(๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
107 | 67, 68, 106 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฟ โ โค โง ๐ฆ โ โ0)
โ ((โฏโ๐)
โ โ โ (๐ผ
โ โ โ ((((๐ผ
+ (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
108 | 107 | com13 88 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ผ โ โ โ
((โฏโ๐) โ
โ โ ((๐ฟ โ
โค โง ๐ฆ โ
โ0) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
109 | 66, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ผ โ โ0
โ ((โฏโ๐)
โ โ โ ((๐ฟ
โ โค โง ๐ฆ
โ โ0) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
110 | 109 | imp 408 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ผ โ โ0
โง (โฏโ๐)
โ โ) โ ((๐ฟ
โ โค โง ๐ฆ
โ โ0) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))) |
111 | 110 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
โข ((๐ผ โ โ0
โง (โฏโ๐)
โ โ โง ๐ผ <
(โฏโ๐)) โ
((๐ฟ โ โค โง
๐ฆ โ
โ0) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))) |
112 | 42, 111 | sylbi 216 |
. . . . . . . . . . . . . . . 16
โข (๐ผ โ
(0..^(โฏโ๐))
โ ((๐ฟ โ โค
โง ๐ฆ โ
โ0) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))) |
113 | 112 | expd 417 |
. . . . . . . . . . . . . . 15
โข (๐ผ โ
(0..^(โฏโ๐))
โ (๐ฟ โ โค
โ (๐ฆ โ
โ0 โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
114 | 113 | adantld 492 |
. . . . . . . . . . . . . 14
โข (๐ผ โ
(0..^(โฏโ๐))
โ ((๐ โ Word
๐ โง ๐ฟ โ โค) โ (๐ฆ โ โ0 โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
115 | 114 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))) โ ((๐ โ Word ๐ โง ๐ฟ โ โค) โ (๐ฆ โ โ0 โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
116 | 115 | impcom 409 |
. . . . . . . . . . . 12
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐ฆ โ โ0 โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))) |
117 | 116 | impcom 409 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐)) = ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))) |
118 | 117 | fveq2d 6851 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ (๐โ((((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)) + ๐ฟ) mod (โฏโ๐))) = (๐โ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))) |
119 | 39, 65, 118 | 3eqtrd 2781 |
. . . . . . . . 9
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) = (๐โ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))) |
120 | 119 | eqeq2d 2748 |
. . . . . . . 8
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ ((๐โ๐ผ) = (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) โ (๐โ๐ผ) = (๐โ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
121 | 120 | biimpd 228 |
. . . . . . 7
โข ((๐ฆ โ โ0
โง ((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))))) โ ((๐โ๐ผ) = (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) โ (๐โ๐ผ) = (๐โ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐))))) |
122 | 121 | ex 414 |
. . . . . 6
โข (๐ฆ โ โ0
โ (((๐ โ Word
๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ ((๐โ๐ผ) = (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐))) โ (๐โ๐ผ) = (๐โ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))))) |
123 | 122 | a2d 29 |
. . . . 5
โข (๐ฆ โ โ0
โ ((((๐ โ Word
๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ฆ ยท ๐ฟ)) mod (โฏโ๐)))) โ (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + ((๐ฆ + 1) ยท ๐ฟ)) mod (โฏโ๐)))))) |
124 | 5, 10, 15, 20, 35, 123 | nn0ind 12605 |
. . . 4
โข (๐ โ โ0
โ (((๐ โ Word
๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ ยท ๐ฟ)) mod (โฏโ๐))))) |
125 | 124 | com12 32 |
. . 3
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ (๐ โ โ0 โ (๐โ๐ผ) = (๐โ((๐ผ + (๐ ยท ๐ฟ)) mod (โฏโ๐))))) |
126 | 125 | ralrimiv 3143 |
. 2
โข (((๐ โ Word ๐ โง ๐ฟ โ โค) โง ((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐)))) โ โ๐ โ โ0
(๐โ๐ผ) = (๐โ((๐ผ + (๐ ยท ๐ฟ)) mod (โฏโ๐)))) |
127 | 126 | ex 414 |
1
โข ((๐ โ Word ๐ โง ๐ฟ โ โค) โ (((๐ cyclShift ๐ฟ) = ๐ โง ๐ผ โ (0..^(โฏโ๐))) โ โ๐ โ โ0
(๐โ๐ผ) = (๐โ((๐ผ + (๐ ยท ๐ฟ)) mod (โฏโ๐))))) |