Step | Hyp | Ref
| Expression |
1 | | trlsegvdeg.v |
. . . . 5
β’ π = (VtxβπΊ) |
2 | | trlsegvdeg.i |
. . . . 5
β’ πΌ = (iEdgβπΊ) |
3 | | trlsegvdeg.f |
. . . . 5
β’ (π β Fun πΌ) |
4 | | trlsegvdeg.n |
. . . . 5
β’ (π β π β (0..^(β―βπΉ))) |
5 | | trlsegvdeg.u |
. . . . 5
β’ (π β π β π) |
6 | | trlsegvdeg.w |
. . . . 5
β’ (π β πΉ(TrailsβπΊ)π) |
7 | | trlsegvdeg.vx |
. . . . 5
β’ (π β (Vtxβπ) = π) |
8 | | trlsegvdeg.vy |
. . . . 5
β’ (π β (Vtxβπ) = π) |
9 | | trlsegvdeg.vz |
. . . . 5
β’ (π β (Vtxβπ) = π) |
10 | | trlsegvdeg.ix |
. . . . 5
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) |
11 | | trlsegvdeg.iy |
. . . . 5
β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
12 | | trlsegvdeg.iz |
. . . . 5
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | trlsegvdeg 29174 |
. . . 4
β’ (π β ((VtxDegβπ)βπ) = (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ))) |
14 | 13 | breq2d 5118 |
. . 3
β’ (π β (2 β₯
((VtxDegβπ)βπ) β 2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)))) |
15 | 14 | notbid 318 |
. 2
β’ (π β (Β¬ 2 β₯
((VtxDegβπ)βπ) β Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)))) |
16 | | eupth2lem3.o |
. . . 4
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) |
17 | | eupth2lem3.e |
. . . . 5
β’ (π β (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
18 | | ifpprsnss 4726 |
. . . . 5
β’ ((πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
19 | 17, 18 | syl 17 |
. . . 4
β’ (π β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 16, 19 | eupth2lem3lem3 29177 |
. . 3
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
21 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 16, 17 | eupth2lem3lem5 29179 |
. . . . . . 7
β’ (π β (πΌβ(πΉβπ)) β π« π) |
22 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 16, 19, 21 | eupth2lem3lem4 29178 |
. . . . . 6
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π = (πβπ) β¨ π = (πβ(π + 1)))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
23 | 22 | 3expa 1119 |
. . . . 5
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (π = (πβπ) β¨ π = (πβ(π + 1)))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
24 | 23 | expcom 415 |
. . . 4
β’ ((π = (πβπ) β¨ π = (πβ(π + 1))) β ((π β§ (πβπ) β (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
25 | | neanior 3038 |
. . . . 5
β’ ((π β (πβπ) β§ π β (πβ(π + 1))) β Β¬ (π = (πβπ) β¨ π = (πβ(π + 1)))) |
26 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 16, 17 | eupth2lem3lem6 29180 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
27 | 26 | 3expa 1119 |
. . . . . 6
β’ (((π β§ (πβπ) β (πβ(π + 1))) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
28 | 27 | expcom 415 |
. . . . 5
β’ ((π β (πβπ) β§ π β (πβ(π + 1))) β ((π β§ (πβπ) β (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
29 | 25, 28 | sylbir 234 |
. . . 4
β’ (Β¬
(π = (πβπ) β¨ π = (πβ(π + 1))) β ((π β§ (πβπ) β (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
30 | 24, 29 | pm2.61i 182 |
. . 3
β’ ((π β§ (πβπ) β (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
31 | 20, 30 | pm2.61dane 3033 |
. 2
β’ (π β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
32 | 15, 31 | bitrd 279 |
1
β’ (π β (Β¬ 2 β₯
((VtxDegβπ)βπ) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |