Step | Hyp | Ref
| Expression |
1 | | wwlkextbij.d |
. . 3
 Word         substr      
 lastS    lastS       |
2 | | wwlkextbij.r |
. . 3
  lastS       |
3 | | wwlkextbij.f |
. . 3
 lastS     |
4 | 1, 2, 3 | wwlkextfun 25469 |
. 2

      |
5 | | fveq2 5870 |
. . . . . . 7
 lastS   lastS     |
6 | | fvex 5880 |
. . . . . . 7
lastS    |
7 | 5, 3, 6 | fvmpt 5953 |
. . . . . 6
    
lastS     |
8 | | fveq2 5870 |
. . . . . . 7
 lastS   lastS     |
9 | | fvex 5880 |
. . . . . . 7
lastS    |
10 | 8, 3, 9 | fvmpt 5953 |
. . . . . 6
    
lastS     |
11 | 7, 10 | eqeqan12d 2469 |
. . . . 5
 
          lastS   lastS      |
12 | 11 | adantl 468 |
. . . 4
  
          
lastS   lastS      |
13 | | fveq2 5870 |
. . . . . . . . 9
           |
14 | 13 | eqeq1d 2455 |
. . . . . . . 8
       
         |
15 | | oveq1 6302 |
. . . . . . . . 9
  substr      
 substr         |
16 | 15 | eqeq1d 2455 |
. . . . . . . 8
   substr
       substr
         |
17 | | fveq2 5870 |
. . . . . . . . . 10
 lastS   lastS     |
18 | 17 | preq2d 4061 |
. . . . . . . . 9
  lastS    lastS    
lastS    lastS      |
19 | 18 | eleq1d 2515 |
. . . . . . . 8
  
lastS    lastS    
lastS    lastS       |
20 | 14, 16, 19 | 3anbi123d 1341 |
. . . . . . 7
         
substr        lastS    lastS             substr  
     lastS   
lastS        |
21 | 20, 1 | elrab2 3200 |
. . . . . 6

 Word         substr      
 lastS    lastS        |
22 | | fveq2 5870 |
. . . . . . . . 9
           |
23 | 22 | eqeq1d 2455 |
. . . . . . . 8
       
         |
24 | | oveq1 6302 |
. . . . . . . . 9
  substr      
 substr         |
25 | 24 | eqeq1d 2455 |
. . . . . . . 8
   substr
       substr
         |
26 | | fveq2 5870 |
. . . . . . . . . 10
 lastS   lastS     |
27 | 26 | preq2d 4061 |
. . . . . . . . 9
  lastS    lastS    
lastS    lastS      |
28 | 27 | eleq1d 2515 |
. . . . . . . 8
  
lastS    lastS    
lastS    lastS       |
29 | 23, 25, 28 | 3anbi123d 1341 |
. . . . . . 7
         
substr        lastS    lastS             substr      
 lastS    lastS        |
30 | 29, 1 | elrab2 3200 |
. . . . . 6

 Word         substr      
 lastS    lastS        |
31 | | eqtr3 2474 |
. . . . . . . . . . . . . . . . 17
                         |
32 | 31 | expcom 437 |
. . . . . . . . . . . . . . . 16
                         |
33 | 32 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . 15
        
substr        lastS    lastS    
      
           |
34 | 33 | adantl 468 |
. . . . . . . . . . . . . 14
  Word        
substr        lastS    lastS                        |
35 | 34 | com12 32 |
. . . . . . . . . . . . 13
         Word        
substr        lastS    lastS                 |
36 | 35 | 3ad2ant1 1030 |
. . . . . . . . . . . 12
        
substr        lastS    lastS    
  Word
       
substr        lastS    lastS                 |
37 | 36 | adantl 468 |
. . . . . . . . . . 11
  Word        
substr        lastS    lastS        Word        
substr        lastS    lastS                 |
38 | 37 | imp 431 |
. . . . . . . . . 10
   Word        
substr        lastS    lastS       Word
       
substr        lastS    lastS                 |
39 | 38 | adantr 467 |
. . . . . . . . 9
    Word         substr  
     lastS   
lastS       Word
       
substr        lastS    lastS      
           |
40 | 39 | adantr 467 |
. . . . . . . 8
     Word         substr      
 lastS    lastS       Word
       
substr        lastS    lastS      
 lastS   lastS   
          |
41 | | simpr 463 |
. . . . . . . 8
     Word         substr      
 lastS    lastS       Word
       
substr        lastS    lastS      
 lastS   lastS   
lastS   lastS     |
42 | | eqtr3 2474 |
. . . . . . . . . . . . . . . . . . . 20
   substr      
 substr      

 substr        substr         |
43 | | 1e2m1 10732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

    |
45 | 44 | oveq2d 6311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

        |
46 | | nn0cn 10886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
47 | | 2cnd 10689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
48 | | 1cnd 9664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
49 | 46, 47, 48 | addsubassd 10011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

          |
50 | 45, 49 | eqtr4d 2490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

        |
51 | 50 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
52 | | oveq1 6302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   |
53 | 52 | eqeq2d 2463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               
         |
54 | 53 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                           |
55 | 51, 54 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
56 | | opeq2 4170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
    
 
         |
57 | 56 | oveq2d 6311 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
 substr        substr             |
58 | 56 | oveq2d 6311 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
 substr        substr             |
59 | 57, 58 | eqeq12d 2468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
  substr      
 substr      
 substr  
         substr              |
60 | 55, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
           substr  
     substr        substr  
         substr              |
61 | 60 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . . . 22
           substr  
     substr      
 substr            substr              |
62 | 61 | ex 436 |
. . . . . . . . . . . . . . . . . . . . 21

         substr
       substr      
 substr            substr               |
63 | 62 | com13 83 |
. . . . . . . . . . . . . . . . . . . 20
  substr      
 substr      
       
 substr          
 substr               |
64 | 42, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   substr      
 substr      

      

 substr            substr               |
65 | 64 | ex 436 |
. . . . . . . . . . . . . . . . . 18
  substr      
  substr      
       
 substr          
 substr                |
66 | 65 | com23 81 |
. . . . . . . . . . . . . . . . 17
  substr      
         substr      

 substr            substr                |
67 | 66 | impcom 432 |
. . . . . . . . . . . . . . . 16
        
substr       
  substr      
  substr            substr               |
68 | 67 | com12 32 |
. . . . . . . . . . . . . . 15
  substr      
         substr  
       substr  
         substr               |
69 | 68 | 3ad2ant2 1031 |
. . . . . . . . . . . . . 14
        
substr        lastS    lastS    
         substr      


 substr            substr               |
70 | 69 | adantl 468 |
. . . . . . . . . . . . 13
  Word        
substr        lastS    lastS              
substr       

 substr            substr               |
71 | 70 | com12 32 |
. . . . . . . . . . . 12
        
substr       
  Word
       
substr        lastS    lastS      
 substr          
 substr               |
72 | 71 | 3adant3 1029 |
. . . . . . . . . . 11
        
substr        lastS    lastS    
  Word
       
substr        lastS    lastS      
 substr          
 substr               |
73 | 72 | adantl 468 |
. . . . . . . . . 10
  Word        
substr        lastS    lastS        Word        
substr        lastS    lastS      
 substr          
 substr               |
74 | 73 | imp31 434 |
. . . . . . . . 9
    Word         substr  
     lastS   
lastS       Word
       
substr        lastS    lastS      
  substr
         
 substr             |
75 | 74 | adantr 467 |
. . . . . . . 8
     Word         substr      
 lastS    lastS       Word
       
substr        lastS    lastS      
 lastS   lastS   
 substr            substr             |
76 | | simpl 459 |
. . . . . . . . . . . . 13
  Word        
substr        lastS    lastS      Word   |
77 | | simpl 459 |
. . . . . . . . . . . . 13
  Word        
substr        lastS    lastS      Word   |
78 | 76, 77 | anim12i 570 |
. . . . . . . . . . . 12
   Word        
substr        lastS    lastS       Word
       
substr        lastS    lastS        Word
Word    |
79 | 78 | adantr 467 |
. . . . . . . . . . 11
    Word         substr  
     lastS   
lastS       Word
       
substr        lastS    lastS      
  Word
Word    |
80 | | nn0re 10885 |
. . . . . . . . . . . . . . . . . . . . 21

  |
81 | | 2re 10686 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21

  |
83 | | nn0ge0 10902 |
. . . . . . . . . . . . . . . . . . . . 21

  |
84 | | 2pos 10708 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21

  |
86 | 80, 82, 83, 85 | addgegt0d 10194 |
. . . . . . . . . . . . . . . . . . . 20

    |
87 | 86 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
       

    |
88 | | breq2 4409 |
. . . . . . . . . . . . . . . . . . . 20
       
    
    |
89 | 88 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
       
     
     |
90 | 87, 89 | mpbird 236 |
. . . . . . . . . . . . . . . . . 18
       

      |
91 | | hashgt0n0 12553 |
. . . . . . . . . . . . . . . . . 18
  Word        |
92 | 90, 91 | sylan2 477 |
. . . . . . . . . . . . . . . . 17
  Word       
    |
93 | 92 | exp32 610 |
. . . . . . . . . . . . . . . 16
 Word        
    |
94 | 93 | com12 32 |
. . . . . . . . . . . . . . 15
        Word
     |
95 | 94 | 3ad2ant1 1030 |
. . . . . . . . . . . . . 14
        
substr        lastS    lastS    
 Word

    |
96 | 95 | impcom 432 |
. . . . . . . . . . . . 13
  Word        
substr        lastS    lastS      
   |
97 | 96 | adantr 467 |
. . . . . . . . . . . 12
   Word        
substr        lastS    lastS       Word
       
substr        lastS    lastS           |
98 | 97 | imp 431 |
. . . . . . . . . . 11
    Word         substr  
     lastS   
lastS       Word
       
substr        lastS    lastS      
   |
99 | 86 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
       

    |
100 | | breq2 4409 |
. . . . . . . . . . . . . . . . . . . 20
       
    
    |
101 | 100 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
       
     
     |
102 | 99, 101 | mpbird 236 |
. . . . . . . . . . . . . . . . . 18
       

      |
103 | | hashgt0n0 12553 |
. . . . . . . . . . . . . . . . . 18
  Word        |
104 | 102, 103 | sylan2 477 |
. . . . . . . . . . . . . . . . 17
  Word       
    |
105 | 104 | exp32 610 |
. . . . . . . . . . . . . . . 16
 Word        
    |
106 | 105 | com12 32 |
. . . . . . . . . . . . . . 15
        Word
     |
107 | 106 | 3ad2ant1 1030 |
. . . . . . . . . . . . . 14
        
substr        lastS    lastS    
 Word

    |
108 | 107 | impcom 432 |
. . . . . . . . . . . . 13
  Word        
substr        lastS    lastS      
   |
109 | 108 | adantl 468 |
. . . . . . . . . . . 12
   Word        
substr        lastS    lastS       Word
       
substr        lastS    lastS           |
110 | 109 | imp 431 |
. . . . . . . . . . 11
    Word         substr  
     lastS   
lastS       Word
       
substr        lastS    lastS      
   |
111 | 79, 98, 110 | jca32 538 |
. . . . . . . . . 10
    Word         substr  
     lastS   
lastS       Word
       
substr        lastS    lastS      
   Word Word 
     |
112 | 111 | adantr 467 |
. . . . . . . . 9
     Word         substr      
 lastS    lastS       Word
       
substr        lastS    lastS      
 lastS   lastS   
  Word
Word       |
113 | | simpl 459 |
. . . . . . . . . . . 12
  Word
Word  Word   |
114 | 113 | adantr 467 |
. . . . . . . . . . 11
   Word
Word     Word   |
115 | | simpr 463 |
. . . . . . . . . . . 12
  Word
Word  Word   |
116 | 115 | adantr 467 |
. . . . . . . . . . 11
   Word
Word     Word   |
117 | | hashneq0 12552 |
. . . . . . . . . . . . . . . 16
 Word 
       |
118 | 117 | biimprd 227 |
. . . . . . . . . . . . . . 15
 Word         |
119 | 118 | adantr 467 |
. . . . . . . . . . . . . 14
  Word
Word          |
120 | 119 | com12 32 |
. . . . . . . . . . . . 13

  Word
Word         |
121 | 120 | adantr 467 |
. . . . . . . . . . . 12
     Word
Word         |
122 | 121 | impcom 432 |
. . . . . . . . . . 11
   Word
Word           |
123 | | 2swrd1eqwrdeq 12817 |
. . . . . . . . . . 11
  Word
Word      
        
  substr          
 substr          
lastS   lastS        |
124 | 114, 116,
122, 123 | syl3anc 1269 |
. . . . . . . . . 10
   Word
Word                 substr  
         substr           lastS   lastS        |
125 | | ancom 452 |
. . . . . . . . . . . 12
   substr            substr          
lastS   lastS   
 lastS   lastS    substr          
 substr              |
126 | 125 | anbi2i 701 |
. . . . . . . . . . 11
            substr
         
 substr          
lastS   lastS               lastS   lastS    substr            substr               |
127 | | 3anass 990 |
. . . . . . . . . . 11
          lastS   lastS    substr          
 substr           
        
 lastS   lastS    substr          
 substr               |
128 | 126, 127 | bitr4i 256 |
. . . . . . . . . 10
            substr
         
 substr          
lastS   lastS              lastS   lastS    substr          
 substr              |
129 | 124, 128 | syl6bb 265 |
. . . . . . . . 9
   Word
Word              
lastS   lastS  
 substr            substr               |
130 | 112, 129 | syl 17 |
. . . . . . . 8
     Word         substr      
 lastS    lastS       Word
       
substr        lastS    lastS      
 lastS   lastS   

        
lastS   lastS  
 substr            substr               |
131 | 40, 41, 75, 130 | mpbir3and 1192 |
. . . . . . 7
     Word         substr      
 lastS    lastS       Word
       
substr        lastS    lastS      
 lastS   lastS   
  |
132 | 131 | exp31 609 |
. . . . . 6
   Word        
substr        lastS    lastS       Word
       
substr        lastS    lastS         lastS   lastS  
    |
133 | 21, 30, 132 | syl2anb 482 |
. . . . 5
 
   lastS   lastS  
    |
134 | 133 | impcom 432 |
. . . 4
  
   lastS   lastS      |
135 | 12, 134 | sylbid 219 |
. . 3
  
              |
136 | 135 | ralrimivva 2811 |
. 2



            |
137 | | dff13 6164 |
. 2
    
     

             |
138 | 4, 136, 137 | sylanbrc 671 |
1

      |