Step | Hyp | Ref
| Expression |
1 | | z0even 16250 |
. . . . 5
β’ 2 β₯
0 |
2 | | eupth2.v |
. . . . . . . . . . . 12
β’ π = (VtxβπΊ) |
3 | 2 | fvexi 6857 |
. . . . . . . . . . 11
β’ π β V |
4 | | eupth2.i |
. . . . . . . . . . . . 13
β’ πΌ = (iEdgβπΊ) |
5 | 4 | fvexi 6857 |
. . . . . . . . . . . 12
β’ πΌ β V |
6 | 5 | resex 5986 |
. . . . . . . . . . 11
β’ (πΌ βΎ (πΉ β (0..^0))) β V |
7 | 3, 6 | pm3.2i 472 |
. . . . . . . . . 10
β’ (π β V β§ (πΌ βΎ (πΉ β (0..^0))) β
V) |
8 | | opvtxfv 27958 |
. . . . . . . . . 10
β’ ((π β V β§ (πΌ βΎ (πΉ β (0..^0))) β V) β
(Vtxββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) = π) |
9 | 7, 8 | mp1i 13 |
. . . . . . . . 9
β’ (π β (Vtxββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) = π) |
10 | 9 | eqcomd 2743 |
. . . . . . . 8
β’ (π β π = (Vtxββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©)) |
11 | 10 | eleq2d 2824 |
. . . . . . 7
β’ (π β (π₯ β π β π₯ β (Vtxββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©))) |
12 | 11 | biimpa 478 |
. . . . . 6
β’ ((π β§ π₯ β π) β π₯ β (Vtxββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©)) |
13 | | opiedgfv 27961 |
. . . . . . . . 9
β’ ((π β V β§ (πΌ βΎ (πΉ β (0..^0))) β V) β
(iEdgββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) = (πΌ βΎ (πΉ β (0..^0)))) |
14 | 7, 13 | mp1i 13 |
. . . . . . . 8
β’ (π β (iEdgββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) = (πΌ βΎ (πΉ β (0..^0)))) |
15 | | fzo0 13597 |
. . . . . . . . . . . 12
β’ (0..^0) =
β
|
16 | 15 | imaeq2i 6012 |
. . . . . . . . . . 11
β’ (πΉ β (0..^0)) = (πΉ β
β
) |
17 | | ima0 6030 |
. . . . . . . . . . 11
β’ (πΉ β β
) =
β
|
18 | 16, 17 | eqtri 2765 |
. . . . . . . . . 10
β’ (πΉ β (0..^0)) =
β
|
19 | 18 | reseq2i 5935 |
. . . . . . . . 9
β’ (πΌ βΎ (πΉ β (0..^0))) = (πΌ βΎ β
) |
20 | | res0 5942 |
. . . . . . . . 9
β’ (πΌ βΎ β
) =
β
|
21 | 19, 20 | eqtri 2765 |
. . . . . . . 8
β’ (πΌ βΎ (πΉ β (0..^0))) =
β
|
22 | 14, 21 | eqtrdi 2793 |
. . . . . . 7
β’ (π β (iEdgββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) =
β
) |
23 | 22 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π) β (iEdgββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) =
β
) |
24 | | eqid 2737 |
. . . . . . 7
β’
(Vtxββ¨π,
(πΌ βΎ (πΉ β (0..^0)))β©) =
(Vtxββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) |
25 | | eqid 2737 |
. . . . . . 7
β’
(iEdgββ¨π,
(πΌ βΎ (πΉ β (0..^0)))β©) =
(iEdgββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) |
26 | 24, 25 | vtxdg0e 28425 |
. . . . . 6
β’ ((π₯ β (Vtxββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) β§
(iEdgββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©) = β
) β
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯) =
0) |
27 | 12, 23, 26 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β π) β ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©)βπ₯) = 0) |
28 | 1, 27 | breqtrrid 5144 |
. . . 4
β’ ((π β§ π₯ β π) β 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)) |
29 | 28 | notnotd 144 |
. . 3
β’ ((π β§ π₯ β π) β Β¬ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)) |
30 | 29 | ralrimiva 3144 |
. 2
β’ (π β βπ₯ β π Β¬ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)) |
31 | | rabeq0 4345 |
. 2
β’ ({π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)}
= β
β βπ₯
β π Β¬ Β¬ 2
β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©)βπ₯)) |
32 | 30, 31 | sylibr 233 |
1
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)}
= β
) |