Proof of Theorem numclwlk2lem2f
Step | Hyp | Ref
| Expression |
1 | | nnnn0 10905 |
. . . . . . . . . 10
   |
2 | | 2nn0 10915 |
. . . . . . . . . . 11
 |
3 | 2 | a1i 11 |
. . . . . . . . . 10
   |
4 | 1, 3 | nn0addcld 10958 |
. . . . . . . . 9
 
   |
5 | 4 | anim2i 577 |
. . . . . . . 8
 
       |
6 | 5 | 3adant1 1032 |
. . . . . . 7
  FriendGrph
 

    |
7 | | numclwwlk.c |
. . . . . . . . 9
   ClWWalksN       |
8 | | numclwwlk.f |
. . . . . . . . 9
 

           |
9 | | numclwwlk.g |
. . . . . . . . 9
 
                 
          |
10 | | numclwwlk.q |
. . . . . . . . 9
 

  WWalksN
         lastS       |
11 | | numclwwlk.h |
. . . . . . . . 9
 

                       |
12 | 7, 8, 9, 10, 11 | numclwwlkovh 25878 |
. . . . . . . 8
  
            
           
           |
13 | 12 | eleq2d 2525 |
. . . . . . 7
  
             
           
            |
14 | 6, 13 | syl 17 |
. . . . . 6
  FriendGrph
       
                             |
15 | | fveq1 5887 |
. . . . . . . . 9
           |
16 | 15 | eqeq1d 2464 |
. . . . . . . 8
     
       |
17 | | fveq1 5887 |
. . . . . . . . 9
     
             |
18 | 17, 15 | neeq12d 2697 |
. . . . . . . 8
             
               |
19 | 16, 18 | anbi12d 722 |
. . . . . . 7
                                         |
20 | 19 | elrab 3208 |
. . . . . 6
     
           
                                     |
21 | 14, 20 | syl6bb 269 |
. . . . 5
  FriendGrph
       
    
           
            |
22 | 4 | 3ad2ant3 1037 |
. . . . . . . 8
  FriendGrph
 
   |
23 | 7 | numclwwlkfvc 25854 |
. . . . . . . . 9
  
        ClWWalksN         |
24 | 23 | eleq2d 2525 |
. . . . . . . 8
  
    
 
  ClWWalksN          |
25 | 22, 24 | syl 17 |
. . . . . . 7
  FriendGrph
       
  ClWWalksN          |
26 | 25 | anbi1d 716 |
. . . . . 6
  FriendGrph
                           
   ClWWalksN                             |
27 | | peano2nn 10649 |
. . . . . . . . . . . . 13
 
   |
28 | | nnz 10988 |
. . . . . . . . . . . . . . . 16
   |
29 | | 2z 10998 |
. . . . . . . . . . . . . . . . 17
 |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
31 | 28, 30 | zaddcld 11073 |
. . . . . . . . . . . . . . 15
 
   |
32 | | uzid 11202 |
. . . . . . . . . . . . . . 15
   
    
    |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
 
    
    |
34 | | nncn 10645 |
. . . . . . . . . . . . . . . . 17
   |
35 | | 1cnd 9685 |
. . . . . . . . . . . . . . . . 17
   |
36 | 34, 35, 35 | addassd 9691 |
. . . . . . . . . . . . . . . 16
           |
37 | | 1p1e2 10751 |
. . . . . . . . . . . . . . . . . 18
   |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . 17
     |
39 | 38 | oveq2d 6331 |
. . . . . . . . . . . . . . . 16
 
       |
40 | 36, 39 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
         |
41 | 40 | fveq2d 5892 |
. . . . . . . . . . . . . 14
                 |
42 | 33, 41 | eleqtrrd 2543 |
. . . . . . . . . . . . 13
 
           |
43 | 27, 42 | jca 539 |
. . . . . . . . . . . 12
    
            |
44 | 43 | 3ad2ant3 1037 |
. . . . . . . . . . 11
  FriendGrph
    
            |
45 | 44 | adantr 471 |
. . . . . . . . . 10
   FriendGrph
    ClWWalksN
                             
            |
46 | | simprl 769 |
. . . . . . . . . 10
   FriendGrph
    ClWWalksN
                            ClWWalksN         |
47 | | wwlksubclwwlk 25581 |
. . . . . . . . . 10
    
             ClWWalksN
       substr      
  WWalksN
           |
48 | 45, 46, 47 | sylc 62 |
. . . . . . . . 9
   FriendGrph
    ClWWalksN
                           substr      
  WWalksN
          |
49 | | pncan1 10071 |
. . . . . . . . . . . . . . 15
       |
50 | 49 | eqcomd 2468 |
. . . . . . . . . . . . . 14
       |
51 | 34, 50 | syl 17 |
. . . . . . . . . . . . 13
       |
52 | 51 | fveq2d 5892 |
. . . . . . . . . . . 12
   WWalksN
      WWalksN
          |
53 | 52 | eleq2d 2525 |
. . . . . . . . . . 11
   substr
        WWalksN
   
 substr         WWalksN            |
54 | 53 | 3ad2ant3 1037 |
. . . . . . . . . 10
  FriendGrph
   substr
        WWalksN
   
 substr         WWalksN            |
55 | 54 | adantr 471 |
. . . . . . . . 9
   FriendGrph
    ClWWalksN
                            substr
        WWalksN
   
 substr         WWalksN            |
56 | 48, 55 | mpbird 240 |
. . . . . . . 8
   FriendGrph
    ClWWalksN
                           substr      
  WWalksN
      |
57 | | clwwlknprop 25549 |
. . . . . . . . . . . . 13
   ClWWalksN    
 
 
 Word   
          |
58 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . 20
          Word 

                           |
59 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
Word  
Word   |
60 | | peano2nn0 10939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

    |
61 | 1, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   |
62 | | nnre 10644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
63 | 62 | lep1d 10566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
64 | | elfz2nn0 11914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      
  
     |
65 | 1, 61, 63, 64 | syl3anbrc 1198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
    |
66 | | 2cnd 10710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
67 | | addsubass 9911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
           |
68 | | 2m1e1 10752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   |
69 | 68 | oveq2i 6326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
70 | 67, 69 | syl6eq 2512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
         |
71 | 34, 66, 35, 70 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
72 | 71 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            
    |
73 | 65, 72 | eleqtrrd 2543 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
74 | | elfzp1b 11900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  
                      |
75 | 28, 31, 74 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
       
     
     |
76 | 73, 75 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
         |
77 | 76 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        
Word  
     
    |
78 | | oveq2 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                       |
79 | 78 | eleq2d 2525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 
     
     |
80 | 79 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        
Word  
 
        
     
     |
81 | 77, 80 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
Word  
            |
82 | | swrd0fv0 12833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  Word 
            substr                |
83 | 59, 81, 82 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
Word  
  substr                |
84 | 83 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
Word    substr                 |
85 | 84 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
         Word 
  substr                 |
86 | 85 | impcom 436 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
Word  
    substr
               |
87 | 86 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . 22
               Word  
 
    
    
         
  substr                |
88 | | simpl 463 |
. . . . . . . . . . . . . . . . . . . . . 22
               Word  
 
    
    
         
      |
89 | 87, 88 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . 21
               Word  
 
    
    
         
  substr            |
90 | | swrd0fvlsw 12836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  Word 
          lastS   substr                  |
91 | 59, 81, 90 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        
Word  
lastS   substr                  |
92 | 34, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
93 | 34, 66 | pncand 10013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
94 | 92, 93 | eqtr4d 2499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           |
95 | 94 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
             |
96 | 95 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        
Word  
                  |
97 | 91, 96 | eqtr2d 2497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        
Word  
        lastS   substr          |
98 | 97 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        
Word          lastS   substr           |
99 | 98 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
         Word 
        lastS   substr           |
100 | 99 | impcom 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
Word  
      
   lastS   substr          |
101 | 100 | neeq1d 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
Word  
              
lastS   substr               |
102 | 101 | biimpcd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                      Word 

  lastS   substr               |
103 | 102 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           
Word  
  lastS   substr               |
104 | 103 | impcom 436 |
. . . . . . . . . . . . . . . . . . . . . . 23
          Word 

                     lastS   substr              |
105 | 104 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
               Word  
 
    
    
         
lastS   substr              |
106 | | neeq2 2699 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      lastS   substr       
lastS   substr               |
107 | 106 | eqcoms 2470 |
. . . . . . . . . . . . . . . . . . . . . . 23
      lastS   substr       
lastS   substr               |
108 | 107 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
               Word  
 
    
    
         
 lastS   substr       
lastS   substr               |
109 | 105, 108 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . 21
               Word  
 
    
    
         
lastS   substr          |
110 | 89, 109 | jca 539 |
. . . . . . . . . . . . . . . . . . . 20
               Word  
 
    
    
         
   substr
         lastS   substr           |
111 | 58, 110 | mpancom 680 |
. . . . . . . . . . . . . . . . . . 19
          Word 

                        substr          lastS   substr           |
112 | 111 | exp31 613 |
. . . . . . . . . . . . . . . . . 18
       
Word                       
   substr
         lastS   substr             |
113 | 112 | com23 81 |
. . . . . . . . . . . . . . . . 17
       
Word                      
    substr          lastS   substr             |
114 | 113 | ex 440 |
. . . . . . . . . . . . . . . 16
        Word
                  
 
    substr         
lastS   substr              |
115 | 114 | adantl 472 |
. . . . . . . . . . . . . . 15
            Word                     
    substr          lastS   substr              |
116 | 115 | impcom 436 |
. . . . . . . . . . . . . 14
  Word           
                         substr          lastS   substr             |
117 | 116 | 3adant1 1032 |
. . . . . . . . . . . . 13
   
Word           
                         substr          lastS   substr             |
118 | 57, 117 | syl 17 |
. . . . . . . . . . . 12
   ClWWalksN    
 
                         substr          lastS   substr             |
119 | 118 | imp 435 |
. . . . . . . . . . 11
    ClWWalksN    
           
               substr          lastS   substr            |
120 | 119 | com12 32 |
. . . . . . . . . 10
 
     ClWWalksN                             substr          lastS   substr            |
121 | 120 | 3adant1 1032 |
. . . . . . . . 9
  FriendGrph
     ClWWalksN
                        
   substr
         lastS   substr            |
122 | 121 | imp 435 |
. . . . . . . 8
   FriendGrph
    ClWWalksN
                             substr          lastS   substr           |
123 | 56, 122 | jca 539 |
. . . . . . 7
   FriendGrph
    ClWWalksN
                            substr
        WWalksN
       substr          lastS   substr            |
124 | 123 | ex 440 |
. . . . . 6
  FriendGrph
     ClWWalksN
                        
  substr      
  WWalksN
       substr          lastS   substr             |
125 | 26, 124 | sylbid 223 |
. . . . 5
  FriendGrph
                              substr         WWalksN        substr         
lastS   substr             |
126 | 21, 125 | sylbid 223 |
. . . 4
  FriendGrph
          substr         WWalksN        substr         
lastS   substr             |
127 | 126 | imp 435 |
. . 3
   FriendGrph

         substr         WWalksN    
   substr
         lastS   substr            |
128 | 1 | anim2i 577 |
. . . . . . . 8
 
 
   |
129 | 128 | 3adant1 1032 |
. . . . . . 7
  FriendGrph
 
   |
130 | 129 | adantr 471 |
. . . . . 6
   FriendGrph

           |
131 | 7, 8, 9, 10 | numclwwlkovq 25876 |
. . . . . 6
 
        WWalksN          lastS       |
132 | 130, 131 | syl 17 |
. . . . 5
   FriendGrph

              WWalksN          lastS       |
133 | 132 | eleq2d 2525 |
. . . 4
   FriendGrph

         substr          
 substr          WWalksN          lastS        |
134 | | fveq1 5887 |
. . . . . . 7
  substr             substr            |
135 | 134 | eqeq1d 2464 |
. . . . . 6
  substr              substr             |
136 | | fveq2 5888 |
. . . . . . 7
  substr       lastS  
lastS   substr          |
137 | 136 | neeq1d 2695 |
. . . . . 6
  substr        lastS  
lastS   substr           |
138 | 135, 137 | anbi12d 722 |
. . . . 5
  substr             lastS       substr         
lastS   substr            |
139 | 138 | elrab 3208 |
. . . 4
  substr      
   WWalksN          lastS       substr         WWalksN    
   substr
         lastS   substr            |
140 | 133, 139 | syl6bb 269 |
. . 3
   FriendGrph

         substr          
  substr      
  WWalksN
       substr          lastS   substr             |
141 | 127, 140 | mpbird 240 |
. 2
   FriendGrph

        substr             |
142 | | numclwwlk.r |
. 2
        substr         |
143 | 141, 142 | fmptd 6069 |
1
  FriendGrph
                 |