Step | Hyp | Ref
| Expression |
1 | | cycliswlk 25360 |
. . . . 5
   Cycles  
  Walks     |
2 | | wlkbprop 25251 |
. . . . 5
   Walks  
    
  
    |
3 | 1, 2 | syl 17 |
. . . 4
   Cycles  
    
  
    |
4 | | iscycl 25353 |
. . . . . 6
      
   Cycles
     Paths                   |
5 | | ispth 25298 |
. . . . . . . 8
      
   Paths
     Trails      ..^                      ..^           |
6 | | istrl 25267 |
. . . . . . . . . 10
      
   Trails
    Word                 ..^                               |
7 | | fzo0to42pr 12000 |
. . . . . . . . . . . . . . . . . . 19
 ..^          |
8 | 7 | raleqi 2991 |
. . . . . . . . . . . . . . . . . 18
 
 ..^                                                        |
9 | | ralunb 3615 |
. . . . . . . . . . . . . . . . . 18
 
                             
 
                                                    |
10 | | 2wlklem 25294 |
. . . . . . . . . . . . . . . . . . 19
 
                                                                  |
11 | | 2z 10969 |
. . . . . . . . . . . . . . . . . . . 20
 |
12 | | 3z 10970 |
. . . . . . . . . . . . . . . . . . . 20
 |
13 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
14 | 13 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
15 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
16 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
17 | | 2p1e3 10733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
18 | 16, 17 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
19 | 18 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
20 | 15, 19 | preq12d 4059 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
21 | 14, 20 | eqeq12d 2466 |
. . . . . . . . . . . . . . . . . . . . 21
                      
                      |
22 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
23 | 22 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
24 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
25 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
26 | | 3p1e4 10735 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
27 | 25, 26 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
28 | 27 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
29 | 24, 28 | preq12d 4059 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
30 | 23, 29 | eqeq12d 2466 |
. . . . . . . . . . . . . . . . . . . . 21
                      
                      |
31 | 21, 30 | ralprg 4021 |
. . . . . . . . . . . . . . . . . . . 20
 
                          
                                           |
32 | 11, 12, 31 | mp2an 678 |
. . . . . . . . . . . . . . . . . . 19
 
                                                                  |
33 | 10, 32 | anbi12i 703 |
. . . . . . . . . . . . . . . . . 18
                                                    
                                                                                    |
34 | 8, 9, 33 | 3bitri 275 |
. . . . . . . . . . . . . . . . 17
 
 ..^                                                                                                           |
35 | | preq2 4052 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                 |
36 | 35 | eqcoms 2459 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 |
37 | 36 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . . . . . 22
                            
                      |
38 | 37 | anbi2d 710 |
. . . . . . . . . . . . . . . . . . . . 21
                                                 
                                           |
39 | 38 | anbi2d 710 |
. . . . . . . . . . . . . . . . . . . 20
                                                                                                                                                                                 |
40 | | 4pos 10705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
41 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
       |
42 | 40, 41 | mpbiri 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
43 | | 0nn0 10884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
44 | 42, 43 | jctil 540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             |
45 | | nvnencycllem 25371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
Word  
                                        |
46 | 44, 45 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
Word                          
              |
47 | | 1lt4 10781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
48 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
       |
49 | 47, 48 | mpbiri 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
50 | | 1nn0 10885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
51 | 49, 50 | jctil 540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             |
52 | | nvnencycllem 25371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
Word  
                                        |
53 | 51, 52 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
Word                          
              |
54 | 46, 53 | anim12d 566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
Word                                                                           |
55 | | 2lt4 10780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
56 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
       |
57 | 55, 56 | mpbiri 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
58 | | 2nn0 10886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
59 | 57, 58 | jctil 540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             |
60 | | nvnencycllem 25371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
Word  
                                        |
61 | 59, 60 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
Word                          
              |
62 | | 3lt4 10779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
63 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
       |
64 | 62, 63 | mpbiri 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
65 | | 3nn0 10887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
66 | 64, 65 | jctil 540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             |
67 | | nvnencycllem 25371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
Word  
                                        |
68 | 66, 67 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
Word                          
              |
69 | 61, 68 | anim12d 566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
Word                                                                           |
70 | 54, 69 | anim12d 566 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
Word                                                                                                                                               |
71 | 70 | adantlrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
Word        
                                                                                                                                        |
72 | 71 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     Word                                                                                           
                        
                           |
73 | | 4z 10971 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
74 | | 3re 10683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
75 | | 4re 10686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
76 | 74, 75, 62 | ltleii 9757 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
77 | | eluz2 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
78 | 12, 73, 76, 77 | mpbir3an 1190 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
79 | | 4fvwrd4 11909 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                


                        |
80 | 78, 79 | mpan 676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         



                        |
81 | | preq12 4053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                           |
82 | 81 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                       |
83 | 82 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                         |
84 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                             |
85 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                             |
86 | 84, 85 | preq12d 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                       |
87 | 86 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                         |
88 | 83, 87 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                                           |
89 | | preq12 4053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                           |
90 | 89 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                       |
91 | 90 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                         |
92 | | simprr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                             |
93 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                             |
94 | 92, 93 | preq12d 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                       |
95 | 94 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                         |
96 | 91, 95 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                                           |
97 | 88, 96 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                                                
                                              |
98 | 97 | biimpcd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                                  
                                            |
99 | 98 | reximdv 2861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                                  
 
                                            |
100 | 99 | reximdv 2861 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                  
 

                       
                     |
101 | 100 | reximdv 2861 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                                  
 


                       

                     |
102 | 101 | reximdv 2861 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                  
 



                       


                     |
103 | 72, 80, 102 | syl2im 39 |
. . . . . . . . . . . . . . . . . . . . . . 23
     Word                                                                                           
         



                     |
104 | 103 | exp41 615 |
. . . . . . . . . . . . . . . . . . . . . 22

 
Word                                                                                                    



        
               |
105 | 104 | com14 91 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                                     Word
       
         



                        |
106 | 105 | com35 93 |
. . . . . . . . . . . . . . . . . . . 20
                                                                                     Word
           
     



                        |
107 | 39, 106 | syl6bi 232 |
. . . . . . . . . . . . . . . . . . 19
                                                                                              Word
           
     



                         |
108 | 107 | com12 32 |
. . . . . . . . . . . . . . . . . 18
                                                                                           
 
Word            
     



                         |
109 | 108 | com24 90 |
. . . . . . . . . . . . . . . . 17
                                                                                              Word  
         
    




        
                |
110 | 34, 109 | sylbi 199 |
. . . . . . . . . . . . . . . 16
 
 ..^                      
           Word            
     



                         |
111 | 110 | com13 83 |
. . . . . . . . . . . . . . 15
  Word             
 ..^                                
     



                         |
112 | 111 | 3imp 1202 |
. . . . . . . . . . . . . 14
   Word  
        
 ..^                                 
     



                       |
113 | 112 | com14 91 |
. . . . . . . . . . . . 13
              
   Word             ..^                        



        
              |
114 | | fveq2 5865 |
. . . . . . . . . . . . . 14
                   |
115 | 114 | eqeq2d 2461 |
. . . . . . . . . . . . 13
                 
           |
116 | | oveq2 6298 |
. . . . . . . . . . . . . . . . 17
                   |
117 | 116 | feq2d 5715 |
. . . . . . . . . . . . . . . 16
                 
           |
118 | | oveq2 6298 |
. . . . . . . . . . . . . . . . 17
      ..^      ..^   |
119 | 118 | raleqdv 2993 |
. . . . . . . . . . . . . . . 16
      
 ..^                             ..^                          |
120 | 117, 119 | 3anbi23d 1342 |
. . . . . . . . . . . . . . 15
        Word                 ..^                           
 
Word             ..^                           |
121 | 120 | imbi1d 319 |
. . . . . . . . . . . . . 14
         Word
                ..^                            



        
         
   Word  
        
 ..^                        



        
             |
122 | 121 | imbi2d 318 |
. . . . . . . . . . . . 13
      
   Word                 ..^                            



        
          
    Word             ..^                         


                       |
123 | 113, 115,
122 | 3imtr4d 272 |
. . . . . . . . . . . 12
                  
   Word  
              ..^                            



                       |
124 | 123 | com14 91 |
. . . . . . . . . . 11
   Word  
              ..^                                         
     



                       |
125 | 124 | 2a1d 27 |
. . . . . . . . . 10
   Word  
              ..^                            
   ..^                       ..^                          



                         |
126 | 6, 125 | syl6bi 232 |
. . . . . . . . 9
      
   Trails
    
 ..^                       ..^      
            
       


                          |
127 | 126 | 3impd 1223 |
. . . . . . . 8
      
    Trails      ..^                      ..^       
            
       


                        |
128 | 5, 127 | sylbid 219 |
. . . . . . 7
      
   Paths
                     



                        |
129 | 128 | impd 433 |
. . . . . 6
      
    Paths                
    




        
              |
130 | 4, 129 | sylbid 219 |
. . . . 5
      
   Cycles
        



                       |
131 | 130 | 3adant1 1026 |
. . . 4
      
   
   Cycles
        



                       |
132 | 3, 131 | mpcom 37 |
. . 3
   Cycles  
       


                      |
133 | 132 | com12 32 |
. 2

   Cycles
        


                      |
134 | 133 | 3imp 1202 |
1
    Cycles
        


                    |