Step 
Hyp 
Ref 
Expression 
1 

orc 
 ( ( L mod ( # ` W ) ) = 0 > ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) 
2 
1

2a1d 
 ( ( L mod ( # ` W ) ) = 0 > ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) > ( ( W cyclShift L ) = W > ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) ) ) 
3 

3simpa 
 ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) > ( W e. Word V /\ ( # ` W ) e. Prime ) ) 
4 
3

ad2antlr 
 ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) > ( W e. Word V /\ ( # ` W ) e. Prime ) ) 
5 

simplr3 
 ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) > L e. ZZ ) 
6 

simpll 
 ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) > ( L mod ( # ` W ) ) =/= 0 ) 
7 

simpr 
 ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) > ( W cyclShift L ) = W ) 
8 

cshwsidrepsw 
 ( ( W e. Word V /\ ( # ` W ) e. Prime ) > ( ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) > W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) 
9 
8

imp 
 ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) > W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) 
10 
4 5 6 7 9

syl13anc 
 ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) > W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) 
11 
10

olcd 
 ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) > ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) 
12 
11

exp31 
 ( ( L mod ( # ` W ) ) =/= 0 > ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) > ( ( W cyclShift L ) = W > ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) ) ) 
13 
2 12

pm2.61ine 
 ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) > ( ( W cyclShift L ) = W > ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) ) 