Step | Hyp | Ref
| Expression |
1 | | wwlknimp 30459 |
. . . 4
   WWalksN    
 
 Word           ..^                    |
2 | | fzonn0p1 11710 |
. . . . . . . . . . 11

 ..^     |
3 | 2 | adantl 466 |
. . . . . . . . . 10
   Word            ..^     |
4 | | fveq2 5789 |
. . . . . . . . . . . . 13
           |
5 | | oveq1 6197 |
. . . . . . . . . . . . . 14
       |
6 | 5 | fveq2d 5793 |
. . . . . . . . . . . . 13
          
    |
7 | 4, 6 | preq12d 4060 |
. . . . . . . . . . . 12
                             |
8 | 7 | eleq1d 2520 |
. . . . . . . . . . 11
                               |
9 | 8 | rspcv 3165 |
. . . . . . . . . 10
  ..^  
 
 ..^                
         
      |
10 | 3, 9 | syl 16 |
. . . . . . . . 9
   Word              ..^                                 |
11 | 10 | imp 429 |
. . . . . . . 8
    Word             ..^                 
         
     |
12 | | simpll 753 |
. . . . . . . . . . . . . 14
   Word           Word   |
13 | | 1z 10777 |
. . . . . . . . . . . . . . . . 17
 |
14 | 13 | a1i 11 |
. . . . . . . . . . . . . . . 16
   Word             |
15 | | lencl 12351 |
. . . . . . . . . . . . . . . . . 18
 Word       |
16 | 15 | nn0zd 10846 |
. . . . . . . . . . . . . . . . 17
 Word       |
17 | 16 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
   Word                 |
18 | | peano2nn0 10721 |
. . . . . . . . . . . . . . . . . 18

    |
19 | 18 | nn0zd 10846 |
. . . . . . . . . . . . . . . . 17

    |
20 | 19 | adantl 466 |
. . . . . . . . . . . . . . . 16
   Word               |
21 | 14, 17, 20 | 3jca 1168 |
. . . . . . . . . . . . . . 15
   Word                     |
22 | | nn0ge0 10706 |
. . . . . . . . . . . . . . . . . 18

  |
23 | | 1re 9486 |
. . . . . . . . . . . . . . . . . . . 20
 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19

  |
25 | | nn0re 10689 |
. . . . . . . . . . . . . . . . . . 19

  |
26 | 24, 25 | addge02d 10029 |
. . . . . . . . . . . . . . . . . 18


     |
27 | 22, 26 | mpbid 210 |
. . . . . . . . . . . . . . . . 17

    |
28 | 27 | adantl 466 |
. . . . . . . . . . . . . . . 16
   Word           
   |
29 | | nn0re 10689 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    |
30 | 18, 29 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22

    |
31 | 30 | lep1d 10365 |
. . . . . . . . . . . . . . . . . . . . 21

        |
32 | | breq2 4394 |
. . . . . . . . . . . . . . . . . . . . 21
           
             |
33 | 31, 32 | syl5ibrcom 222 |
. . . . . . . . . . . . . . . . . . . 20

         
        |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
    

        
          |
35 | 34 | com23 78 |
. . . . . . . . . . . . . . . . . 18
    
        

          |
36 | 15, 35 | syl 16 |
. . . . . . . . . . . . . . . . 17
 Word          

         |
37 | 36 | imp31 432 |
. . . . . . . . . . . . . . . 16
   Word                   |
38 | 28, 37 | jca 532 |
. . . . . . . . . . . . . . 15
   Word                       |
39 | | elfz2 11545 |
. . . . . . . . . . . . . . 15
          
      
   
           |
40 | 21, 38, 39 | sylanbrc 664 |
. . . . . . . . . . . . . 14
   Word                       |
41 | 12, 40 | jca 532 |
. . . . . . . . . . . . 13
   Word            Word              |
42 | | swrd0fvlsw 12441 |
. . . . . . . . . . . . 13
  Word 
          lastS   substr                  |
43 | 41, 42 | syl 16 |
. . . . . . . . . . . 12
   Word           lastS
  substr                  |
44 | | nn0cn 10690 |
. . . . . . . . . . . . . . 15

  |
45 | | ax-1cn 9441 |
. . . . . . . . . . . . . . . 16
 |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . . 15

  |
47 | 44, 46 | pncand 9821 |
. . . . . . . . . . . . . 14

      |
48 | 47 | fveq2d 5793 |
. . . . . . . . . . . . 13

              |
49 | 48 | adantl 466 |
. . . . . . . . . . . 12
   Word                         |
50 | 43, 49 | eqtrd 2492 |
. . . . . . . . . . 11
   Word           lastS
  substr              |
51 | | lsw 12368 |
. . . . . . . . . . . . 13
 Word lastS               |
52 | 51 | ad2antrr 725 |
. . . . . . . . . . . 12
   Word           lastS
              |
53 | | oveq1 6197 |
. . . . . . . . . . . . . . 15
                       |
54 | 53 | fveq2d 5793 |
. . . . . . . . . . . . . 14
                               |
55 | 54 | adantl 466 |
. . . . . . . . . . . . 13
  Word                                |
56 | 18 | nn0cnd 10739 |
. . . . . . . . . . . . . . 15

    |
57 | 56, 46 | pncand 9821 |
. . . . . . . . . . . . . 14

          |
58 | 57 | fveq2d 5793 |
. . . . . . . . . . . . 13

             
    |
59 | 55, 58 | sylan9eq 2512 |
. . . . . . . . . . . 12
   Word                             |
60 | 52, 59 | eqtrd 2492 |
. . . . . . . . . . 11
   Word           lastS
     
    |
61 | 50, 60 | preq12d 4060 |
. . . . . . . . . 10
   Word            lastS   substr         lastS                   |
62 | 61 | eleq1d 2520 |
. . . . . . . . 9
   Word             lastS   substr         lastS                    |
63 | 62 | adantr 465 |
. . . . . . . 8
    Word             ..^                 
  lastS   substr         lastS                    |
64 | 11, 63 | mpbird 232 |
. . . . . . 7
    Word             ..^                 
 lastS   substr         lastS      |
65 | 64 | exp31 604 |
. . . . . 6
  Word              ..^                  lastS   substr         lastS        |
66 | 65 | com23 78 |
. . . . 5
  Word             ..^                   lastS   substr         lastS        |
67 | 66 | 3impia 1185 |
. . . 4
  Word         
 ..^                  
 lastS   substr         lastS       |
68 | 1, 67 | syl 16 |
. . 3
   WWalksN    
 

 lastS   substr         lastS       |
69 | | hashrabrex.x |
. . 3
  WWalksN        |
70 | 68, 69 | eleq2s 2559 |
. 2
 
 lastS   substr         lastS       |
71 | 70 | imp 429 |
1
 
 
lastS   substr         lastS      |