Step | Hyp | Ref
| Expression |
1 | | trlsegvdeg.u |
. . . . 5
β’ (π β π β π) |
2 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = π β ((VtxDegβπ)βπ₯) = ((VtxDegβπ)βπ)) |
3 | 2 | breq2d 5118 |
. . . . . . 7
β’ (π₯ = π β (2 β₯ ((VtxDegβπ)βπ₯) β 2 β₯ ((VtxDegβπ)βπ))) |
4 | 3 | notbid 318 |
. . . . . 6
β’ (π₯ = π β (Β¬ 2 β₯
((VtxDegβπ)βπ₯) β Β¬ 2 β₯ ((VtxDegβπ)βπ))) |
5 | 4 | elrab3 3647 |
. . . . 5
β’ (π β π β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} β Β¬ 2 β₯
((VtxDegβπ)βπ))) |
6 | 1, 5 | syl 17 |
. . . 4
β’ (π β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} β Β¬ 2 β₯
((VtxDegβπ)βπ))) |
7 | | eupth2lem3.o |
. . . . 5
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) |
8 | 7 | eleq2d 2824 |
. . . 4
β’ (π β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
9 | 6, 8 | bitr3d 281 |
. . 3
β’ (π β (Β¬ 2 β₯
((VtxDegβπ)βπ) β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
10 | 9 | adantr 482 |
. 2
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (Β¬ 2 β₯
((VtxDegβπ)βπ) β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
11 | | 2z 12536 |
. . . . . 6
β’ 2 β
β€ |
12 | 11 | a1i 11 |
. . . . 5
β’ ((π β§ (πβπ) = (πβ(π + 1))) β 2 β
β€) |
13 | | trlsegvdeg.v |
. . . . . . . 8
β’ π = (VtxβπΊ) |
14 | | trlsegvdeg.i |
. . . . . . . 8
β’ πΌ = (iEdgβπΊ) |
15 | | trlsegvdeg.f |
. . . . . . . 8
β’ (π β Fun πΌ) |
16 | | trlsegvdeg.n |
. . . . . . . 8
β’ (π β π β (0..^(β―βπΉ))) |
17 | | trlsegvdeg.w |
. . . . . . . 8
β’ (π β πΉ(TrailsβπΊ)π) |
18 | | trlsegvdeg.vx |
. . . . . . . 8
β’ (π β (Vtxβπ) = π) |
19 | | trlsegvdeg.vy |
. . . . . . . 8
β’ (π β (Vtxβπ) = π) |
20 | | trlsegvdeg.vz |
. . . . . . . 8
β’ (π β (Vtxβπ) = π) |
21 | | trlsegvdeg.ix |
. . . . . . . 8
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) |
22 | | trlsegvdeg.iy |
. . . . . . . 8
β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
23 | | trlsegvdeg.iz |
. . . . . . . 8
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) |
24 | 13, 14, 15, 16, 1, 17, 18, 19, 20, 21, 22, 23 | eupth2lem3lem1 29175 |
. . . . . . 7
β’ (π β ((VtxDegβπ)βπ) β
β0) |
25 | 24 | nn0zd 12526 |
. . . . . 6
β’ (π β ((VtxDegβπ)βπ) β β€) |
26 | 25 | adantr 482 |
. . . . 5
β’ ((π β§ (πβπ) = (πβ(π + 1))) β ((VtxDegβπ)βπ) β β€) |
27 | 13, 14, 15, 16, 1, 17, 18, 19, 20, 21, 22, 23 | eupth2lem3lem2 29176 |
. . . . . . 7
β’ (π β ((VtxDegβπ)βπ) β
β0) |
28 | 27 | nn0zd 12526 |
. . . . . 6
β’ (π β ((VtxDegβπ)βπ) β β€) |
29 | 28 | adantr 482 |
. . . . 5
β’ ((π β§ (πβπ) = (πβ(π + 1))) β ((VtxDegβπ)βπ) β β€) |
30 | | z2even 16253 |
. . . . . . 7
β’ 2 β₯
2 |
31 | 19 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β (Vtxβπ) = π) |
32 | | fvexd 6858 |
. . . . . . . 8
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β (πΉβπ) β V) |
33 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β π β π) |
34 | 22 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
35 | | eupth2lem3lem3.e |
. . . . . . . . . . . . . 14
β’ (π β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) = (πβ(π + 1))) β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
37 | | ifptru 1075 |
. . . . . . . . . . . . . 14
β’ ((πβπ) = (πβ(π + 1)) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β (πΌβ(πΉβπ)) = {(πβπ)})) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β (πΌβ(πΉβπ)) = {(πβπ)})) |
39 | 36, 38 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (πΌβ(πΉβπ)) = {(πβπ)}) |
40 | | sneq 4597 |
. . . . . . . . . . . . 13
β’ ((πβπ) = π β {(πβπ)} = {π}) |
41 | 40 | eqcoms 2745 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β {(πβπ)} = {π}) |
42 | 39, 41 | sylan9eq 2797 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β (πΌβ(πΉβπ)) = {π}) |
43 | 42 | opeq2d 4838 |
. . . . . . . . . 10
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β β¨(πΉβπ), (πΌβ(πΉβπ))β© = β¨(πΉβπ), {π}β©) |
44 | 43 | sneqd 4599 |
. . . . . . . . 9
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β {β¨(πΉβπ), (πΌβ(πΉβπ))β©} = {β¨(πΉβπ), {π}β©}) |
45 | 34, 44 | eqtrd 2777 |
. . . . . . . 8
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β (iEdgβπ) = {β¨(πΉβπ), {π}β©}) |
46 | 31, 32, 33, 45 | 1loopgrvd2 28454 |
. . . . . . 7
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β ((VtxDegβπ)βπ) = 2) |
47 | 30, 46 | breqtrrid 5144 |
. . . . . 6
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π = (πβπ)) β 2 β₯ ((VtxDegβπ)βπ)) |
48 | | z0even 16250 |
. . . . . . 7
β’ 2 β₯
0 |
49 | 19 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π β (πβπ)) β (Vtxβπ) = π) |
50 | | fvexd 6858 |
. . . . . . . 8
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π β (πβπ)) β (πΉβπ) β V) |
51 | 13, 14, 15, 16, 1, 17 | trlsegvdeglem1 29167 |
. . . . . . . . . 10
β’ (π β ((πβπ) β π β§ (πβ(π + 1)) β π)) |
52 | 51 | simpld 496 |
. . . . . . . . 9
β’ (π β (πβπ) β π) |
53 | 52 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π β (πβπ)) β (πβπ) β π) |
54 | 22 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
55 | 39 | opeq2d 4838 |
. . . . . . . . . . 11
β’ ((π β§ (πβπ) = (πβ(π + 1))) β β¨(πΉβπ), (πΌβ(πΉβπ))β© = β¨(πΉβπ), {(πβπ)}β©) |
56 | 55 | sneqd 4599 |
. . . . . . . . . 10
β’ ((π β§ (πβπ) = (πβ(π + 1))) β {β¨(πΉβπ), (πΌβ(πΉβπ))β©} = {β¨(πΉβπ), {(πβπ)}β©}) |
57 | 54, 56 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (iEdgβπ) = {β¨(πΉβπ), {(πβπ)}β©}) |
58 | 57 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π β (πβπ)) β (iEdgβπ) = {β¨(πΉβπ), {(πβπ)}β©}) |
59 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (πβπ) = (πβ(π + 1))) β π β π) |
60 | 59 | anim1i 616 |
. . . . . . . . 9
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π β (πβπ)) β (π β π β§ π β (πβπ))) |
61 | | eldifsn 4748 |
. . . . . . . . 9
β’ (π β (π β {(πβπ)}) β (π β π β§ π β (πβπ))) |
62 | 60, 61 | sylibr 233 |
. . . . . . . 8
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π β (πβπ)) β π β (π β {(πβπ)})) |
63 | 49, 50, 53, 58, 62 | 1loopgrvd0 28455 |
. . . . . . 7
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π β (πβπ)) β ((VtxDegβπ)βπ) = 0) |
64 | 48, 63 | breqtrrid 5144 |
. . . . . 6
β’ (((π β§ (πβπ) = (πβ(π + 1))) β§ π β (πβπ)) β 2 β₯ ((VtxDegβπ)βπ)) |
65 | 47, 64 | pm2.61dane 3033 |
. . . . 5
β’ ((π β§ (πβπ) = (πβ(π + 1))) β 2 β₯
((VtxDegβπ)βπ)) |
66 | | dvdsadd2b 16189 |
. . . . 5
β’ ((2
β β€ β§ ((VtxDegβπ)βπ) β β€ β§ (((VtxDegβπ)βπ) β β€ β§ 2 β₯
((VtxDegβπ)βπ))) β (2 β₯ ((VtxDegβπ)βπ) β 2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)))) |
67 | 12, 26, 29, 65, 66 | syl112anc 1375 |
. . . 4
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (2 β₯
((VtxDegβπ)βπ) β 2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)))) |
68 | 27 | nn0cnd 12476 |
. . . . . . 7
β’ (π β ((VtxDegβπ)βπ) β β) |
69 | 24 | nn0cnd 12476 |
. . . . . . 7
β’ (π β ((VtxDegβπ)βπ) β β) |
70 | 68, 69 | addcomd 11358 |
. . . . . 6
β’ (π β (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) = (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ))) |
71 | 70 | breq2d 5118 |
. . . . 5
β’ (π β (2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β 2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)))) |
72 | 71 | adantr 482 |
. . . 4
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β 2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)))) |
73 | 67, 72 | bitrd 279 |
. . 3
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (2 β₯
((VtxDegβπ)βπ) β 2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)))) |
74 | 73 | notbid 318 |
. 2
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (Β¬ 2 β₯
((VtxDegβπ)βπ) β Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)))) |
75 | | simpr 486 |
. . . . 5
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (πβπ) = (πβ(π + 1))) |
76 | 75 | eqeq2d 2748 |
. . . 4
β’ ((π β§ (πβπ) = (πβ(π + 1))) β ((πβ0) = (πβπ) β (πβ0) = (πβ(π + 1)))) |
77 | 75 | preq2d 4702 |
. . . 4
β’ ((π β§ (πβπ) = (πβ(π + 1))) β {(πβ0), (πβπ)} = {(πβ0), (πβ(π + 1))}) |
78 | 76, 77 | ifbieq2d 4513 |
. . 3
β’ ((π β§ (πβπ) = (πβ(π + 1))) β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})) |
79 | 78 | eleq2d 2824 |
. 2
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
80 | 10, 74, 79 | 3bitr3d 309 |
1
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |