Step | Hyp | Ref
| Expression |
1 | | prfi 7877 |
. . . . . 6
    |
2 | | 3ne0 10737 |
. . . . . . 7
 |
3 | | 1re 9673 |
. . . . . . . 8
 |
4 | | 1lt3 10812 |
. . . . . . . 8
 |
5 | 3, 4 | gtneii 9777 |
. . . . . . 7
 |
6 | 2, 5 | nelpri 4000 |
. . . . . 6
    |
7 | | 3nn0 10921 |
. . . . . . 7
 |
8 | | hashunsng 12609 |
. . . . . . 7

    
                           |
9 | 7, 8 | ax-mp 5 |
. . . . . 6
    
                          |
10 | 1, 6, 9 | mp2an 683 |
. . . . 5
                     |
11 | | df-3 10702 |
. . . . . 6
   |
12 | | 0ne1 10710 |
. . . . . . . 8
 |
13 | | 0nn0 10918 |
. . . . . . . . 9
 |
14 | | 1nn0 10919 |
. . . . . . . . 9
 |
15 | | hashprg 12610 |
. . . . . . . . 9
 
            |
16 | 13, 14, 15 | mp2an 683 |
. . . . . . . 8

         |
17 | 12, 16 | mpbi 213 |
. . . . . . 7
        |
18 | 17 | oveq1i 6330 |
. . . . . 6
            |
19 | 11, 18 | eqtr4i 2487 |
. . . . 5
          |
20 | 10, 19 | eqtr4i 2487 |
. . . 4
            |
21 | | konigsberg.v |
. . . . . . . 8
     |
22 | | fzfi 12223 |
. . . . . . . 8
     |
23 | 21, 22 | eqeltri 2536 |
. . . . . . 7
 |
24 | | ssrab2 3526 |
. . . . . . 7

  VDeg       |
25 | | ssfi 7823 |
. . . . . . 7
  
  VDeg       
  VDeg        |
26 | 23, 24, 25 | mp2an 683 |
. . . . . 6

  VDeg       |
27 | | nn0uz 11227 |
. . . . . . . . . . . 12
     |
28 | 7, 27 | eleqtri 2538 |
. . . . . . . . . . 11
     |
29 | | eluzfz1 11841 |
. . . . . . . . . . 11
    
      |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . 10
     |
31 | 30, 21 | eleqtrri 2539 |
. . . . . . . . 9
 |
32 | | 2nn 10801 |
. . . . . . . . . 10
 |
33 | | 1nn 10653 |
. . . . . . . . . 10
 |
34 | | 2t1e2 10792 |
. . . . . . . . . . . 12
   |
35 | 34 | oveq1i 6330 |
. . . . . . . . . . 11
       |
36 | 35, 11 | eqtr4i 2487 |
. . . . . . . . . 10
     |
37 | | 1lt2 10810 |
. . . . . . . . . 10
 |
38 | 32, 14, 33, 36, 37 | ndvdsi 14446 |
. . . . . . . . 9
 |
39 | | fveq2 5892 |
. . . . . . . . . . . . 13
   VDeg
      VDeg       |
40 | 23 | elexi 3067 |
. . . . . . . . . . . . . 14
 |
41 | | df-s6 12991 |
. . . . . . . . . . . . . . 15
                                          ++          |
42 | | df-s5 12990 |
. . . . . . . . . . . . . . . 16
                                    ++          |
43 | | df-s4 12989 |
. . . . . . . . . . . . . . . . 17
                              ++          |
44 | | df-s3 12988 |
. . . . . . . . . . . . . . . . . 18
                        ++          |
45 | | df-s2 12987 |
. . . . . . . . . . . . . . . . . . 19
                  ++          |
46 | | 1le3 10860 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
47 | 14, 27 | eleqtri 2538 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
48 | | 3z 11004 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
49 | | elfz5 11827 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
   |
50 | 47, 48, 49 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
  |
51 | 46, 50 | mpbir 214 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
52 | 51, 21 | eleqtrri 2539 |
. . . . . . . . . . . . . . . . . . . . 21
 |
53 | 40, 31, 52 | umgrabi 25767 |
. . . . . . . . . . . . . . . . . . . 20
            
   |
54 | 53 | s1cld 12784 |
. . . . . . . . . . . . . . . . . . 19
       Word              |
55 | | 2re 10712 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
56 | | 3re 10716 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
57 | | 2lt3 10811 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
58 | 55, 56, 57 | ltleii 9788 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
59 | | 2eluzge0 11237 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
60 | | elfz5 11827 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
   |
61 | 59, 48, 60 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . 22
    
  |
62 | 58, 61 | mpbir 214 |
. . . . . . . . . . . . . . . . . . . . 21
     |
63 | 62, 21 | eleqtrri 2539 |
. . . . . . . . . . . . . . . . . . . 20
 |
64 | 40, 31, 63 | umgrabi 25767 |
. . . . . . . . . . . . . . . . . . 19
            
   |
65 | 45, 54, 64 | cats1cld 12994 |
. . . . . . . . . . . . . . . . . 18
          Word          
   |
66 | | eluzfz2 11842 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
67 | 28, 66 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
     |
68 | 67, 21 | eleqtrri 2539 |
. . . . . . . . . . . . . . . . . . 19
 |
69 | 40, 31, 68 | umgrabi 25767 |
. . . . . . . . . . . . . . . . . 18
            
   |
70 | 44, 65, 69 | cats1cld 12994 |
. . . . . . . . . . . . . . . . 17
             Word              |
71 | 40, 52, 63 | umgrabi 25767 |
. . . . . . . . . . . . . . . . 17
            
   |
72 | 43, 70, 71 | cats1cld 12994 |
. . . . . . . . . . . . . . . 16
                Word              |
73 | 42, 72, 71 | cats1cld 12994 |
. . . . . . . . . . . . . . 15
                   Word              |
74 | 40, 63, 68 | umgrabi 25767 |
. . . . . . . . . . . . . . 15
            
   |
75 | 41, 73, 74 | cats1cld 12994 |
. . . . . . . . . . . . . 14
                      Word          
   |
76 | | wrd0 12733 |
. . . . . . . . . . . . . . . . . . . . 21
Word          
  |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
Word
         
   |
78 | 40, 31 | vdeg0i 25766 |
. . . . . . . . . . . . . . . . . . . 20
  VDeg      |
79 | | 1e0p1 11113 |
. . . . . . . . . . . . . . . . . . . 20
   |
80 | | ax-1ne0 9639 |
. . . . . . . . . . . . . . . . . . . 20
 |
81 | | s0s1 13059 |
. . . . . . . . . . . . . . . . . . . 20
        ++          |
82 | 40, 77, 31, 78, 79, 52, 80, 81 | vdegp1bi 25769 |
. . . . . . . . . . . . . . . . . . 19
  VDeg             |
83 | | df-2 10701 |
. . . . . . . . . . . . . . . . . . 19
   |
84 | | 2ne0 10735 |
. . . . . . . . . . . . . . . . . . 19
 |
85 | 40, 54, 31, 82, 83, 63, 84, 45 | vdegp1bi 25769 |
. . . . . . . . . . . . . . . . . 18
  VDeg                |
86 | 40, 65, 31, 85, 11, 68, 2, 44 | vdegp1bi 25769 |
. . . . . . . . . . . . . . . . 17
  VDeg                   |
87 | 40, 70, 31, 86, 52, 80, 63, 84, 43 | vdegp1ai 25768 |
. . . . . . . . . . . . . . . 16
  VDeg                      |
88 | 40, 72, 31, 87, 52, 80, 63, 84, 42 | vdegp1ai 25768 |
. . . . . . . . . . . . . . 15
  VDeg                         |
89 | 40, 73, 31, 88, 63, 84, 68, 2, 41 | vdegp1ai 25768 |
. . . . . . . . . . . . . 14
  VDeg                            |
90 | | konigsberg.e |
. . . . . . . . . . . . . . 15
                          |
91 | | df-s7 12992 |
. . . . . . . . . . . . . . 15
                                                ++          |
92 | 90, 91 | eqtri 2484 |
. . . . . . . . . . . . . 14
                       ++          |
93 | 40, 75, 31, 89, 63, 84, 68, 2, 92 | vdegp1ai 25768 |
. . . . . . . . . . . . 13
  VDeg      |
94 | 39, 93 | syl6eq 2512 |
. . . . . . . . . . . 12
   VDeg
      |
95 | 94 | breq2d 4430 |
. . . . . . . . . . 11
 
  VDeg        |
96 | 95 | notbid 300 |
. . . . . . . . . 10
 
  VDeg    
   |
97 | 96 | elrab 3208 |
. . . . . . . . 9
    VDeg          |
98 | 31, 38, 97 | mpbir2an 936 |
. . . . . . . 8
   VDeg
      |
99 | | fveq2 5892 |
. . . . . . . . . . . . 13
   VDeg
      VDeg       |
100 | 40, 52 | vdeg0i 25766 |
. . . . . . . . . . . . . . . . . . . 20
  VDeg      |
101 | 40, 77, 52, 100, 79, 31, 12, 81 | vdegp1ci 25770 |
. . . . . . . . . . . . . . . . . . 19
  VDeg             |
102 | 3, 37 | gtneii 9777 |
. . . . . . . . . . . . . . . . . . 19
 |
103 | 40, 54, 52, 101, 31, 12, 63, 102, 45 | vdegp1ai 25768 |
. . . . . . . . . . . . . . . . . 18
  VDeg                |
104 | 40, 65, 52, 103, 31, 12, 68, 5, 44 | vdegp1ai 25768 |
. . . . . . . . . . . . . . . . 17
  VDeg                   |
105 | 40, 70, 52, 104, 83, 63, 102, 43 | vdegp1bi 25769 |
. . . . . . . . . . . . . . . 16
  VDeg                      |
106 | 40, 72, 52, 105, 11, 63, 102, 42 | vdegp1bi 25769 |
. . . . . . . . . . . . . . 15
  VDeg                         |
107 | 40, 73, 52, 106, 63, 102, 68, 5, 41 | vdegp1ai 25768 |
. . . . . . . . . . . . . 14
  VDeg                            |
108 | 40, 75, 52, 107, 63, 102, 68, 5, 92 | vdegp1ai 25768 |
. . . . . . . . . . . . 13
  VDeg      |
109 | 99, 108 | syl6eq 2512 |
. . . . . . . . . . . 12
   VDeg
      |
110 | 109 | breq2d 4430 |
. . . . . . . . . . 11
 
  VDeg        |
111 | 110 | notbid 300 |
. . . . . . . . . 10
 
  VDeg    
   |
112 | 111 | elrab 3208 |
. . . . . . . . 9
    VDeg          |
113 | 52, 38, 112 | mpbir2an 936 |
. . . . . . . 8
   VDeg
      |
114 | | prssi 4141 |
. . . . . . . 8
  
  VDeg         VDeg
         
  VDeg        |
115 | 98, 113, 114 | mp2an 683 |
. . . . . . 7
   
  VDeg       |
116 | | fveq2 5892 |
. . . . . . . . . . . . 13
   VDeg
      VDeg       |
117 | 40, 68 | vdeg0i 25766 |
. . . . . . . . . . . . . . . . . . . 20
  VDeg      |
118 | | 0re 9674 |
. . . . . . . . . . . . . . . . . . . . 21
 |
119 | | 3pos 10736 |
. . . . . . . . . . . . . . . . . . . . 21
 |
120 | 118, 119 | ltneii 9778 |
. . . . . . . . . . . . . . . . . . . 20
 |
121 | 3, 4 | ltneii 9778 |
. . . . . . . . . . . . . . . . . . . 20
 |
122 | 40, 77, 68, 117, 31, 120, 52, 121, 81 | vdegp1ai 25768 |
. . . . . . . . . . . . . . . . . . 19
  VDeg             |
123 | 55, 57 | ltneii 9778 |
. . . . . . . . . . . . . . . . . . 19
 |
124 | 40, 54, 68, 122, 31, 120, 63, 123, 45 | vdegp1ai 25768 |
. . . . . . . . . . . . . . . . . 18
  VDeg                |
125 | 40, 65, 68, 124, 79, 31, 120, 44 | vdegp1ci 25770 |
. . . . . . . . . . . . . . . . 17
  VDeg                   |
126 | 40, 70, 68, 125, 52, 121, 63, 123, 43 | vdegp1ai 25768 |
. . . . . . . . . . . . . . . 16
  VDeg                      |
127 | 40, 72, 68, 126, 52, 121, 63, 123, 42 | vdegp1ai 25768 |
. . . . . . . . . . . . . . 15
  VDeg                         |
128 | 40, 73, 68, 127, 83, 63, 123, 41 | vdegp1ci 25770 |
. . . . . . . . . . . . . 14
  VDeg                            |
129 | 40, 75, 68, 128, 11, 63, 123, 92 | vdegp1ci 25770 |
. . . . . . . . . . . . 13
  VDeg      |
130 | 116, 129 | syl6eq 2512 |
. . . . . . . . . . . 12
   VDeg
      |
131 | 130 | breq2d 4430 |
. . . . . . . . . . 11
 
  VDeg        |
132 | 131 | notbid 300 |
. . . . . . . . . 10
 
  VDeg    
   |
133 | 132 | elrab 3208 |
. . . . . . . . 9
    VDeg          |
134 | 68, 38, 133 | mpbir2an 936 |
. . . . . . . 8
   VDeg
      |
135 | | snssi 4129 |
. . . . . . . 8
    VDeg           VDeg        |
136 | 134, 135 | ax-mp 5 |
. . . . . . 7
 

  VDeg       |
137 | 115, 136 | unssi 3621 |
. . . . . 6
      

  VDeg       |
138 | | ssdomg 7646 |
. . . . . 6
 
  VDeg             

  VDeg             
  VDeg         |
139 | 26, 137, 138 | mp2 9 |
. . . . 5
          VDeg       |
140 | | snfi 7681 |
. . . . . . 7
   |
141 | | unfi 7869 |
. . . . . . 7
                 |
142 | 1, 140, 141 | mp2an 683 |
. . . . . 6
        |
143 | | hashdom 12596 |
. . . . . 6
        

  VDeg                      
  VDeg              
  VDeg         |
144 | 142, 26, 143 | mp2an 683 |
. . . . 5
                  VDeg      
          VDeg        |
145 | 139, 144 | mpbir 214 |
. . . 4
              
  VDeg        |
146 | 20, 145 | eqbrtrri 4440 |
. . 3
   
  VDeg        |
147 | | hashcl 12576 |
. . . . . 6
 
  VDeg         
  VDeg         |
148 | 26, 147 | ax-mp 5 |
. . . . 5
      VDeg
       |
149 | 148 | nn0rei 10914 |
. . . 4
      VDeg
       |
150 | 56, 149 | lenlti 9785 |
. . 3
    
  VDeg          
  VDeg         |
151 | 146, 150 | mpbi 213 |
. 2
      VDeg        |
152 | | eupath 25765 |
. . . 4
  EulPaths        VDeg            |
153 | | elpri 3997 |
. . . 4
    
  VDeg         
       VDeg          
  VDeg          |
154 | | id 22 |
. . . . . 6
    
  VDeg      
   
  VDeg         |
155 | 154, 119 | syl6eqbr 4456 |
. . . . 5
    
  VDeg      
   
  VDeg         |
156 | | id 22 |
. . . . . 6
    
  VDeg      
   
  VDeg         |
157 | 156, 57 | syl6eqbr 4456 |
. . . . 5
    
  VDeg      
   
  VDeg         |
158 | 155, 157 | jaoi 385 |
. . . 4
     
  VDeg             VDeg       
   
  VDeg         |
159 | 152, 153,
158 | 3syl 18 |
. . 3
  EulPaths        VDeg         |
160 | 159 | necon1bi 2664 |
. 2
    
  VDeg        EulPaths    |
161 | 151, 160 | ax-mp 5 |
1
 EulPaths   |