Step | Hyp | Ref
| Expression |
1 | | rusisusgra 25715 |
. . . 4
  
 RegUSGrph USGrph   |
2 | 1 | adantr 471 |
. . 3
     RegUSGrph 
  USGrph
  |
3 | | simpr2 1021 |
. . 3
     RegUSGrph 
    |
4 | | simp3 1016 |
. . . 4
 

  |
5 | 4 | adantl 472 |
. . 3
     RegUSGrph 
    |
6 | | rusgranumwlk.w |
. . . . 5
   Walks             |
7 | | rusgranumwlk.l |
. . . . 5
 
                    |
8 | 6, 7 | rusgranumwlklem4 25736 |
. . . 4
  USGrph
           WWalksN             |
9 | 8 | eqeq1d 2464 |
. . 3
  USGrph
         
      WWalksN                  |
10 | 2, 3, 5, 9 | syl3anc 1276 |
. 2
     RegUSGrph 
                 WWalksN                  |
11 | | wwlknredwwlkn0 25511 |
. . . . . . . . . . . 12
 
  WWalksN    
       
   WWalksN        substr      
   
 lastS    lastS        |
12 | 11 | ex 440 |
. . . . . . . . . . 11

   WWalksN    
 
    
   WWalksN
       substr      
     lastS   
lastS         |
13 | 12 | 3ad2ant3 1037 |
. . . . . . . . . 10
 
    WWalksN
          
   WWalksN        substr      
   
 lastS    lastS         |
14 | 13 | adantl 472 |
. . . . . . . . 9
     RegUSGrph 
     WWalksN               WWalksN
       substr      
     lastS   
lastS         |
15 | 14 | imp 435 |
. . . . . . . 8
      RegUSGrph 
    WWalksN       
    
   WWalksN
       substr      
     lastS   
lastS        |
16 | 15 | rabbidva 3047 |
. . . . . . 7
     RegUSGrph 
     WWalksN               WWalksN          WWalksN        substr      
   
 lastS    lastS        |
17 | 16 | adantr 471 |
. . . . . 6
      RegUSGrph 
        WWalksN               
   WWalksN               WWalksN          WWalksN        substr      
   
 lastS    lastS        |
18 | 17 | fveq2d 5896 |
. . . . 5
      RegUSGrph 
        WWalksN               
      WWalksN    
              WWalksN    
     WWalksN        substr      
   
 lastS    lastS         |
19 | | simp2 1015 |
. . . . . . . . . . . . 13
   substr      
   
 lastS    lastS           |
20 | 19 | pm4.71ri 643 |
. . . . . . . . . . . 12
   substr      
   
 lastS    lastS    
    
  substr
           lastS    lastS        |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
       RegUSGrph 
 
  WWalksN    
     WWalksN     
   substr
           lastS    lastS            substr      
     lastS   
lastS         |
22 | 21 | rexbidva 2910 |
. . . . . . . . . 10
      RegUSGrph 
    WWalksN       
 
  WWalksN        substr            lastS   
lastS        WWalksN
            substr
           lastS    lastS         |
23 | | fveq1 5891 |
. . . . . . . . . . . 12
           |
24 | 23 | eqeq1d 2464 |
. . . . . . . . . . 11
     
       |
25 | 24 | rexrab 3214 |
. . . . . . . . . 10
     WWalksN            substr            lastS   
lastS        WWalksN
            substr
           lastS    lastS        |
26 | 22, 25 | syl6bbr 271 |
. . . . . . . . 9
      RegUSGrph 
    WWalksN       
 
  WWalksN        substr            lastS   
lastS         WWalksN            substr      
     lastS   
lastS        |
27 | 26 | rabbidva 3047 |
. . . . . . . 8
     RegUSGrph 
     WWalksN          WWalksN        substr      
   
 lastS    lastS      
  WWalksN
      
   WWalksN            substr            lastS   
lastS        |
28 | 27 | adantr 471 |
. . . . . . 7
      RegUSGrph 
        WWalksN               
   WWalksN          WWalksN        substr      
   
 lastS    lastS      
  WWalksN
      
   WWalksN            substr            lastS   
lastS        |
29 | 28 | fveq2d 5896 |
. . . . . 6
      RegUSGrph 
        WWalksN               
      WWalksN    
     WWalksN        substr      
   
 lastS    lastS             WWalksN    
      WWalksN
           substr
           lastS    lastS         |
30 | | simplr1 1056 |
. . . . . . 7
      RegUSGrph 
        WWalksN               
  |
31 | | eqid 2462 |
. . . . . . . 8
  WWalksN    
    WWalksN    
   |
32 | | eqid 2462 |
. . . . . . . 8
   WWalksN             WWalksN           |
33 | 31, 32 | hashwwlkext 25530 |
. . . . . . 7
       WWalksN           WWalksN
           substr
           lastS    lastS           WWalksN                WWalksN
        substr      
   
 lastS    lastS         |
34 | 30, 33 | syl 17 |
. . . . . 6
      RegUSGrph 
        WWalksN               
      WWalksN    
      WWalksN
           substr
           lastS    lastS           WWalksN                WWalksN
        substr      
   
 lastS    lastS         |
35 | | fveq1 5891 |
. . . . . . . . . 10
           |
36 | 35 | eqeq1d 2464 |
. . . . . . . . 9
     
       |
37 | 36 | cbvrabv 3056 |
. . . . . . . 8
   WWalksN             WWalksN           |
38 | 37 | sumeq1i 13819 |
. . . . . . 7
    WWalksN
               WWalksN         substr            lastS   
lastS           WWalksN                WWalksN
        substr      
   
 lastS    lastS        |
39 | 38 | a1i 11 |
. . . . . 6
      RegUSGrph 
        WWalksN               
    WWalksN
               WWalksN         substr            lastS   
lastS           WWalksN                WWalksN
        substr      
   
 lastS    lastS         |
40 | 29, 34, 39 | 3eqtrd 2500 |
. . . . 5
      RegUSGrph 
        WWalksN               
      WWalksN    
     WWalksN        substr      
   
 lastS    lastS           WWalksN                WWalksN
        substr      
   
 lastS    lastS         |
41 | | rusgranumwlklem0 25732 |
. . . . . . . . . . 11
    WWalksN         
   WWalksN         substr        lastS   
lastS         WWalksN    
    substr      
     lastS   
lastS        |
42 | 41 | eqcomd 2468 |
. . . . . . . . . 10
    WWalksN         
   WWalksN         substr            lastS   
lastS         WWalksN    
    substr      
 lastS    lastS        |
43 | 42 | fveq2d 5896 |
. . . . . . . . 9
    WWalksN         
      WWalksN    
    substr      
     lastS   
lastS             WWalksN    
    substr      
 lastS    lastS         |
44 | 43 | adantl 472 |
. . . . . . . 8
       RegUSGrph 
        WWalksN                   WWalksN
                WWalksN    
    substr      
     lastS   
lastS             WWalksN    
    substr      
 lastS    lastS         |
45 | | elrabi 3205 |
. . . . . . . . . 10
    WWalksN         
  WWalksN       |
46 | 45 | adantl 472 |
. . . . . . . . 9
       RegUSGrph 
        WWalksN                   WWalksN
            WWalksN
      |
47 | | wwlkexthasheq 25518 |
. . . . . . . . 9
   WWalksN    
      WWalksN    
    substr      
 lastS    lastS           
lastS         |
48 | 46, 47 | syl 17 |
. . . . . . . 8
       RegUSGrph 
        WWalksN                   WWalksN
                WWalksN    
    substr      
 lastS    lastS           
lastS         |
49 | | rusgraprop3 25727 |
. . . . . . . . . 10
  
 RegUSGrph  USGrph

            |
50 | | fveq1 5891 |
. . . . . . . . . . . . . . . . . . . 20
           |
51 | 50 | eqeq1d 2464 |
. . . . . . . . . . . . . . . . . . 19
     
       |
52 | 51 | elrab 3208 |
. . . . . . . . . . . . . . . . . 18
    WWalksN             WWalksN            |
53 | | wwlknimp 25471 |
. . . . . . . . . . . . . . . . . . . 20
   WWalksN    
 Word         ..^                  |
54 | 53 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
    WWalksN    
      Word
      
 ..^                  |
55 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . . . 22
   Word        
  Word   |
56 | | nn0p1gt0 10933 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

    |
57 | 56 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

    |
58 | 57 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   Word        
      |
59 | | breq2 4422 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
    
    |
60 | 59 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   Word        
  
    
    |
61 | 58, 60 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
   Word        
        |
62 | | hashle00 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 Word     
   |
63 | | lencl 12728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 Word       |
64 | 63 | nn0red 10960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 Word       |
65 | | 0re 9674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
66 | | lenlt 9743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
     
       |
67 | 66 | bicomd 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
             |
68 | 64, 65, 67 | sylancl 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 Word 
   
   
   |
69 | | nne 2639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 Word 
   |
71 | 62, 68, 70 | 3bitr4rd 294 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 Word 
       |
72 | 71 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   Word        
  
       |
73 | 72 | con4bid 299 |
. . . . . . . . . . . . . . . . . . . . . . 23
   Word        
  
       |
74 | 61, 73 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . 22
   Word        
    |
75 | 55, 74 | jca 539 |
. . . . . . . . . . . . . . . . . . . . 21
   Word        
   Word
   |
76 | 75 | ex 440 |
. . . . . . . . . . . . . . . . . . . 20
  Word         
  Word     |
77 | 76 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . 19
  Word       
 ..^                 
  Word
    |
78 | 54, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    WWalksN    
      
  Word
    |
79 | 52, 78 | sylbi 200 |
. . . . . . . . . . . . . . . . 17
    WWalksN         
 
  Word
    |
80 | 79 | imp 435 |
. . . . . . . . . . . . . . . 16
     WWalksN          
   Word
   |
81 | | lswcl 12757 |
. . . . . . . . . . . . . . . 16
  Word  lastS     |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . 15
     WWalksN          
  lastS     |
83 | 82 | ad2antrr 737 |
. . . . . . . . . . . . . 14
       WWalksN
         
        WWalksN                
         
lastS     |
84 | | preq1 4064 |
. . . . . . . . . . . . . . . . . . 19
 lastS  
    lastS       |
85 | 84 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . 18
 lastS  
   
 lastS    
   |
86 | 85 | rabbidv 3048 |
. . . . . . . . . . . . . . . . 17
 lastS  

    
 lastS        |
87 | 86 | fveq2d 5896 |
. . . . . . . . . . . . . . . 16
 lastS  
      
       lastS         |
88 | 87 | eqeq1d 2464 |
. . . . . . . . . . . . . . 15
 lastS  
             
 lastS          |
89 | 88 | rspcva 3160 |
. . . . . . . . . . . . . 14
  lastS  

      
       
lastS         |
90 | 83, 89 | sylancom 678 |
. . . . . . . . . . . . 13
       WWalksN
         
        WWalksN                
         
    
lastS         |
91 | 90 | exp41 619 |
. . . . . . . . . . . 12
    WWalksN         
 
        WWalksN                
      
     
 lastS            |
92 | 91 | com14 91 |
. . . . . . . . . . 11
 
          
        WWalksN                   WWalksN
            
 lastS            |
93 | 92 | 3ad2ant3 1037 |
. . . . . . . . . 10
  USGrph

      
    
        WWalksN                   WWalksN
            
 lastS            |
94 | 49, 93 | syl 17 |
. . . . . . . . 9
  
 RegUSGrph  
        WWalksN
                  WWalksN         
    
lastS            |
95 | 94 | imp41 602 |
. . . . . . . 8
       RegUSGrph 
        WWalksN                   WWalksN
              
lastS         |
96 | 44, 48, 95 | 3eqtrd 2500 |
. . . . . . 7
       RegUSGrph 
        WWalksN                   WWalksN
                WWalksN    
    substr      
     lastS   
lastS         |
97 | 96 | sumeq2dv 13824 |
. . . . . 6
      RegUSGrph 
        WWalksN               
    WWalksN
               WWalksN         substr            lastS   
lastS           WWalksN             |
98 | | oveq1 6327 |
. . . . . . . 8
       WWalksN                      WWalksN
                   |
99 | 98 | adantl 472 |
. . . . . . 7
      RegUSGrph 
        WWalksN               
       WWalksN                    |
100 | | wwlknfi 25522 |
. . . . . . . . . . 11
   WWalksN
      |
101 | 100 | 3ad2ant1 1035 |
. . . . . . . . . 10
 
   WWalksN       |
102 | 101 | ad2antlr 738 |
. . . . . . . . 9
      RegUSGrph 
        WWalksN               
  WWalksN       |
103 | | rabfi 7827 |
. . . . . . . . 9
   WWalksN
       WWalksN
           |
104 | 102, 103 | syl 17 |
. . . . . . . 8
      RegUSGrph 
        WWalksN               
   WWalksN            |
105 | | rusgraprop 25713 |
. . . . . . . . . 10
  
 RegUSGrph  USGrph

  VDeg
       |
106 | | nn0cn 10913 |
. . . . . . . . . . 11

  |
107 | 106 | 3ad2ant2 1036 |
. . . . . . . . . 10
  USGrph

  VDeg        |
108 | 105, 107 | syl 17 |
. . . . . . . . 9
  
 RegUSGrph   |
109 | 108 | ad2antrr 737 |
. . . . . . . 8
      RegUSGrph 
        WWalksN               
  |
110 | | fsumconst 13906 |
. . . . . . . 8
     WWalksN
              WWalksN                  WWalksN              |
111 | 104, 109,
110 | syl2anc 671 |
. . . . . . 7
      RegUSGrph 
        WWalksN               
    WWalksN
                 WWalksN
             |
112 | | expp1 12317 |
. . . . . . . . 9
 
    
          |
113 | 108, 4, 112 | syl2an 484 |
. . . . . . . 8
     RegUSGrph 
                |
114 | 113 | adantr 471 |
. . . . . . 7
      RegUSGrph 
        WWalksN               
              |
115 | 99, 111, 114 | 3eqtr4d 2506 |
. . . . . 6
      RegUSGrph 
        WWalksN               
    WWalksN
                  |
116 | 97, 115 | eqtrd 2496 |
. . . . 5
      RegUSGrph 
        WWalksN               
    WWalksN
               WWalksN         substr            lastS   
lastS          
    |
117 | 18, 40, 116 | 3eqtrd 2500 |
. . . 4
      RegUSGrph 
        WWalksN               
      WWalksN    
           
    |
118 | | peano2nn0 10944 |
. . . . . . . 8

    |
119 | 118 | 3ad2ant3 1037 |
. . . . . . 7
 
     |
120 | 119 | adantl 472 |
. . . . . 6
     RegUSGrph 
      |
121 | 6, 7 | rusgranumwlklem4 25736 |
. . . . . . 7
  USGrph
               WWalksN    
          |
122 | 121 | eqeq1d 2464 |
. . . . . 6
  USGrph
               
      WWalksN    
           
     |
123 | 2, 3, 120, 122 | syl3anc 1276 |
. . . . 5
     RegUSGrph 
            
        WWalksN    
           
     |
124 | 123 | adantr 471 |
. . . 4
      RegUSGrph 
        WWalksN               
          
        WWalksN    
           
     |
125 | 117, 124 | mpbird 240 |
. . 3
      RegUSGrph 
        WWalksN               
         
    |
126 | 125 | ex 440 |
. 2
     RegUSGrph 
         WWalksN
                       
     |
127 | 10, 126 | sylbid 223 |
1
     RegUSGrph 
          
         
     |