Step | Hyp | Ref
| Expression |
1 | | usgrav 25058 |
. . 3
 USGrph 
   |
2 | | 2nn0 10883 |
. . . . 5
 |
3 | | isclwwlkn 25490 |
. . . . 5
 
 
  ClWWalksN       ClWWalks
         |
4 | 2, 3 | mp3an3 1352 |
. . . 4
 
    ClWWalksN
   
  ClWWalks
         |
5 | | isclwwlk 25489 |
. . . . 5
 
   ClWWalks 
 Word   ..^                      lastS             |
6 | 5 | anbi1d 710 |
. . . 4
 
    ClWWalks
        Word   ..^                      lastS                  |
7 | 4, 6 | bitrd 257 |
. . 3
 
    ClWWalksN
   
 
Word 
 ..^                      lastS                  |
8 | 1, 7 | syl 17 |
. 2
 USGrph    ClWWalksN    
 
Word 
 ..^                      lastS                  |
9 | | 3anass 988 |
. . . . 5
  Word   ..^                      lastS           Word    ..^                      lastS             |
10 | | oveq1 6295 |
. . . . . . . . . . . 12
               |
11 | 10 | oveq2d 6304 |
. . . . . . . . . . 11
      ..^        ..^     |
12 | 11 | raleqdv 2992 |
. . . . . . . . . 10
      
 ..^                       ..^                    |
13 | 12 | ad2antlr 732 |
. . . . . . . . 9
   USGrph     
Word     ..^                       ..^                    |
14 | | 2m1e1 10721 |
. . . . . . . . . . . . 13
   |
15 | 14 | oveq2i 6299 |
. . . . . . . . . . . 12
 ..^    ..^  |
16 | | fzo01 11992 |
. . . . . . . . . . . 12
 ..^    |
17 | 15, 16 | eqtri 2472 |
. . . . . . . . . . 11
 ..^      |
18 | 17 | a1i 11 |
. . . . . . . . . 10
   USGrph     
Word   ..^       |
19 | 18 | raleqdv 2992 |
. . . . . . . . 9
   USGrph     
Word     ..^                                    |
20 | | c0ex 9634 |
. . . . . . . . . 10
 |
21 | | fveq2 5863 |
. . . . . . . . . . . . 13
           |
22 | | oveq1 6295 |
. . . . . . . . . . . . . . 15
       |
23 | | 0p1e1 10718 |
. . . . . . . . . . . . . . 15
   |
24 | 22, 23 | syl6eq 2500 |
. . . . . . . . . . . . . 14
     |
25 | 24 | fveq2d 5867 |
. . . . . . . . . . . . 13
             |
26 | 21, 25 | preq12d 4058 |
. . . . . . . . . . . 12
                           |
27 | 26 | eleq1d 2512 |
. . . . . . . . . . 11
                             |
28 | 27 | ralsng 4005 |
. . . . . . . . . 10
  
                             |
29 | 20, 28 | mp1i 13 |
. . . . . . . . 9
   USGrph     
Word                  
              |
30 | 13, 19, 29 | 3bitrd 283 |
. . . . . . . 8
   USGrph     
Word     ..^                                   |
31 | 30 | anbi1d 710 |
. . . . . . 7
   USGrph     
Word      ..^                      lastS                       lastS             |
32 | | lsw 12708 |
. . . . . . . . . . . . . 14
 Word lastS               |
33 | 32 | adantl 468 |
. . . . . . . . . . . . 13
   USGrph     
Word  lastS               |
34 | 10 | ad2antlr 732 |
. . . . . . . . . . . . . . 15
   USGrph     
Word            |
35 | 34, 14 | syl6eq 2500 |
. . . . . . . . . . . . . 14
   USGrph     
Word          |
36 | 35 | fveq2d 5867 |
. . . . . . . . . . . . 13
   USGrph     
Word                  |
37 | 33, 36 | eqtr2d 2485 |
. . . . . . . . . . . 12
   USGrph     
Word      lastS     |
38 | 37 | preq2d 4057 |
. . . . . . . . . . 11
   USGrph     
Word                   lastS      |
39 | | prcom 4049 |
. . . . . . . . . . 11
      lastS     lastS          |
40 | 38, 39 | syl6eq 2500 |
. . . . . . . . . 10
   USGrph     
Word              lastS           |
41 | 40 | eleq1d 2512 |
. . . . . . . . 9
   USGrph     
Word              
lastS            |
42 | 41 | biimpd 211 |
. . . . . . . 8
   USGrph     
Word               lastS            |
43 | 42 | pm4.71d 639 |
. . . . . . 7
   USGrph     
Word                           lastS             |
44 | 31, 43 | bitr4d 260 |
. . . . . 6
   USGrph     
Word      ..^                      lastS                        |
45 | 44 | pm5.32da 646 |
. . . . 5
  USGrph
       Word    ..^                      lastS            Word                |
46 | 9, 45 | syl5bb 261 |
. . . 4
  USGrph
       Word   ..^                      lastS           Word                |
47 | 46 | ex 436 |
. . 3
 USGrph        Word 
 ..^                      lastS           Word                 |
48 | 47 | pm5.32rd 645 |
. 2
 USGrph    Word   ..^                      lastS                 Word                     |
49 | | 3anass 988 |
. . . 4
      Word                   Word                |
50 | | ancom 452 |
. . . 4
       Word             
 
Word                    |
51 | 49, 50 | bitr2i 254 |
. . 3
   Word            
          Word               |
52 | 51 | a1i 11 |
. 2
 USGrph    Word                       Word                |
53 | 8, 48, 52 | 3bitrd 283 |
1
 USGrph    ClWWalksN    
     Word                |