MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2cshwcshw Unicode version

Theorem 2cshwcshw 12793
Description: If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018.) (Revised by AV, 12-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)
Assertion
Ref Expression
2cshwcshw
Distinct variable groups:   , ,   ,N,   , ,   , ,   , ,   , ,

Proof of Theorem 2cshwcshw
StepHypRef Expression
1 difelfznle 11818 . . . . . . . . . . . . . . . . . . 19
213exp 1195 . . . . . . . . . . . . . . . . . 18
32ad2antrr 725 . . . . . . . . . . . . . . . . 17
43imp 429 . . . . . . . . . . . . . . . 16
54adantr 465 . . . . . . . . . . . . . . 15
65com12 31 . . . . . . . . . . . . . 14
76adantl 466 . . . . . . . . . . . . 13
87imp 429 . . . . . . . . . . . 12
9 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . 25
109ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
11 elfzelz 11717 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1211adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
1312ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
14 elfz2 11708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
15 elfzelz 11717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
16 zaddcl 10929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1716adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
18 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1917, 18zsubcld 10999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2019ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2115, 20syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2221com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
23223adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2423adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2514, 24sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2625ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
2726imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24
28 2cshw 12781 . . . . . . . . . . . . . . . . . . . . . . . 24
2910, 13, 27, 28syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23
3018, 19zaddcld 10998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3130ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3215, 31syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3332com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
34333adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3534adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3614, 35sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3736ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
3837imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24
39 cshwsublen 12767 . . . . . . . . . . . . . . . . . . . . . . . 24
4010, 38, 39syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
4129, 40eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . 22
42 elfz2nn0 11798 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
43 elfznn0 11800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
44 nn0cn 10830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
45 nn0cn 10830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
46 nn0cn 10830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4745, 46anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
48 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
49 addcl 9595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
5049adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
5148, 50pncan3d 9957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5251oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
53 pncan 9849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5453adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5552, 54eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5644, 47, 55syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5756ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5843, 57syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5958com12 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60593adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6142, 60sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6261adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
63 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6463eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6564imbi2d 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6665adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6766adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6862, 67mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . 25
6968adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
7069imp 429 . . . . . . . . . . . . . . . . . . . . . . 23
7170oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . 22
7241, 71eqtr2d 2499 . . . . . . . . . . . . . . . . . . . . 21
7372adantr 465 . . . . . . . . . . . . . . . . . . . 20
74 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21
7574adantl 466 . . . . . . . . . . . . . . . . . . . 20
7673, 75eqtr4d 2501 . . . . . . . . . . . . . . . . . . 19
7776exp41 610 . . . . . . . . . . . . . . . . . 18
7877com24 87 . . . . . . . . . . . . . . . . 17
7978imp41 593 . . . . . . . . . . . . . . . 16
8079eqeq2d 2471 . . . . . . . . . . . . . . 15
8180biimpd 207 . . . . . . . . . . . . . 14
8281impancom 440 . . . . . . . . . . . . 13
8382impcom 430 . . . . . . . . . . . 12
84 oveq2 6304 . . . . . . . . . . . . . 14
8584eqeq2d 2471 . . . . . . . . . . . . 13
8685rspcev 3210 . . . . . . . . . . . 12
878, 83, 86syl2anc 661 . . . . . . . . . . 11
8887exp31 604 . . . . . . . . . 10
89 oveq2 6304 . . . . . . . . . . . . . . . 16
9089eqeq2d 2471 . . . . . . . . . . . . . . 15
91 cshw0 12765 . . . . . . . . . . . . . . . . . . . . . 22
9291adantr 465 . . . . . . . . . . . . . . . . . . . . 21
9392eqeq2d 2471 . . . . . . . . . . . . . . . . . . . 20
94 fznn0sub2 11810 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9594adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
96 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9796eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9897ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9995, 98mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10099adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
101 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
102 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103 2cshwid 12782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
104102, 11, 103syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
105101, 104sylan9eqr 2520 . . . . . . . . . . . . . . . . . . . . . . . . . 26
106105eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . 25
107 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
108107eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . 26
109108rspcev 3210 . . . . . . . . . . . . . . . . . . . . . . . . 25
110100, 106, 109syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
111110adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
112 eqeq1 2461 . . . . . . . . . . . . . . . . . . . . . . . . 25
113112rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . 24
114113adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
115111, 114mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22
116115exp41 610 . . . . . . . . . . . . . . . . . . . . 21
117116com24 87 . . . . . . . . . . . . . . . . . . . 20
11893, 117sylbid 215 . . . . . . . . . . . . . . . . . . 19
119118com24 87 . . . . . . . . . . . . . . . . . 18
120119impcom 430 . . . . . . . . . . . . . . . . 17
121120com13 80 . . . . . . . . . . . . . . . 16
122121a1d 25 . . . . . . . . . . . . . . 15
12390, 122syl6bi 228 . . . . . . . . . . . . . 14
124123com24 87 . . . . . . . . . . . . 13
125124com15 93 . . . . . . . . . . . 12
126125imp41 593 . . . . . . . . . . 11
127126com12 31 . . . . . . . . . 10
128 difelfzle 11817 . . . . . . . . . . . . . . . . 17
1291283exp 1195 . . . . . . . . . . . . . . . 16
130129ad2antrr 725 . . . . . . . . . . . . . . 15
131130imp 429 . . . . . . . . . . . . . 14
132131adantr 465 . . . . . . . . . . . . 13
133132impcom 430 . . . . . . . . . . . 12
1349ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
13512ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
136 zsubcl 10931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137136ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
13815, 137syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
13911, 138syl5com 30 . . . . . . . . . . . . . . . . . . . . . . . . . 26
140139ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
141140imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24
142 2cshw 12781 . . . . . . . . . . . . . . . . . . . . . . . 24
143134, 135, 141, 142syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23
144 zcn 10894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
14515zcnd 10995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
146 pncan3 9851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
147144, 145, 146syl2anr 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28