Step | Hyp | Ref
| Expression |
1 | | fvexd 6858 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (πΉβπ) β V) |
2 | | trlsegvdeg.u |
. . . . . . . . . . . 12
β’ (π β π β π) |
3 | 2 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β π β π) |
4 | | trlsegvdeg.v |
. . . . . . . . . . . . . 14
β’ π = (VtxβπΊ) |
5 | | trlsegvdeg.i |
. . . . . . . . . . . . . 14
β’ πΌ = (iEdgβπΊ) |
6 | | trlsegvdeg.f |
. . . . . . . . . . . . . 14
β’ (π β Fun πΌ) |
7 | | trlsegvdeg.n |
. . . . . . . . . . . . . 14
β’ (π β π β (0..^(β―βπΉ))) |
8 | | trlsegvdeg.w |
. . . . . . . . . . . . . 14
β’ (π β πΉ(TrailsβπΊ)π) |
9 | 4, 5, 6, 7, 2, 8 | trlsegvdeglem1 29167 |
. . . . . . . . . . . . 13
β’ (π β ((πβπ) β π β§ (πβ(π + 1)) β π)) |
10 | 9 | simprd 497 |
. . . . . . . . . . . 12
β’ (π β (πβ(π + 1)) β π) |
11 | 10 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (πβ(π + 1)) β π) |
12 | | neeq1 3007 |
. . . . . . . . . . . . . 14
β’ ((πβπ) = π β ((πβπ) β (πβ(π + 1)) β π β (πβ(π + 1)))) |
13 | 12 | biimpcd 249 |
. . . . . . . . . . . . 13
β’ ((πβπ) β (πβ(π + 1)) β ((πβπ) = π β π β (πβ(π + 1)))) |
14 | 13 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) β (πβ(π + 1))) β ((πβπ) = π β π β (πβ(π + 1)))) |
15 | 14 | imp 408 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β π β (πβ(π + 1))) |
16 | | eupth2lem3lem4.i |
. . . . . . . . . . . 12
β’ (π β (πΌβ(πΉβπ)) β π« π) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (πΌβ(πΉβπ)) β π« π) |
18 | | trlsegvdeg.iy |
. . . . . . . . . . . 12
β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
20 | | eupth2lem3lem3.e |
. . . . . . . . . . . . . 14
β’ (π β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) β (πβ(π + 1))) β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
22 | | df-ne 2945 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β (πβ(π + 1)) β Β¬ (πβπ) = (πβ(π + 1))) |
23 | | ifpfal 1076 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(πβπ) = (πβ(π + 1)) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
24 | 22, 23 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β (πβ(π + 1)) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
25 | 24 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβπ) β (πβ(π + 1))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
26 | | preq1 4695 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) = π β {(πβπ), (πβ(π + 1))} = {π, (πβ(π + 1))}) |
27 | 26 | sseq1d 3976 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) = π β ({(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)) β {π, (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
28 | 27 | biimpcd 249 |
. . . . . . . . . . . . . 14
β’ ({(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)) β ((πβπ) = π β {π, (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
29 | 25, 28 | syl6bi 253 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) β (πβ(π + 1))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β ((πβπ) = π β {π, (πβ(π + 1))} β (πΌβ(πΉβπ))))) |
30 | 21, 29 | mpd 15 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) β (πβ(π + 1))) β ((πβπ) = π β {π, (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
31 | 30 | imp 408 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β {π, (πβ(π + 1))} β (πΌβ(πΉβπ))) |
32 | | trlsegvdeg.vy |
. . . . . . . . . . . 12
β’ (π β (Vtxβπ) = π) |
33 | 32 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (Vtxβπ) = π) |
34 | 1, 3, 11, 15, 17, 19, 31, 33 | 1hegrvtxdg1 28458 |
. . . . . . . . . 10
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β ((VtxDegβπ)βπ) = 1) |
35 | 34 | oveq2d 7374 |
. . . . . . . . 9
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) = (((VtxDegβπ)βπ) + 1)) |
36 | 35 | breq2d 5118 |
. . . . . . . 8
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β 2 β₯ (((VtxDegβπ)βπ) + 1))) |
37 | 36 | notbid 318 |
. . . . . . 7
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β Β¬ 2 β₯
(((VtxDegβπ)βπ) + 1))) |
38 | | trlsegvdeg.vx |
. . . . . . . . . . . . . . 15
β’ (π β (Vtxβπ) = π) |
39 | | trlsegvdeg.vz |
. . . . . . . . . . . . . . 15
β’ (π β (Vtxβπ) = π) |
40 | | trlsegvdeg.ix |
. . . . . . . . . . . . . . 15
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) |
41 | | trlsegvdeg.iz |
. . . . . . . . . . . . . . 15
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) |
42 | 4, 5, 6, 7, 2, 8, 38, 32, 39, 40, 18, 41 | eupth2lem3lem1 29175 |
. . . . . . . . . . . . . 14
β’ (π β ((VtxDegβπ)βπ) β
β0) |
43 | 42 | nn0zd 12526 |
. . . . . . . . . . . . 13
β’ (π β ((VtxDegβπ)βπ) β β€) |
44 | | 2nn 12227 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
45 | 44 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 2 β
β) |
46 | | 1lt2 12325 |
. . . . . . . . . . . . . 14
β’ 1 <
2 |
47 | 46 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 1 < 2) |
48 | | ndvdsp1 16294 |
. . . . . . . . . . . . 13
β’
((((VtxDegβπ)βπ) β β€ β§ 2 β β
β§ 1 < 2) β (2 β₯ ((VtxDegβπ)βπ) β Β¬ 2 β₯
(((VtxDegβπ)βπ) + 1))) |
49 | 43, 45, 47, 48 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β (2 β₯
((VtxDegβπ)βπ) β Β¬ 2 β₯
(((VtxDegβπ)βπ) + 1))) |
50 | 49 | con2d 134 |
. . . . . . . . . . 11
β’ (π β (2 β₯
(((VtxDegβπ)βπ) + 1) β Β¬ 2 β₯
((VtxDegβπ)βπ))) |
51 | | 1z 12534 |
. . . . . . . . . . . . . 14
β’ 1 β
β€ |
52 | | n2dvds1 16251 |
. . . . . . . . . . . . . 14
β’ Β¬ 2
β₯ 1 |
53 | | opoe 16246 |
. . . . . . . . . . . . . 14
β’
(((((VtxDegβπ)βπ) β β€ β§ Β¬ 2 β₯
((VtxDegβπ)βπ)) β§ (1 β β€ β§ Β¬ 2
β₯ 1)) β 2 β₯ (((VtxDegβπ)βπ) + 1)) |
54 | 51, 52, 53 | mpanr12 704 |
. . . . . . . . . . . . 13
β’
((((VtxDegβπ)βπ) β β€ β§ Β¬ 2 β₯
((VtxDegβπ)βπ)) β 2 β₯ (((VtxDegβπ)βπ) + 1)) |
55 | 54 | ex 414 |
. . . . . . . . . . . 12
β’
(((VtxDegβπ)βπ) β β€ β (Β¬ 2 β₯
((VtxDegβπ)βπ) β 2 β₯ (((VtxDegβπ)βπ) + 1))) |
56 | 43, 55 | syl 17 |
. . . . . . . . . . 11
β’ (π β (Β¬ 2 β₯
((VtxDegβπ)βπ) β 2 β₯ (((VtxDegβπ)βπ) + 1))) |
57 | 50, 56 | impbid 211 |
. . . . . . . . . 10
β’ (π β (2 β₯
(((VtxDegβπ)βπ) + 1) β Β¬ 2 β₯
((VtxDegβπ)βπ))) |
58 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β ((VtxDegβπ)βπ₯) = ((VtxDegβπ)βπ)) |
59 | 58 | breq2d 5118 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (2 β₯ ((VtxDegβπ)βπ₯) β 2 β₯ ((VtxDegβπ)βπ))) |
60 | 59 | notbid 318 |
. . . . . . . . . . . 12
β’ (π₯ = π β (Β¬ 2 β₯
((VtxDegβπ)βπ₯) β Β¬ 2 β₯ ((VtxDegβπ)βπ))) |
61 | 60 | elrab3 3647 |
. . . . . . . . . . 11
β’ (π β π β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} β Β¬ 2 β₯
((VtxDegβπ)βπ))) |
62 | 2, 61 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} β Β¬ 2 β₯
((VtxDegβπ)βπ))) |
63 | | eupth2lem3.o |
. . . . . . . . . . 11
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) |
64 | 63 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
65 | 57, 62, 64 | 3bitr2d 307 |
. . . . . . . . 9
β’ (π β (2 β₯
(((VtxDegβπ)βπ) + 1) β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
66 | 65 | notbid 318 |
. . . . . . . 8
β’ (π β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + 1) β Β¬ π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
67 | 66 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + 1) β Β¬ π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
68 | | fvex 6856 |
. . . . . . . . 9
β’ (πβπ) β V |
69 | 68 | eupth2lem2 29166 |
. . . . . . . 8
β’ (((πβπ) β (πβ(π + 1)) β§ (πβπ) = π) β (Β¬ π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
70 | 69 | adantll 713 |
. . . . . . 7
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (Β¬ π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
71 | 37, 67, 70 | 3bitrd 305 |
. . . . . 6
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβπ) = π) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
72 | 71 | expcom 415 |
. . . . 5
β’ ((πβπ) = π β ((π β§ (πβπ) β (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
73 | 72 | eqcoms 2745 |
. . . 4
β’ (π = (πβπ) β ((π β§ (πβπ) β (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
74 | | fvexd 6858 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (πΉβπ) β V) |
75 | 9 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β (πβπ) β π) |
76 | 75 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (πβπ) β π) |
77 | 2 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β π β π) |
78 | | neeq2 3008 |
. . . . . . . . . . . . . 14
β’ ((πβ(π + 1)) = π β ((πβπ) β (πβ(π + 1)) β (πβπ) β π)) |
79 | 78 | biimpcd 249 |
. . . . . . . . . . . . 13
β’ ((πβπ) β (πβ(π + 1)) β ((πβ(π + 1)) = π β (πβπ) β π)) |
80 | 79 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) β (πβ(π + 1))) β ((πβ(π + 1)) = π β (πβπ) β π)) |
81 | 80 | imp 408 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (πβπ) β π) |
82 | 16 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (πΌβ(πΉβπ)) β π« π) |
83 | 18 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
84 | | preq2 4696 |
. . . . . . . . . . . . . . . 16
β’ ((πβ(π + 1)) = π β {(πβπ), (πβ(π + 1))} = {(πβπ), π}) |
85 | 84 | sseq1d 3976 |
. . . . . . . . . . . . . . 15
β’ ((πβ(π + 1)) = π β ({(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)) β {(πβπ), π} β (πΌβ(πΉβπ)))) |
86 | 85 | biimpcd 249 |
. . . . . . . . . . . . . 14
β’ ({(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)) β ((πβ(π + 1)) = π β {(πβπ), π} β (πΌβ(πΉβπ)))) |
87 | 25, 86 | syl6bi 253 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) β (πβ(π + 1))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β ((πβ(π + 1)) = π β {(πβπ), π} β (πΌβ(πΉβπ))))) |
88 | 21, 87 | mpd 15 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) β (πβ(π + 1))) β ((πβ(π + 1)) = π β {(πβπ), π} β (πΌβ(πΉβπ)))) |
89 | 88 | imp 408 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β {(πβπ), π} β (πΌβ(πΉβπ))) |
90 | 32 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (Vtxβπ) = π) |
91 | 74, 76, 77, 81, 82, 83, 89, 90 | 1hegrvtxdg1r 28459 |
. . . . . . . . . 10
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β ((VtxDegβπ)βπ) = 1) |
92 | 91 | oveq2d 7374 |
. . . . . . . . 9
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) = (((VtxDegβπ)βπ) + 1)) |
93 | 92 | breq2d 5118 |
. . . . . . . 8
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β 2 β₯ (((VtxDegβπ)βπ) + 1))) |
94 | 93 | notbid 318 |
. . . . . . 7
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β Β¬ 2 β₯
(((VtxDegβπ)βπ) + 1))) |
95 | 66 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + 1) β Β¬ π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
96 | | necom 2998 |
. . . . . . . . . 10
β’ ((πβπ) β (πβ(π + 1)) β (πβ(π + 1)) β (πβπ)) |
97 | | fvex 6856 |
. . . . . . . . . . 11
β’ (πβ(π + 1)) β V |
98 | 97 | eupth2lem2 29166 |
. . . . . . . . . 10
β’ (((πβ(π + 1)) β (πβπ) β§ (πβ(π + 1)) = π) β (Β¬ π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}) β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
99 | 96, 98 | sylanb 582 |
. . . . . . . . 9
β’ (((πβπ) β (πβ(π + 1)) β§ (πβ(π + 1)) = π) β (Β¬ π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}) β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
100 | 99 | con1bid 356 |
. . . . . . . 8
β’ (((πβπ) β (πβ(π + 1)) β§ (πβ(π + 1)) = π) β (Β¬ π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
101 | 100 | adantll 713 |
. . . . . . 7
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (Β¬ π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
102 | 94, 95, 101 | 3bitrd 305 |
. . . . . 6
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (πβ(π + 1)) = π) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
103 | 102 | expcom 415 |
. . . . 5
β’ ((πβ(π + 1)) = π β ((π β§ (πβπ) β (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
104 | 103 | eqcoms 2745 |
. . . 4
β’ (π = (πβ(π + 1)) β ((π β§ (πβπ) β (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
105 | 73, 104 | jaoi 856 |
. . 3
β’ ((π = (πβπ) β¨ π = (πβ(π + 1))) β ((π β§ (πβπ) β (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
106 | 105 | com12 32 |
. 2
β’ ((π β§ (πβπ) β (πβ(π + 1))) β ((π = (πβπ) β¨ π = (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
107 | 106 | 3impia 1118 |
1
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π = (πβπ) β¨ π = (πβ(π + 1)))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |