Step | Hyp | Ref
| Expression |
1 | | cycliswlk 23669 |
. . 3
   Cycles  
  Walks     |
2 | | wlkbprop 23584 |
. . . 4
   Walks  
    
  
    |
3 | | iscycl 23662 |
. . . . . 6
      
   Cycles
     Paths                   |
4 | 3 | 3adant1 1006 |
. . . . 5
      
   
   Cycles
     Paths                   |
5 | | pthistrl 23622 |
. . . . . . . 8
   Paths  
  Trails     |
6 | | trliswlk 23589 |
. . . . . . . 8
   Trails  
  Walks     |
7 | 5, 6 | syl 16 |
. . . . . . 7
   Paths  
  Walks     |
8 | | usgrnloop 23613 |
. . . . . . . . . . 11
  USGrph
  Walks   
  ..^                  |
9 | | nne 2653 |
. . . . . . . . . . . . . . . 16
           |
10 | | 0z 10767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
11 | | 1z 10786 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
12 | | 0lt1 9972 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
13 | | fzolb 11674 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  ..^     |
14 | 10, 11, 12, 13 | mpbir3an 1170 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 ..^  |
15 | | oveq2 6207 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      ..^      ..^   |
16 | 14, 15 | syl5eleqr 2549 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      ..^       |
17 | 16 | anim2i 569 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ..^                    
 
 ..^                 ..^        |
18 | 17 | ex 434 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 ..^               
    
 
 ..^                 ..^         |
19 | 18 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^                             ..^                 ..^         |
20 | 19 | impcom 430 |
. . . . . . . . . . . . . . . . . . . 20
         ..^                         ..^                 ..^        |
21 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
22 | | oveq1 6206 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
23 | 22 | fveq2d 5802 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
24 | 21, 23 | neeq12d 2730 |
. . . . . . . . . . . . . . . . . . . . 21
           
             |
25 | 24 | rspccva 3176 |
. . . . . . . . . . . . . . . . . . . 20
    ..^                 ..^                  |
26 | 20, 25 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
         ..^                                  |
27 | | 0p1e1 10543 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
28 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
      |
29 | 28 | eqcoms 2466 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
30 | 27, 29 | syl5eq 2507 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
31 | 30 | fveq2d 5802 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
32 | 31 | neeq2d 2729 |
. . . . . . . . . . . . . . . . . . . 20
               
               |
33 | | df-ne 2649 |
. . . . . . . . . . . . . . . . . . . 20
            
              |
34 | 32, 33 | syl6bb 261 |
. . . . . . . . . . . . . . . . . . 19
               
               |
35 | 26, 34 | syl5ibcom 220 |
. . . . . . . . . . . . . . . . . 18
         ..^                                          |
36 | 35 | ex 434 |
. . . . . . . . . . . . . . . . 17
         ..^                                          |
37 | 36 | pm2.43a 49 |
. . . . . . . . . . . . . . . 16
         ..^                                    |
38 | 9, 37 | sylbi 195 |
. . . . . . . . . . . . . . 15
         ..^                                    |
39 | 38 | com12 31 |
. . . . . . . . . . . . . 14
    ..^                         
               |
40 | 39 | con4d 105 |
. . . . . . . . . . . . 13
    ..^                                         |
41 | 40 | ex 434 |
. . . . . . . . . . . 12
 
 ..^               
                          |
42 | 41 | com23 78 |
. . . . . . . . . . 11
 
 ..^               
            
             |
43 | 8, 42 | syl 16 |
. . . . . . . . . 10
  USGrph
  Walks   
            
             |
44 | 43 | ex 434 |
. . . . . . . . 9
 USGrph    Walks                              |
45 | 44 | com14 88 |
. . . . . . . 8
    
   Walks
                USGrph          |
46 | 45 | 3ad2ant1 1009 |
. . . . . . 7
      
   
   Walks
                USGrph          |
47 | 7, 46 | syl5 32 |
. . . . . 6
      
   
   Paths
                USGrph          |
48 | 47 | impd 431 |
. . . . 5
      
   
    Paths                 USGrph
        |
49 | 4, 48 | sylbid 215 |
. . . 4
      
   
   Cycles
   USGrph         |
50 | 2, 49 | syl 16 |
. . 3
   Walks  
   Cycles
   USGrph         |
51 | 1, 50 | mpcom 36 |
. 2
   Cycles  
 USGrph        |
52 | 51 | impcom 430 |
1
  USGrph
  Cycles   
      |