Step | Hyp | Ref
| Expression |
1 | | clwwlkbij.d |
. . 3
   WWalksN
    lastS         |
2 | | clwwlkbij.f |
. . 3
  substr       |
3 | 1, 2 | clwwlkf 25601 |
. 2
 
       ClWWalksN       |
4 | 1, 2 | clwwlkfv 25602 |
. . . . . 6
      substr       |
5 | 1, 2 | clwwlkfv 25602 |
. . . . . 6
      substr  
    |
6 | 4, 5 | eqeqan12d 2487 |
. . . . 5
 
           substr
     substr        |
7 | 6 | adantl 473 |
. . . 4
  
              substr
     substr        |
8 | | fveq2 5879 |
. . . . . . . . 9
 lastS   lastS     |
9 | | fveq1 5878 |
. . . . . . . . 9
           |
10 | 8, 9 | eqeq12d 2486 |
. . . . . . . 8
  lastS      
lastS          |
11 | 10, 1 | elrab2 3186 |
. . . . . . 7

   WWalksN    
lastS          |
12 | | fveq2 5879 |
. . . . . . . . 9
 lastS   lastS     |
13 | | fveq1 5878 |
. . . . . . . . 9
           |
14 | 12, 13 | eqeq12d 2486 |
. . . . . . . 8
  lastS      
lastS          |
15 | 14, 1 | elrab2 3186 |
. . . . . . 7

   WWalksN    
lastS          |
16 | 11, 15 | anbi12i 711 |
. . . . . 6
 
     WWalksN
    lastS           WWalksN    
lastS           |
17 | | wwlknimp 25494 |
. . . . . . . . 9
   WWalksN    
 Word         ..^                  |
18 | | wwlknimp 25494 |
. . . . . . . . . . . . 13
   WWalksN    
 Word         ..^                  |
19 | | simprlr 781 |
. . . . . . . . . . . . . . . . . . . . . 22
    Word        lastS          Word        lastS                 |
20 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . . . . 22
    Word        lastS          Word        lastS                 |
21 | 19, 20 | eqtr4d 2508 |
. . . . . . . . . . . . . . . . . . . . 21
    Word        lastS          Word        lastS                   |
22 | 21 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . 20
      Word        lastS          Word        lastS           substr      substr                |
23 | | nncn 10639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
24 | | ax-1cn 9615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
25 | | pncan 9901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
       |
26 | 25 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
       |
27 | 23, 24, 26 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
28 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   |
29 | 28 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
30 | 27, 29 | sylan9eqr 2527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
         |
31 | 30 | opeq2d 4165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
               |
32 | 31 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
  substr      substr             |
33 | 31 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
  substr      substr             |
34 | 32, 33 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
   substr      substr      substr            substr              |
35 | 34 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
  substr      substr      substr            substr               |
36 | 35 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . 23
   Word        lastS        
  substr      substr      substr
         
 substr               |
37 | 36 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
    Word        lastS          Word        lastS         
  substr      substr      substr            substr               |
38 | 37 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . 21
     Word        lastS          Word        lastS            substr      substr  
   substr
         
 substr              |
39 | 38 | biimpa 492 |
. . . . . . . . . . . . . . . . . . . 20
      Word        lastS          Word        lastS           substr      substr       substr          
 substr             |
40 | | simpll 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   Word        lastS        Word   |
41 | | simpll 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   Word        lastS        Word   |
42 | 40, 41 | anim12ci 577 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    Word        lastS          Word        lastS          Word
Word    |
43 | 42 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     Word        lastS          Word        lastS           Word Word    |
44 | | nnnn0 10900 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
45 | | 0nn0 10908 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
46 | 44, 45 | jctil 546 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
47 | 46 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     Word        lastS          Word        lastS          
   |
48 | | nnre 10638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
49 | 48 | lep1d 10560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
50 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
     |
51 | 49, 50 | syl5ibr 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
       |
52 | 51 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   Word        lastS        
       |
53 | 52 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    Word        lastS          Word        lastS         
       |
54 | 53 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     Word        lastS          Word        lastS                |
55 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
     |
56 | 49, 55 | syl5ibr 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
       |
57 | 56 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   Word        lastS        
       |
58 | 57 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    Word        lastS          Word        lastS         
       |
59 | 58 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     Word        lastS          Word        lastS                |
60 | | swrdspsleq 12859 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   Word
Word  
     
        substr
     substr       ..^             |
61 | 43, 47, 54, 59, 60 | syl112anc 1296 |
. . . . . . . . . . . . . . . . . . . . . . 23
     Word        lastS          Word        lastS            substr      substr  
  
 ..^             |
62 | | lbfzo0 11983 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  ..^
  |
63 | 62 | biimpri 211 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  ..^   |
64 | 63 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     Word        lastS          Word        lastS           ..^   |
65 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
66 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
67 | 65, 66 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
           |
68 | 67 | rspcv 3132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ..^
 
 ..^         
           |
69 | 64, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
     Word        lastS          Word        lastS             ..^                     |
70 | 61, 69 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . . . 22
     Word        lastS          Word        lastS            substr      substr  
             |
71 | 70 | imp 436 |
. . . . . . . . . . . . . . . . . . . . 21
      Word        lastS          Word        lastS           substr      substr                |
72 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
   Word        lastS        lastS
        |
73 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
   Word        lastS        lastS
        |
74 | 72, 73 | eqeqan12rd 2489 |
. . . . . . . . . . . . . . . . . . . . . 22
    Word        lastS          Word        lastS          lastS   lastS              |
75 | 74 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . 21
      Word        lastS          Word        lastS           substr      substr       lastS   lastS              |
76 | 71, 75 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . 20
      Word        lastS          Word        lastS           substr      substr      lastS   lastS     |
77 | 22, 39, 76 | jca32 544 |
. . . . . . . . . . . . . . . . . . 19
      Word        lastS          Word        lastS           substr      substr              
  substr          
 substr          
lastS   lastS       |
78 | 41 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
    Word        lastS          Word        lastS         Word   |
79 | 78 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
     Word        lastS          Word        lastS          Word   |
80 | 40 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
    Word        lastS          Word        lastS         Word   |
81 | 80 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
     Word        lastS          Word        lastS          Word   |
82 | | 1red 9676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
83 | | nngt0 10660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
84 | | 0lt1 10157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
86 | 48, 82, 83, 85 | addgt0d 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
87 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
    
    |
88 | 86, 87 | syl5ibr 229 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
       |
89 | 88 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   Word        lastS        
       |
90 | 89 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
    Word        lastS          Word        lastS         
       |
91 | 90 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . . 22
     Word        lastS          Word        lastS                |
92 | 79, 81, 91 | 3jca 1210 |
. . . . . . . . . . . . . . . . . . . . 21
     Word        lastS          Word        lastS           Word Word
       |
93 | 92 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
      Word        lastS          Word        lastS           substr      substr       Word
Word        |
94 | | 2swrd1eqwrdeq 12864 |
. . . . . . . . . . . . . . . . . . . 20
  Word
Word      
        
  substr          
 substr          
lastS   lastS        |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
      Word        lastS          Word        lastS           substr      substr      
        
  substr          
 substr          
lastS   lastS        |
96 | 77, 95 | mpbird 240 |
. . . . . . . . . . . . . . . . . 18
      Word        lastS          Word        lastS           substr      substr        |
97 | 96 | exp31 615 |
. . . . . . . . . . . . . . . . 17
     Word        lastS          Word        lastS           substr      substr    
    |
98 | 97 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . 16
 
     Word        lastS          Word        lastS        
  substr      substr         |
99 | 98 | expdcom 446 |
. . . . . . . . . . . . . . 15
   Word        lastS           Word        lastS         
   substr      substr  
       |
100 | 99 | ex 441 |
. . . . . . . . . . . . . 14
  Word         lastS          Word        lastS       
 
   substr      substr    
      |
101 | 100 | 3adant3 1050 |
. . . . . . . . . . . . 13
  Word       
 ..^                 lastS      
   Word        lastS         
   substr
     substr    
      |
102 | 18, 101 | syl 17 |
. . . . . . . . . . . 12
   WWalksN    
 lastS          Word        lastS         
   substr      substr  
        |
103 | 102 | imp 436 |
. . . . . . . . . . 11
    WWalksN    
lastS           Word        lastS         
   substr      substr  
       |
104 | 103 | expdcom 446 |
. . . . . . . . . 10
  Word         lastS           WWalksN    
lastS             substr
     substr    
      |
105 | 104 | 3adant3 1050 |
. . . . . . . . 9
  Word       
 ..^                 lastS      
    WWalksN    
lastS         
   substr
     substr    
      |
106 | 17, 105 | syl 17 |
. . . . . . . 8
   WWalksN    
 lastS           WWalksN    
lastS         
   substr
     substr    
      |
107 | 106 | imp31 439 |
. . . . . . 7
     WWalksN
    lastS           WWalksN    
lastS        
 
   substr      substr    
    |
108 | 107 | com12 31 |
. . . . . 6
 
      WWalksN    
lastS           WWalksN    
lastS           substr      substr  
      |
109 | 16, 108 | syl5bi 225 |
. . . . 5
 
      substr
     substr    
    |
110 | 109 | imp 436 |
. . . 4
  
      substr      substr    
   |
111 | 7, 110 | sylbid 223 |
. . 3
  
                |
112 | 111 | ralrimivva 2814 |
. 2
 
  
            |
113 | | dff13 6177 |
. 2
       ClWWalksN            ClWWalksN      
        
    |
114 | 3, 112, 113 | sylanbrc 677 |
1
 
       ClWWalksN
      |