Step | Hyp | Ref
| Expression |
1 | | erclwwlkn.w |
. . . . 5
⢠ð = (ð ClWWalksN ðº) |
2 | | erclwwlkn.r |
. . . . 5
⢠⌠=
{âšð¡, ð¢â© ⣠(ð¡ â ð ⧠ð¢ â ð ⧠âð â (0...ð)ð¡ = (ð¢ cyclShift ð))} |
3 | 1, 2 | eclclwwlkn1 29019 |
. . . 4
⢠(ð â (ð / ⌠) â (ð â (ð / ⌠) â
âð¥ â ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)})) |
4 | | rabeq 3421 |
. . . . . . . . . 10
⢠(ð = (ð ClWWalksN ðº) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
5 | 1, 4 | mp1i 13 |
. . . . . . . . 9
⢠((ð â â ⧠ð¥ â ð) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
6 | | prmnn 16550 |
. . . . . . . . . . 11
⢠(ð â â â ð â
â) |
7 | 6 | nnnn0d 12473 |
. . . . . . . . . 10
⢠(ð â â â ð â
â0) |
8 | 1 | eleq2i 2829 |
. . . . . . . . . . 11
⢠(ð¥ â ð â ð¥ â (ð ClWWalksN ðº)) |
9 | 8 | biimpi 215 |
. . . . . . . . . 10
⢠(ð¥ â ð â ð¥ â (ð ClWWalksN ðº)) |
10 | | clwwlknscsh 29006 |
. . . . . . . . . 10
⢠((ð â â0
⧠ð¥ â (ð ClWWalksN ðº)) â {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
11 | 7, 9, 10 | syl2an 596 |
. . . . . . . . 9
⢠((ð â â ⧠ð¥ â ð) â {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
12 | 5, 11 | eqtrd 2776 |
. . . . . . . 8
⢠((ð â â ⧠ð¥ â ð) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
13 | 12 | eqeq2d 2747 |
. . . . . . 7
⢠((ð â â ⧠ð¥ â ð) â (ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)})) |
14 | | simpll 765 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â ð¥ â Word (Vtxâðº)) |
15 | | elnnne0 12427 |
. . . . . . . . . . . . . . . . . 18
⢠(ð â â â (ð â â0
⧠ð â
0)) |
16 | | eqeq1 2740 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð = (â¯âð¥) â (ð = 0 â (â¯âð¥) = 0)) |
17 | 16 | eqcoms 2744 |
. . . . . . . . . . . . . . . . . . . . 21
â¢
((â¯âð¥) =
ð â (ð = 0 â (â¯âð¥) = 0)) |
18 | | hasheq0 14263 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ð¥ â Word (Vtxâðº) â ((â¯âð¥) = 0 â ð¥ = â
)) |
19 | 17, 18 | sylan9bbr 511 |
. . . . . . . . . . . . . . . . . . . 20
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð = 0 â ð¥ = â
)) |
20 | 19 | necon3bid 2988 |
. . . . . . . . . . . . . . . . . . 19
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â 0 â ð¥ â â
)) |
21 | 20 | biimpcd 248 |
. . . . . . . . . . . . . . . . . 18
⢠(ð â 0 â ((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â ð¥ â â
)) |
22 | 15, 21 | simplbiim 505 |
. . . . . . . . . . . . . . . . 17
⢠(ð â â â ((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â ð¥ â â
)) |
23 | 22 | impcom 408 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â ð¥ â â
) |
24 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â (â¯âð¥) = ð) |
25 | 24 | eqcomd 2742 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â ð = (â¯âð¥)) |
26 | 14, 23, 25 | 3jca 1128 |
. . . . . . . . . . . . . . 15
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥))) |
27 | 26 | ex 413 |
. . . . . . . . . . . . . 14
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â â â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)))) |
28 | | eqid 2736 |
. . . . . . . . . . . . . . 15
â¢
(Vtxâðº) =
(Vtxâðº) |
29 | 28 | clwwlknbp 28979 |
. . . . . . . . . . . . . 14
⢠(ð¥ â (ð ClWWalksN ðº) â (ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð)) |
30 | 27, 29 | syl11 33 |
. . . . . . . . . . . . 13
⢠(ð â â â (ð¥ â (ð ClWWalksN ðº) â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)))) |
31 | 8, 30 | biimtrid 241 |
. . . . . . . . . . . 12
⢠(ð â â â (ð¥ â ð â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)))) |
32 | 6, 31 | syl 17 |
. . . . . . . . . . 11
⢠(ð â â â (ð¥ â ð â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)))) |
33 | 32 | imp 407 |
. . . . . . . . . 10
⢠((ð â â ⧠ð¥ â ð) â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥))) |
34 | | scshwfzeqfzo 14715 |
. . . . . . . . . 10
⢠((ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)) â {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)}) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⢠((ð â â ⧠ð¥ â ð) â {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)}) |
36 | 35 | eqeq2d 2747 |
. . . . . . . 8
⢠((ð â â ⧠ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)})) |
37 | | oveq2 7365 |
. . . . . . . . . . . . . . . . . . . . . . 23
⢠(ð = ð â (ð¥ cyclShift ð) = (ð¥ cyclShift ð)) |
38 | 37 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð = ð â (ðŠ = (ð¥ cyclShift ð) â ðŠ = (ð¥ cyclShift ð))) |
39 | 38 | cbvrexvw 3226 |
. . . . . . . . . . . . . . . . . . . . 21
â¢
(âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)) |
40 | | eqeq1 2740 |
. . . . . . . . . . . . . . . . . . . . . . 23
⢠(ðŠ = ð¢ â (ðŠ = (ð¥ cyclShift ð) â ð¢ = (ð¥ cyclShift ð))) |
41 | | eqcom 2743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⢠(ð¢ = (ð¥ cyclShift ð) â (ð¥ cyclShift ð) = ð¢) |
42 | 40, 41 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ðŠ = ð¢ â (ðŠ = (ð¥ cyclShift ð) â (ð¥ cyclShift ð) = ð¢)) |
43 | 42 | rexbidv 3175 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ðŠ = ð¢ â (âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢)) |
44 | 39, 43 | bitrid 282 |
. . . . . . . . . . . . . . . . . . . 20
⢠(ðŠ = ð¢ â (âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢)) |
45 | 44 | cbvrabv 3417 |
. . . . . . . . . . . . . . . . . . 19
⢠{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} = {ð¢ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢} |
46 | 45 | cshwshash 16977 |
. . . . . . . . . . . . . . . . . 18
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) â â) â
((â¯â{ðŠ â
Word (Vtxâðº) â£
âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥) âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1)) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) â â) ⧠ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â ((â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥) âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1)) |
48 | 47 | orcomd 869 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) â â) ⧠ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â ((â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1 âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥))) |
49 | | fveqeq2 6851 |
. . . . . . . . . . . . . . . . . 18
⢠(ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 â (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1)) |
50 | | fveqeq2 6851 |
. . . . . . . . . . . . . . . . . 18
⢠(ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = (â¯âð¥) â (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥))) |
51 | 49, 50 | orbi12d 917 |
. . . . . . . . . . . . . . . . 17
⢠(ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)) â ((â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1 âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥)))) |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) â â) ⧠ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â (((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)) â ((â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1 âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥)))) |
53 | 48, 52 | mpbird 256 |
. . . . . . . . . . . . . . 15
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) â â) ⧠ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥))) |
54 | 53 | ex 413 |
. . . . . . . . . . . . . 14
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))) |
55 | 54 | ex 413 |
. . . . . . . . . . . . 13
⢠(ð¥ â Word (Vtxâðº) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥))))) |
56 | 55 | adantr 481 |
. . . . . . . . . . . 12
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥))))) |
57 | | eleq1 2825 |
. . . . . . . . . . . . . . 15
⢠(ð = (â¯âð¥) â (ð â â â (â¯âð¥) â
â)) |
58 | | oveq2 7365 |
. . . . . . . . . . . . . . . . . . 19
⢠(ð = (â¯âð¥) â (0..^ð) = (0..^(â¯âð¥))) |
59 | 58 | rexeqdv 3314 |
. . . . . . . . . . . . . . . . . 18
⢠(ð = (â¯âð¥) â (âð â (0..^ð)ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð))) |
60 | 59 | rabbidv 3415 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) |
61 | 60 | eqeq2d 2747 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)})) |
62 | | eqeq2 2748 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â ((â¯âð) = ð â (â¯âð) = (â¯âð¥))) |
63 | 62 | orbi2d 914 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â (((â¯âð) = 1 âš (â¯âð) = ð) â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))) |
64 | 61, 63 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⢠(ð = (â¯âð¥) â ((ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð)) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥))))) |
65 | 57, 64 | imbi12d 344 |
. . . . . . . . . . . . . 14
⢠(ð = (â¯âð¥) â ((ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))))) |
66 | 65 | eqcoms 2744 |
. . . . . . . . . . . . 13
â¢
((â¯âð¥) =
ð â ((ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))))) |
67 | 66 | adantl 482 |
. . . . . . . . . . . 12
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â ((ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))))) |
68 | 56, 67 | mpbird 256 |
. . . . . . . . . . 11
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð)))) |
69 | 29, 68 | syl 17 |
. . . . . . . . . 10
⢠(ð¥ â (ð ClWWalksN ðº) â (ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð)))) |
70 | 69, 1 | eleq2s 2855 |
. . . . . . . . 9
⢠(ð¥ â ð â (ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð)))) |
71 | 70 | impcom 408 |
. . . . . . . 8
⢠((ð â â ⧠ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) |
72 | 36, 71 | sylbid 239 |
. . . . . . 7
⢠((ð â â ⧠ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) |
73 | 13, 72 | sylbid 239 |
. . . . . 6
⢠((ð â â ⧠ð¥ â ð) â (ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) |
74 | 73 | rexlimdva 3152 |
. . . . 5
⢠(ð â â â
(âð¥ â ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) |
75 | 74 | com12 32 |
. . . 4
â¢
(âð¥ â
ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â (ð â â â ((â¯âð) = 1 âš (â¯âð) = ð))) |
76 | 3, 75 | syl6bi 252 |
. . 3
⢠(ð â (ð / ⌠) â (ð â (ð / ⌠) â (ð â â â
((â¯âð) = 1 âš
(â¯âð) = ð)))) |
77 | 76 | pm2.43i 52 |
. 2
⢠(ð â (ð / ⌠) â (ð â â â
((â¯âð) = 1 âš
(â¯âð) = ð))) |
78 | 77 | impcom 408 |
1
⢠((ð â â ⧠ð â (ð / ⌠)) â
((â¯âð) = 1 âš
(â¯âð) = ð)) |