Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . 4
|
2 | | s6cli 13629 |
. . . . 5
Word |
3 | 2 | elexi 3213 |
. . . 4
|
4 | 1, 3 | opvtxfvi 25889 |
. . 3
Vtx |
5 | 4 | eqcomi 2631 |
. 2
Vtx |
6 | | 1nn0 11308 |
. . 3
|
7 | | 3nn0 11310 |
. . 3
|
8 | | 1le3 11244 |
. . 3
|
9 | | elfz2nn0 12431 |
. . 3
|
10 | 6, 7, 8, 9 | mpbir3an 1244 |
. 2
|
11 | 1, 3 | opiedgfvi 25890 |
. . 3
iEdg |
12 | 11 | eqcomi 2631 |
. 2
iEdg |
13 | | s1cli 13384 |
. . 3
Word |
14 | | df-s7 13598 |
. . 3
++ |
15 | | eqid 2622 |
. . . 4
|
16 | | eqid 2622 |
. . . 4
|
17 | | eqid 2622 |
. . . 4
|
18 | 15, 16, 17 | konigsbergssiedgw 27111 |
. . 3
Word
Word ++ Word
|
19 | 2, 13, 14, 18 | mp3an 1424 |
. 2
Word
|
20 | | s5cli 13628 |
. . . . . 6
Word |
21 | 20 | elexi 3213 |
. . . . 5
|
22 | 1, 21 | opvtxfvi 25889 |
. . . 4
Vtx |
23 | 22 | eqcomi 2631 |
. . 3
Vtx |
24 | 1, 21 | opiedgfvi 25890 |
. . . 4
iEdg |
25 | 24 | eqcomi 2631 |
. . 3
iEdg |
26 | | s2cli 13625 |
. . . 4
Word |
27 | | s5s2 13680 |
. . . 4
++
|
28 | 15, 16, 17 | konigsbergssiedgw 27111 |
. . . 4
Word Word ++ Word |
29 | 20, 26, 27, 28 | mp3an 1424 |
. . 3
Word
|
30 | | s4cli 13627 |
. . . . . . . 8
Word |
31 | 30 | elexi 3213 |
. . . . . . 7
|
32 | 1, 31 | opvtxfvi 25889 |
. . . . . 6
Vtx |
33 | 32 | eqcomi 2631 |
. . . . 5
Vtx |
34 | 1, 31 | opiedgfvi 25890 |
. . . . . 6
iEdg |
35 | 34 | eqcomi 2631 |
. . . . 5
iEdg |
36 | | s3cli 13626 |
. . . . . 6
Word |
37 | | s4s3 13676 |
. . . . . 6
++ |
38 | 15, 16, 17 | konigsbergssiedgw 27111 |
. . . . . 6
Word Word ++ Word |
39 | 30, 36, 37, 38 | mp3an 1424 |
. . . . 5
Word |
40 | | s3cli 13626 |
. . . . . . . . . 10
Word |
41 | 40 | elexi 3213 |
. . . . . . . . 9
|
42 | 1, 41 | opvtxfvi 25889 |
. . . . . . . 8
Vtx |
43 | 42 | eqcomi 2631 |
. . . . . . 7
Vtx |
44 | 1, 41 | opiedgfvi 25890 |
. . . . . . . 8
iEdg |
45 | 44 | eqcomi 2631 |
. . . . . . 7
iEdg |
46 | | s4cli 13627 |
. . . . . . . 8
Word |
47 | | s3s4 13678 |
. . . . . . . 8
++ |
48 | 15, 16, 17 | konigsbergssiedgw 27111 |
. . . . . . . 8
Word Word ++ Word |
49 | 40, 46, 47, 48 | mp3an 1424 |
. . . . . . 7
Word |
50 | | s2cli 13625 |
. . . . . . . . . . 11
Word |
51 | 50 | elexi 3213 |
. . . . . . . . . 10
|
52 | 1, 51 | opvtxfvi 25889 |
. . . . . . . . 9
Vtx |
53 | 52 | eqcomi 2631 |
. . . . . . . 8
Vtx |
54 | 1, 51 | opiedgfvi 25890 |
. . . . . . . . 9
iEdg |
55 | 54 | eqcomi 2631 |
. . . . . . . 8
iEdg |
56 | | s5cli 13628 |
. . . . . . . . 9
Word |
57 | | s2s5 13679 |
. . . . . . . . 9
++ |
58 | 15, 16, 17 | konigsbergssiedgw 27111 |
. . . . . . . . 9
Word
Word ++ Word
|
59 | 50, 56, 57, 58 | mp3an 1424 |
. . . . . . . 8
Word
|
60 | | s1cli 13384 |
. . . . . . . . . . . 12
Word |
61 | 60 | elexi 3213 |
. . . . . . . . . . 11
|
62 | 1, 61 | opvtxfvi 25889 |
. . . . . . . . . 10
Vtx |
63 | 62 | eqcomi 2631 |
. . . . . . . . 9
Vtx |
64 | 1, 61 | opiedgfvi 25890 |
. . . . . . . . . 10
iEdg |
65 | 64 | eqcomi 2631 |
. . . . . . . . 9
iEdg |
66 | | s6cli 13629 |
. . . . . . . . . 10
Word |
67 | | s1s6 13672 |
. . . . . . . . . 10
++
|
68 | 15, 16, 17 | konigsbergssiedgw 27111 |
. . . . . . . . . 10
Word Word ++ Word |
69 | 60, 66, 67, 68 | mp3an 1424 |
. . . . . . . . 9
Word
|
70 | | 0ex 4790 |
. . . . . . . . . . . . 13
|
71 | 1, 70 | opvtxfvi 25889 |
. . . . . . . . . . . 12
Vtx |
72 | 71 | eqcomi 2631 |
. . . . . . . . . . 11
Vtx |
73 | 1, 70 | opiedgfvi 25890 |
. . . . . . . . . . . 12
iEdg |
74 | 73 | eqcomi 2631 |
. . . . . . . . . . 11
iEdg |
75 | | wrd0 13330 |
. . . . . . . . . . 11
Word
|
76 | | eqid 2622 |
. . . . . . . . . . . 12
|
77 | 72, 74 | vtxdg0e 26370 |
. . . . . . . . . . . 12
VtxDeg |
78 | 10, 76, 77 | mp2an 708 |
. . . . . . . . . . 11
VtxDeg |
79 | | 0elfz 12436 |
. . . . . . . . . . . 12
|
80 | 7, 79 | ax-mp 5 |
. . . . . . . . . . 11
|
81 | | 0ne1 11088 |
. . . . . . . . . . 11
|
82 | | s0s1 13667 |
. . . . . . . . . . . 12
++ |
83 | 64, 82 | eqtri 2644 |
. . . . . . . . . . 11
iEdg ++ |
84 | 72, 10, 74, 75, 78, 62, 80, 81, 83 | vdegp1ci 26434 |
. . . . . . . . . 10
VtxDeg |
85 | | 0p1e1 11132 |
. . . . . . . . . 10
|
86 | 84, 85 | eqtri 2644 |
. . . . . . . . 9
VtxDeg |
87 | | 2nn0 11309 |
. . . . . . . . . 10
|
88 | | 2re 11090 |
. . . . . . . . . . 11
|
89 | | 3re 11094 |
. . . . . . . . . . 11
|
90 | | 2lt3 11195 |
. . . . . . . . . . 11
|
91 | 88, 89, 90 | ltleii 10160 |
. . . . . . . . . 10
|
92 | | elfz2nn0 12431 |
. . . . . . . . . 10
|
93 | 87, 7, 91, 92 | mpbir3an 1244 |
. . . . . . . . 9
|
94 | | 1ne2 11240 |
. . . . . . . . . 10
|
95 | 94 | necomi 2848 |
. . . . . . . . 9
|
96 | | df-s2 13593 |
. . . . . . . . . 10
++ |
97 | 54, 96 | eqtri 2644 |
. . . . . . . . 9
iEdg ++
|
98 | 63, 10, 65, 69, 86, 52, 80, 81, 93, 95, 97 | vdegp1ai 26432 |
. . . . . . . 8
VtxDeg |
99 | | nn0fz0 12437 |
. . . . . . . . 9
|
100 | 7, 99 | mpbi 220 |
. . . . . . . 8
|
101 | | 1re 10039 |
. . . . . . . . 9
|
102 | | 1lt3 11196 |
. . . . . . . . 9
|
103 | 101, 102 | gtneii 10149 |
. . . . . . . 8
|
104 | | df-s3 13594 |
. . . . . . . . 9
++ |
105 | 44, 104 | eqtri 2644 |
. . . . . . . 8
iEdg ++ |
106 | 53, 10, 55, 59, 98, 42, 80, 81, 100, 103, 105 | vdegp1ai 26432 |
. . . . . . 7
VtxDeg |
107 | | df-s4 13595 |
. . . . . . . 8
++ |
108 | 34, 107 | eqtri 2644 |
. . . . . . 7
iEdg ++
|
109 | 43, 10, 45, 49, 106, 32, 93, 95, 108 | vdegp1bi 26433 |
. . . . . 6
VtxDeg |
110 | | 1p1e2 11134 |
. . . . . 6
|
111 | 109, 110 | eqtri 2644 |
. . . . 5
VtxDeg |
112 | | df-s5 13596 |
. . . . . 6
++ |
113 | 24, 112 | eqtri 2644 |
. . . . 5
iEdg ++ |
114 | 33, 10, 35, 39, 111, 22, 93, 95, 113 | vdegp1bi 26433 |
. . . 4
VtxDeg |
115 | | 2p1e3 11151 |
. . . 4
|
116 | 114, 115 | eqtri 2644 |
. . 3
VtxDeg |
117 | | df-s6 13597 |
. . . 4
++ |
118 | 11, 117 | eqtri 2644 |
. . 3
iEdg ++
|
119 | 23, 10, 25, 29, 116, 4, 93, 95, 100, 103, 118 | vdegp1ai 26432 |
. 2
VtxDeg |
120 | | konigsberg.v |
. . 3
|
121 | | konigsberg.e |
. . 3
|
122 | | konigsberg.g |
. . 3
|
123 | 120, 121,
122 | konigsbergvtx 27106 |
. 2
Vtx |
124 | 120, 121,
122 | konigsbergiedg 27107 |
. . 3
iEdg |
125 | 124, 14 | eqtri 2644 |
. 2
iEdg ++ |
126 | 5, 10, 12, 19, 119, 123, 93, 95, 100, 103, 125 | vdegp1ai 26432 |
1
VtxDeg |