Proof of Theorem eupath2lem3
Step | Hyp | Ref
| Expression |
1 | | imaundi 5270 |
. . . . . . . . . . 11
                                 |
2 | | 1z 11001 |
. . . . . . . . . . . . 13
 |
3 | | eupath2.5 |
. . . . . . . . . . . . . 14
   |
4 | | nn0uz 11227 |
. . . . . . . . . . . . . . 15
     |
5 | | 1m1e0 10711 |
. . . . . . . . . . . . . . . 16
   |
6 | 5 | fveq2i 5895 |
. . . . . . . . . . . . . . 15
           |
7 | 4, 6 | eqtr4i 2487 |
. . . . . . . . . . . . . 14
       |
8 | 3, 7 | syl6eleq 2550 |
. . . . . . . . . . . . 13
         |
9 | | fzsuc2 11888 |
. . . . . . . . . . . . 13
 
          
              |
10 | 2, 8, 9 | sylancr 674 |
. . . . . . . . . . . 12
    
              |
11 | 10 | imaeq2d 5190 |
. . . . . . . . . . 11
                           |
12 | | eupath2.3 |
. . . . . . . . . . . . . . 15
   EulPaths     |
13 | | eupath2.1 |
. . . . . . . . . . . . . . 15
   |
14 | | eupaf1o 25754 |
. . . . . . . . . . . . . . 15
    EulPaths                  |
15 | 12, 13, 14 | syl2anc 671 |
. . . . . . . . . . . . . 14
               |
16 | | f1ofn 5842 |
. . . . . . . . . . . . . 14
            
          |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
           |
18 | | eupath2.6 |
. . . . . . . . . . . . . 14
  
      |
19 | | nn0p1nn 10943 |
. . . . . . . . . . . . . . . . 17

    |
20 | 3, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
     |
21 | | nnuz 11228 |
. . . . . . . . . . . . . . . 16
     |
22 | 20, 21 | syl6eleq 2550 |
. . . . . . . . . . . . . . 15
         |
23 | | eupacl 25753 |
. . . . . . . . . . . . . . . . 17
   EulPaths
        |
24 | 12, 23 | syl 17 |
. . . . . . . . . . . . . . . 16
       |
25 | 24 | nn0zd 11072 |
. . . . . . . . . . . . . . 15
       |
26 | | elfz5 11827 |
. . . . . . . . . . . . . . 15
                       
         |
27 | 22, 25, 26 | syl2anc 671 |
. . . . . . . . . . . . . 14
           
         |
28 | 18, 27 | mpbird 240 |
. . . . . . . . . . . . 13
             |
29 | | fnsnfv 5953 |
. . . . . . . . . . . . 13
          
              
             |
30 | 17, 28, 29 | syl2anc 671 |
. . . . . . . . . . . 12
     
             |
31 | 30 | uneq2d 3600 |
. . . . . . . . . . 11
              
                        |
32 | 1, 11, 31 | 3eqtr4a 2522 |
. . . . . . . . . 10
                        
      |
33 | 32 | reseq2d 5127 |
. . . . . . . . 9
                           
       |
34 | | resundi 5140 |
. . . . . . . . 9
              
                     
      |
35 | 33, 34 | syl6eq 2512 |
. . . . . . . 8
                             
       |
36 | | f1of 5841 |
. . . . . . . . . . . . 13
            
              |
37 | 15, 36 | syl 17 |
. . . . . . . . . . . 12
               |
38 | 37, 28 | ffvelrnd 6051 |
. . . . . . . . . . 11
    
    |
39 | | fnressn 6105 |
. . . . . . . . . . 11
                        
         
       |
40 | 13, 38, 39 | syl2anc 671 |
. . . . . . . . . 10
                
         
       |
41 | | eupaseg 25757 |
. . . . . . . . . . . . . 14
    EulPaths             
      
                      |
42 | 12, 28, 41 | syl2anc 671 |
. . . . . . . . . . . . 13
                        
     |
43 | 3 | nn0cnd 10961 |
. . . . . . . . . . . . . . . 16
   |
44 | | ax-1cn 9628 |
. . . . . . . . . . . . . . . 16
 |
45 | | pncan 9912 |
. . . . . . . . . . . . . . . 16
 
       |
46 | 43, 44, 45 | sylancl 673 |
. . . . . . . . . . . . . . 15
       |
47 | 46 | fveq2d 5896 |
. . . . . . . . . . . . . 14
               |
48 | 47 | preq1d 4070 |
. . . . . . . . . . . . 13
                           
     |
49 | 42, 48 | eqtrd 2496 |
. . . . . . . . . . . 12
                    
     |
50 | 49 | opeq2d 4187 |
. . . . . . . . . . 11
     
         
        
                   |
51 | 50 | sneqd 3992 |
. . . . . . . . . 10
      
                                 
       |
52 | 40, 51 | eqtrd 2496 |
. . . . . . . . 9
                
            
       |
53 | 52 | uneq2d 3600 |
. . . . . . . 8
                 
      
              
                     |
54 | 35, 53 | eqtrd 2496 |
. . . . . . 7
                                          
        |
55 | 54 | oveq2d 6336 |
. . . . . 6
  VDeg               VDeg                              
         |
56 | 55 | fveq1d 5894 |
. . . . 5
   VDeg        
          VDeg                              
            |
57 | | imassrn 5201 |
. . . . . . . 8
         |
58 | | f1ofo 5848 |
. . . . . . . . 9
            
              |
59 | | forn 5823 |
. . . . . . . . 9
               |
60 | 15, 58, 59 | 3syl 18 |
. . . . . . . 8
   |
61 | 57, 60 | syl5sseq 3492 |
. . . . . . 7
           |
62 | | fnssres 5715 |
. . . . . . 7
                               |
63 | 13, 61, 62 | syl2anc 671 |
. . . . . 6
                     |
64 | | fvex 5902 |
. . . . . . . 8
       |
65 | | prex 4659 |
. . . . . . . 8
         
    |
66 | 64, 65 | fnsn 5658 |
. . . . . . 7
                  
         
    |
67 | 66 | a1i 11 |
. . . . . 6
      
                            |
68 | | eupafi 25755 |
. . . . . . . 8
    EulPaths      |
69 | 12, 13, 68 | syl2anc 671 |
. . . . . . 7
   |
70 | | ssfi 7823 |
. . . . . . 7
                     |
71 | 69, 61, 70 | syl2anc 671 |
. . . . . 6
           |
72 | | snfi 7681 |
. . . . . . 7
         |
73 | 72 | a1i 11 |
. . . . . 6
     
     |
74 | 3 | nn0red 10960 |
. . . . . . . . . 10
   |
75 | 74 | ltp1d 10570 |
. . . . . . . . 9
     |
76 | | peano2re 9837 |
. . . . . . . . . . 11
 
   |
77 | 74, 76 | syl 17 |
. . . . . . . . . 10
     |
78 | 74, 77 | ltnled 9813 |
. . . . . . . . 9
  
  
   |
79 | 75, 78 | mpbid 215 |
. . . . . . . 8
     |
80 | | f1of1 5840 |
. . . . . . . . . . 11
            
              |
81 | 15, 80 | syl 17 |
. . . . . . . . . 10
               |
82 | 3 | nn0zd 11072 |
. . . . . . . . . . . 12
   |
83 | 82 | peano2zd 11077 |
. . . . . . . . . . . . 13
     |
84 | | eluz2 11199 |
. . . . . . . . . . . . 13
                  

       |
85 | 83, 25, 18, 84 | syl3anbrc 1198 |
. . . . . . . . . . . 12
        
    |
86 | | peano2uzr 11248 |
. . . . . . . . . . . 12
         
             |
87 | 82, 85, 86 | syl2anc 671 |
. . . . . . . . . . 11
           |
88 | | fzss2 11873 |
. . . . . . . . . . 11
            
          |
89 | 87, 88 | syl 17 |
. . . . . . . . . 10
    
          |
90 | | f1elima 6194 |
. . . . . . . . . 10
              
                     
              
         |
91 | 81, 28, 89, 90 | syl3anc 1276 |
. . . . . . . . 9
     
                   |
92 | | elfz5 11827 |
. . . . . . . . . 10
               
     |
93 | 22, 82, 92 | syl2anc 671 |
. . . . . . . . 9
         
   |
94 | 91, 93 | bitrd 261 |
. . . . . . . 8
     
           
   |
95 | 79, 94 | mtbird 307 |
. . . . . . 7
    
            |
96 | | disjsn 4044 |
. . . . . . 7
                  
                |
97 | 95, 96 | sylibr 217 |
. . . . . 6
              
      |
98 | | eupagra 25750 |
. . . . . . 7
   EulPaths
  UMGrph
  |
99 | | umgrares 25107 |
. . . . . . 7
 UMGrph UMGrph
            |
100 | 12, 98, 99 | 3syl 18 |
. . . . . 6
 UMGrph             |
101 | | relumgra 25097 |
. . . . . . . . 9
UMGrph |
102 | 101 | brrelexi 4897 |
. . . . . . . 8
 UMGrph   |
103 | 12, 98, 102 | 3syl 18 |
. . . . . . 7
   |
104 | | eupapf 25756 |
. . . . . . . . 9
   EulPaths
                |
105 | 12, 104 | syl 17 |
. . . . . . . 8
               |
106 | 3, 4 | syl6eleq 2550 |
. . . . . . . . 9
       |
107 | | elfzuzb 11829 |
. . . . . . . . 9
        
                |
108 | 106, 87, 107 | sylanbrc 675 |
. . . . . . . 8
           |
109 | 105, 108 | ffvelrnd 6051 |
. . . . . . 7
       |
110 | | peano2nn0 10944 |
. . . . . . . . . . . 12

    |
111 | 3, 110 | syl 17 |
. . . . . . . . . . 11
     |
112 | 111, 4 | syl6eleq 2550 |
. . . . . . . . . 10
         |
113 | | elfz5 11827 |
. . . . . . . . . 10
                       
         |
114 | 112, 25, 113 | syl2anc 671 |
. . . . . . . . 9
           
         |
115 | 18, 114 | mpbird 240 |
. . . . . . . 8
             |
116 | 105, 115 | ffvelrnd 6051 |
. . . . . . 7
    
    |
117 | | umgra1 25109 |
. . . . . . 7
      
                UMGrph      
                    |
118 | 103, 38, 109, 116, 117 | syl22anc 1277 |
. . . . . 6
 UMGrph      
                    |
119 | | eupath2.7 |
. . . . . 6
   |
120 | 63, 67, 71, 73, 97, 100, 118, 119 | vdgrfiun 25686 |
. . . . 5
   VDeg                              
             VDeg                 VDeg                   
            |
121 | 56, 120 | eqtrd 2496 |
. . . 4
   VDeg        
           VDeg                 VDeg      
                         |
122 | 121 | breq2d 4430 |
. . 3
    VDeg
                   VDeg                 VDeg      
            
             |
123 | 122 | notbid 300 |
. 2
    VDeg        
       
   VDeg                 VDeg      
                          |
124 | | fveq2 5892 |
. . . . . . . . . 10
   VDeg
                VDeg                 |
125 | 124 | breq2d 4430 |
. . . . . . . . 9
 
  VDeg                 VDeg                  |
126 | 125 | notbid 300 |
. . . . . . . 8
 
  VDeg              
  VDeg                  |
127 | 126 | elrab3 3209 |
. . . . . . 7
 

  VDeg               
  VDeg                  |
128 | 119, 127 | syl 17 |
. . . . . 6
  
  VDeg               
  VDeg                  |
129 | | eupath2.8 |
. . . . . . 7
    VDeg
                                         |
130 | 129 | eleq2d 2525 |
. . . . . 6
  
  VDeg               
                           |
131 | 128, 130 | bitr3d 263 |
. . . . 5
    VDeg              
                           |
132 | 131 | adantr 471 |
. . . 4
 
          
   VDeg                                          |
133 | | 2z 11003 |
. . . . . . . 8
 |
134 | 133 | a1i 11 |
. . . . . . 7
 
          
  |
135 | | vdgrfif 25683 |
. . . . . . . . . . 11
  
                           VDeg                  |
136 | 103, 63, 71, 135 | syl3anc 1276 |
. . . . . . . . . 10
  VDeg                  |
137 | 136, 119 | ffvelrnd 6051 |
. . . . . . . . 9
   VDeg                 |
138 | 137 | nn0zd 11072 |
. . . . . . . 8
   VDeg                 |
139 | 138 | adantr 471 |
. . . . . . 7
 
          
  VDeg                 |
140 | | vdgrfif 25683 |
. . . . . . . . . . 11
       
            
                       VDeg
                  
            |
141 | 103, 67, 73, 140 | syl3anc 1276 |
. . . . . . . . . 10
  VDeg                   
            |
142 | 141, 119 | ffvelrnd 6051 |
. . . . . . . . 9
   VDeg      
            
           |
143 | 142 | nn0zd 11072 |
. . . . . . . 8
   VDeg      
            
           |
144 | 143 | adantr 471 |
. . . . . . 7
 
          
  VDeg      
                        |
145 | | iddvds 14371 |
. . . . . . . . . 10
   |
146 | 133, 145 | ax-mp 5 |
. . . . . . . . 9
 |
147 | | simpr 467 |
. . . . . . . . . . . . . . . 16
          
              |
148 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
          
                    |
149 | 148, 147 | eqtr3d 2498 |
. . . . . . . . . . . . . . . 16
          
           
    |
150 | 147, 149 | preq12d 4072 |
. . . . . . . . . . . . . . 15
          
                          |
151 | | dfsn2 3993 |
. . . . . . . . . . . . . . 15
 
    |
152 | 150, 151 | syl6eqr 2514 |
. . . . . . . . . . . . . 14
          
                         |
153 | 152 | opeq2d 4187 |
. . . . . . . . . . . . 13
          
            
            
        
        |
154 | 153 | sneqd 3992 |
. . . . . . . . . . . 12
          
             
                                 |
155 | 154 | oveq2d 6336 |
. . . . . . . . . . 11
          
         VDeg
                  
       VDeg      
          |
156 | 155 | fveq1d 5894 |
. . . . . . . . . 10
          
          VDeg      
            
           VDeg      
             |
157 | 103 | ad2antrr 737 |
. . . . . . . . . . 11
          
       
  |
158 | 64 | a1i 11 |
. . . . . . . . . . 11
          
           
    |
159 | 119 | ad2antrr 737 |
. . . . . . . . . . 11
          
       
  |
160 | 157, 158,
159 | vdgr1d 25687 |
. . . . . . . . . 10
          
          VDeg      
             |
161 | 156, 160 | eqtrd 2496 |
. . . . . . . . 9
          
          VDeg      
            
           |
162 | 146, 161 | syl5breqr 4455 |
. . . . . . . 8
          
       
  VDeg      
                        |
163 | | dvds0 14373 |
. . . . . . . . . 10
   |
164 | 133, 163 | ax-mp 5 |
. . . . . . . . 9
 |
165 | 103 | ad2antrr 737 |
. . . . . . . . . 10
          
       
  |
166 | 64 | a1i 11 |
. . . . . . . . . 10
          
           
    |
167 | 119 | ad2antrr 737 |
. . . . . . . . . 10
          
       
  |
168 | 109 | ad2antrr 737 |
. . . . . . . . . 10
          
              |
169 | | simpr 467 |
. . . . . . . . . 10
          
              |
170 | 116 | ad2antrr 737 |
. . . . . . . . . 10
          
           
    |
171 | | simplr 767 |
. . . . . . . . . . 11
          
                    |
172 | 171, 169 | eqnetrrd 2704 |
. . . . . . . . . 10
          
           
    |
173 | 165, 166,
167, 168, 169, 170, 172 | vdgr1a 25690 |
. . . . . . . . 9
          
          VDeg      
            
           |
174 | 164, 173 | syl5breqr 4455 |
. . . . . . . 8
          
       
  VDeg      
                        |
175 | 162, 174 | pm2.61dane 2723 |
. . . . . . 7
 
          
  VDeg      
            
           |
176 | | dvdsadd2b 14402 |
. . . . . . 7
    VDeg                  VDeg                   
           VDeg      
            
           
  VDeg                  VDeg                   
           VDeg                   |
177 | 134, 139,
144, 175, 176 | syl112anc 1280 |
. . . . . 6
 
          
   VDeg                  VDeg                   
           VDeg                   |
178 | 142 | nn0cnd 10961 |
. . . . . . . . 9
   VDeg      
            
           |
179 | 137 | nn0cnd 10961 |
. . . . . . . . 9
   VDeg                 |
180 | 178, 179 | addcomd 9866 |
. . . . . . . 8
    VDeg      
                        VDeg                   VDeg                 VDeg      
            
            |
181 | 180 | breq2d 4430 |
. . . . . . 7
     VDeg      
            
           VDeg                   VDeg                 VDeg      
            
             |
182 | 181 | adantr 471 |
. . . . . 6
 
          
    VDeg                   
           VDeg                   VDeg                 VDeg                   
             |
183 | 177, 182 | bitrd 261 |
. . . . 5
 
          
   VDeg                  VDeg                 VDeg                   
             |
184 | 183 | notbid 300 |
. . . 4
 
          
   VDeg              
   VDeg                 VDeg                   
             |
185 | | simpr 467 |
. . . . . . 7
 
          
            |
186 | 185 | eqeq2d 2472 |
. . . . . 6
 
          
        
       
     |
187 | 185 | preq2d 4071 |
. . . . . 6
 
          
                          |
188 | 186, 187 | ifbieq2d 3918 |
. . . . 5
 
          
                                 
                    |
189 | 188 | eleq2d 2525 |
. . . 4
 
          
                        
                       
       |
190 | 132, 184,
189 | 3bitr3d 291 |
. . 3
 
          
    VDeg                 VDeg                   
                                 
       |
191 | | simpr 467 |
. . . . . . . . . . . . . 14
          
              |
192 | 191 | preq1d 4070 |
. . . . . . . . . . . . 13
          
                 
              |
193 | 192 | opeq2d 4187 |
. . . . . . . . . . . 12
          
                         
                 
      |
194 | 193 | sneqd 3992 |
. . . . . . . . . . 11
          
                          
          
    
           |
195 | 194 | oveq2d 6336 |
. . . . . . . . . 10
          
         VDeg      
                    VDeg               
        |
196 | 195 | fveq1d 5894 |
. . . . . . . . 9
          
          VDeg
                  
           VDeg      
        
           |
197 | 103 | ad2antrr 737 |
. . . . . . . . . 10
          
          |
198 | 64 | a1i 11 |
. . . . . . . . . 10
          
                |
199 | 119 | ad2antrr 737 |
. . . . . . . . . 10
          
          |
200 | 116 | ad2antrr 737 |
. . . . . . . . . 10
          
                |
201 | | simplr 767 |
. . . . . . . . . . . 12
          
               
    |
202 | 191, 201 | eqnetrrd 2704 |
. . . . . . . . . . 11
          
           
    |
203 | 202 | necomd 2691 |
. . . . . . . . . 10
          
                |
204 | 197, 198,
199, 200, 203 | vdgr1b 25688 |
. . . . . . . . 9
          
          VDeg
              
           |
205 | 196, 204 | eqtrd 2496 |
. . . . . . . 8
          
          VDeg
                  
           |
206 | 205 | oveq2d 6336 |
. . . . . . 7
          
           VDeg                 VDeg      
            
             VDeg                  |
207 | 206 | breq2d 4430 |
. . . . . 6
          
        
   VDeg
                VDeg                   
             VDeg                   |
208 | 207 | notbid 300 |
. . . . 5
          
        
   VDeg                 VDeg                   
         
   VDeg                   |
209 | | 2nn 10801 |
. . . . . . . . . . . 12
 |
210 | 209 | a1i 11 |
. . . . . . . . . . 11
   |
211 | | 1lt2 10810 |
. . . . . . . . . . . 12
 |
212 | 211 | a1i 11 |
. . . . . . . . . . 11
   |
213 | | ndvdsp1 14445 |
. . . . . . . . . . 11
    VDeg                
  VDeg              
   VDeg                   |
214 | 138, 210,
212, 213 | syl3anc 1276 |
. . . . . . . . . 10
    VDeg
             
   VDeg                   |
215 | 214 | con2d 120 |
. . . . . . . . 9
     VDeg                  VDeg                  |
216 | | n2dvds1 14409 |
. . . . . . . . . . . 12
 |
217 | | opoe 14816 |
. . . . . . . . . . . 12
     VDeg                 VDeg                      VDeg                  |
218 | 2, 216, 217 | mpanr12 696 |
. . . . . . . . . . 11
    VDeg                 VDeg                   VDeg                  |
219 | 218 | ex 440 |
. . . . . . . . . 10
   VDeg                  VDeg
             
   VDeg                   |
220 | 138, 219 | syl 17 |
. . . . . . . . 9
    VDeg              
   VDeg
                  |
221 | 215, 220 | impbid 195 |
. . . . . . . 8
     VDeg               
  VDeg                  |
222 | 221, 131 | bitrd 261 |
. . . . . . 7
     VDeg               
                           |
223 | 222 | notbid 300 |
. . . . . 6
     VDeg               
                           |
224 | 223 | ad2antrr 737 |
. . . . 5
          
        
   VDeg               
                           |
225 | | fvex 5902 |
. . . . . . 7
     |
226 | 225 | eupath2lem2 25762 |
. . . . . 6
                                         
                       
       |
227 | 226 | adantll 725 |
. . . . 5
          
        
                                               
       |
228 | 208, 224,
227 | 3bitrd 287 |
. . . 4
          
        
   VDeg                 VDeg                   
                                 
       |
229 | | simpr 467 |
. . . . . . . . . . . . . 14
          
             
    |
230 | 229 | preq2d 4071 |
. . . . . . . . . . . . 13
          
                                |
231 | 230 | opeq2d 4187 |
. . . . . . . . . . . 12
          
              
            
        
             |
232 | 231 | sneqd 3992 |
. . . . . . . . . . 11
          
               
                                      |
233 | 232 | oveq2d 6336 |
. . . . . . . . . 10
          
           VDeg
                  
       VDeg      
               |
234 | 233 | fveq1d 5894 |
. . . . . . . . 9
          
            VDeg      
            
           VDeg      
                  |
235 | 103 | ad2antrr 737 |
. . . . . . . . . 10
          
         
  |
236 | 64 | a1i 11 |
. . . . . . . . . 10
          
             
    |
237 | 119 | ad2antrr 737 |
. . . . . . . . . 10
          
         
  |
238 | 109 | ad2antrr 737 |
. . . . . . . . . 10
          
                |
239 | | simplr 767 |
. . . . . . . . . . 11
          
                      |
240 | 239, 229 | neeqtrd 2705 |
. . . . . . . . . 10
          
                |
241 | 235, 236,
237, 238, 240 | vdgr1c 25689 |
. . . . . . . . 9
          
            VDeg      
                  |
242 | 234, 241 | eqtrd 2496 |
. . . . . . . 8
          
            VDeg      
            
           |
243 | 242 | oveq2d 6336 |
. . . . . . 7
          
             VDeg                 VDeg      
                          VDeg                  |
244 | 243 | breq2d 4430 |
. . . . . 6
          
              VDeg                 VDeg      
            
             VDeg                   |
245 | 244 | notbid 300 |
. . . . 5
          
              VDeg                 VDeg      
                      
   VDeg                   |
246 | 223 | ad2antrr 737 |
. . . . 5
          
              VDeg               
                           |
247 | | necom 2689 |
. . . . . . . 8
        
 
            |
248 | | fvex 5902 |
. . . . . . . . 9
       |
249 | 248 | eupath2lem2 25762 |
. . . . . . . 8
     
                       
                 
                           |
250 | 247, 249 | sylanb 479 |
. . . . . . 7
                             
                 
                           |
251 | 250 | con1bid 336 |
. . . . . 6
                                           
                       
       |
252 | 251 | adantll 725 |
. . . . 5
          
                                  
                       
       |
253 | 245, 246,
252 | 3bitrd 287 |
. . . 4
          
              VDeg                 VDeg      
                      
                       
       |
254 | 103 | ad2antrr 737 |
. . . . . . . . . 10
          
                  |
255 | 64 | a1i 11 |
. . . . . . . . . 10
          
                   
    |
256 | 119 | ad2antrr 737 |
. . . . . . . . . 10
          
                  |
257 | 109 | ad2antrr 737 |
. . . . . . . . . 10
          
                      |
258 | | simprl 769 |
. . . . . . . . . 10
          
                      |
259 | 116 | ad2antrr 737 |
. . . . . . . . . 10
          
                   
    |
260 | | simprr 771 |
. . . . . . . . . 10
          
                   
    |
261 | 254, 255,
256, 257, 258, 259, 260 | vdgr1a 25690 |
. . . . . . . . 9
          
                  VDeg      
                        |
262 | 261 | oveq2d 6336 |
. . . . . . . 8
          
                   VDeg                 VDeg                   
             VDeg                  |
263 | 179 | addid1d 9864 |
. . . . . . . . 9
    VDeg                  VDeg                 |
264 | 263 | ad2antrr 737 |
. . . . . . . 8
          
                   VDeg                  VDeg                 |
265 | 262, 264 | eqtrd 2496 |
. . . . . . 7
          
                   VDeg                 VDeg                   
            VDeg                 |
266 | 265 | breq2d 4430 |
. . . . . 6
          
                    VDeg                 VDeg      
                      
  VDeg                  |
267 | 266 | notbid 300 |
. . . . 5
          
                    VDeg                 VDeg      
                      
  VDeg                  |
268 | 131 | ad2antrr 737 |
. . . . 5
          
                   VDeg              
                           |
269 | 258 | necomd 2691 |
. . . . . . . . . 10
          
                      |
270 | 260 | necomd 2691 |
. . . . . . . . . 10
          
                        |
271 | 269, 270 | 2thd 248 |
. . . . . . . . 9
          
                    
         |
272 | | neeq1 2698 |
. . . . . . . . . 10
         
           |
273 | | neeq1 2698 |
. . . . . . . . . 10
         
 
       
     |
274 | 272, 273 | bibi12d 327 |
. . . . . . . . 9
              
  
                       |
275 | 271, 274 | syl5ibcom 228 |
. . . . . . . 8
          
                    
                       |
276 | 275 | pm5.32rd 650 |
. . . . . . 7
          
                              
        
          |
277 | 269 | neneqd 2640 |
. . . . . . . . . 10
          
               
      |
278 | | biorf 411 |
. . . . . . . . . 10
                       |
279 | 277, 278 | syl 17 |
. . . . . . . . 9
          
                                  |
280 | | orcom 393 |
. . . . . . . . 9
                       |
281 | 279, 280 | syl6bb 269 |
. . . . . . . 8
          
                                  |
282 | 281 | anbi2d 715 |
. . . . . . 7
          
                              
        
              |
283 | 270 | neneqd 2640 |
. . . . . . . . . 10
          
               
        |
284 | | biorf 411 |
. . . . . . . . . 10
                           |
285 | 283, 284 | syl 17 |
. . . . . . . . 9
          
                         
          |
286 | | orcom 393 |
. . . . . . . . 9
                           |
287 | 285, 286 | syl6bb 269 |
. . . . . . . 8
          
                             
      |
288 | 287 | anbi2d 715 |
. . . . . . 7
          
                         
      
        
          
       |
289 | 276, 282,
288 | 3bitr3d 291 |
. . . . . 6
          
                          
                  
          
       |
290 | | eupath2lem1 25761 |
. . . . . . 7
 
                       
        
              |
291 | 256, 290 | syl 17 |
. . . . . 6
          
                                                 
              |
292 | | eupath2lem1 25761 |
. . . . . . 7
 
                       
   
        
          
       |
293 | 256, 292 | syl 17 |
. . . . . 6
          
                          
                          
          
       |
294 | 289, 291,
293 | 3bitr4d 293 |
. . . . 5
          
                                        
                       
       |
295 | 267, 268,
294 | 3bitrd 287 |
. . . 4
          
                    VDeg                 VDeg      
                      
                       
       |
296 | 228, 253,
295 | pm2.61da2ne 2724 |
. . 3
 
          
    VDeg                 VDeg                   
                                 
       |
297 | 190, 296 | pm2.61dane 2723 |
. 2
     VDeg                 VDeg      
                      
                       
       |
298 | 123, 297 | bitrd 261 |
1
    VDeg        
       
                       
       |