Step | Hyp | Ref
| Expression |
1 | | df-cycl 23557 |
. . . 4
Cycles          Paths                   |
2 | 1 | brovmpt2ex 6843 |
. . 3
   Cycles  
 
 
    |
3 | | iscycl 23648 |
. . . 4
      
   Cycles
     Paths                   |
4 | | pthistrl 23608 |
. . . . . . . . . . . 12
   Paths  
  Trails     |
5 | | trliswlk 23575 |
. . . . . . . . . . . 12
   Trails  
  Walks     |
6 | | 2mwlk 23564 |
. . . . . . . . . . . 12
   Walks  
 Word                |
7 | | lennncl 12354 |
. . . . . . . . . . . . . . . 16
  Word
       |
8 | | df-f1 5523 |
. . . . . . . . . . . . . . . . . . . . . . 23
            
                 |
9 | | nnne0 10457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
      |
10 | 9 | necomd 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
      |
11 | 10 | neneqd 2651 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
      |
12 | 11 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                  
      |
13 | | simpr 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                 |
14 | | nnnn0 10689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
      |
15 | | 0nn0 10697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
  |
17 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
      |
18 | | nn0ge0 10708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
      |
19 | | elfz2nn0 11583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        

   
       |
20 | 16, 17, 18, 19 | syl3anbrc 1172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
          |
21 | | nn0re 10691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
      |
22 | 21 | leidd 10009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
   
      |
23 | | elfz2nn0 11583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                     
           |
24 | 17, 17, 22, 23 | syl3anbrc 1172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
              |
25 | 20, 24 | jca 532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
                        |
26 | 14, 25 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
                        |
27 | 26 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                           |
28 | | f1fveq 6076 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                         |
29 | 13, 27, 28 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                       |
30 | 12, 29 | mtbird 301 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                  
              |
31 | 30 | expcom 435 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 |
32 | 8, 31 | sylbir 213 |
. . . . . . . . . . . . . . . . . . . . . 22
                                    |
33 | 32 | expcom 435 |
. . . . . . . . . . . . . . . . . . . . 21
 
                                  |
34 | 33 | com13 80 |
. . . . . . . . . . . . . . . . . . . 20
    
             
                 |
35 | 34 | imp 429 |
. . . . . . . . . . . . . . . . . . 19
                    
               |
36 | 35 | con2d 115 |
. . . . . . . . . . . . . . . . . 18
                               
    |
37 | 36 | ex 434 |
. . . . . . . . . . . . . . . . 17
    
                               |
38 | 37 | com23 78 |
. . . . . . . . . . . . . . . 16
    
            
                  |
39 | 7, 38 | syl 16 |
. . . . . . . . . . . . . . 15
  Word
                          
     |
40 | 39 | ex 434 |
. . . . . . . . . . . . . 14
 Word
                                 |
41 | 40 | com24 87 |
. . . . . . . . . . . . 13
 Word
                                 |
42 | 41 | imp 429 |
. . . . . . . . . . . 12
  Word                           
     |
43 | 4, 5, 6, 42 | 4syl 21 |
. . . . . . . . . . 11
   Paths  
            

     |
44 | 43 | imp 429 |
. . . . . . . . . 10
    Paths                
    |
45 | 44 | adantl 466 |
. . . . . . . . 9
   


     Paths                      |
46 | 45 | imp 429 |
. . . . . . . 8
      
     Paths                     |
47 | 46 | intnand 907 |
. . . . . . 7
      
     Paths                     Trails       |
48 | | isspth 23605 |
. . . . . . . . 9
      
   SPaths
     Trails        |
49 | 48 | adantr 465 |
. . . . . . . 8
   


     Paths                    SPaths  
   Trails
       |
50 | 49 | adantr 465 |
. . . . . . 7
      
     Paths                     SPaths  
   Trails
       |
51 | 47, 50 | mtbird 301 |
. . . . . 6
      
     Paths                    SPaths     |
52 | 51 | ex 434 |
. . . . 5
   


     Paths                    SPaths      |
53 | 52 | ex 434 |
. . . 4
      
    Paths                
  SPaths
      |
54 | 3, 53 | sylbid 215 |
. . 3
      
   Cycles
  
  SPaths       |
55 | 2, 54 | mpcom 36 |
. 2
   Cycles  

  SPaths
     |
56 | 55 | com12 31 |
1

   Cycles
 
  SPaths      |