Step | Hyp | Ref
| Expression |
1 | | finsumvtxdgeven.v |
. . 3
β’ π = (VtxβπΊ) |
2 | | finsumvtxdgeven.i |
. . 3
β’ πΌ = (iEdgβπΊ) |
3 | | finsumvtxdgeven.d |
. . 3
β’ π· = (VtxDegβπΊ) |
4 | 1, 2, 3 | finsumvtxdgeven 28809 |
. 2
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β 2 β₯
Ξ£π€ β π (π·βπ€)) |
5 | | incom 4202 |
. . . . . . 7
β’ ({π£ β π β£ Β¬ 2 β₯ (π·βπ£)} β© {π£ β π β£ 2 β₯ (π·βπ£)}) = ({π£ β π β£ 2 β₯ (π·βπ£)} β© {π£ β π β£ Β¬ 2 β₯ (π·βπ£)}) |
6 | | rabnc 4388 |
. . . . . . 7
β’ ({π£ β π β£ 2 β₯ (π·βπ£)} β© {π£ β π β£ Β¬ 2 β₯ (π·βπ£)}) = β
|
7 | 5, 6 | eqtri 2761 |
. . . . . 6
β’ ({π£ β π β£ Β¬ 2 β₯ (π·βπ£)} β© {π£ β π β£ 2 β₯ (π·βπ£)}) = β
|
8 | 7 | a1i 11 |
. . . . 5
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β ({π£ β π β£ Β¬ 2 β₯ (π·βπ£)} β© {π£ β π β£ 2 β₯ (π·βπ£)}) = β
) |
9 | | rabxm 4387 |
. . . . . . 7
β’ π = ({π£ β π β£ 2 β₯ (π·βπ£)} βͺ {π£ β π β£ Β¬ 2 β₯ (π·βπ£)}) |
10 | 9 | equncomi 4156 |
. . . . . 6
β’ π = ({π£ β π β£ Β¬ 2 β₯ (π·βπ£)} βͺ {π£ β π β£ 2 β₯ (π·βπ£)}) |
11 | 10 | a1i 11 |
. . . . 5
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β π = ({π£ β π β£ Β¬ 2 β₯ (π·βπ£)} βͺ {π£ β π β£ 2 β₯ (π·βπ£)})) |
12 | | simp2 1138 |
. . . . 5
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β π β Fin) |
13 | 3 | fveq1i 6893 |
. . . . . 6
β’ (π·βπ€) = ((VtxDegβπΊ)βπ€) |
14 | | dmfi 9330 |
. . . . . . . . 9
β’ (πΌ β Fin β dom πΌ β Fin) |
15 | 14 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β dom πΌ β Fin) |
16 | | eqid 2733 |
. . . . . . . . 9
β’ dom πΌ = dom πΌ |
17 | 1, 2, 16 | vtxdgfisnn0 28732 |
. . . . . . . 8
β’ ((dom
πΌ β Fin β§ π€ β π) β ((VtxDegβπΊ)βπ€) β
β0) |
18 | 15, 17 | sylan 581 |
. . . . . . 7
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β π) β ((VtxDegβπΊ)βπ€) β
β0) |
19 | 18 | nn0cnd 12534 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β π) β ((VtxDegβπΊ)βπ€) β β) |
20 | 13, 19 | eqeltrid 2838 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β π) β (π·βπ€) β β) |
21 | 8, 11, 12, 20 | fsumsplit 15687 |
. . . 4
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β Ξ£π€ β π (π·βπ€) = (Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€) + Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€))) |
22 | 21 | breq2d 5161 |
. . 3
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β (2 β₯
Ξ£π€ β π (π·βπ€) β 2 β₯ (Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€) + Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€)))) |
23 | | rabfi 9269 |
. . . . . . . . 9
β’ (π β Fin β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} β Fin) |
24 | 23 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} β Fin) |
25 | | elrabi 3678 |
. . . . . . . . . . 11
β’ (π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} β π€ β π) |
26 | 15, 25, 17 | syl2an 597 |
. . . . . . . . . 10
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)}) β ((VtxDegβπΊ)βπ€) β
β0) |
27 | 26 | nn0zd 12584 |
. . . . . . . . 9
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)}) β ((VtxDegβπΊ)βπ€) β β€) |
28 | 13, 27 | eqeltrid 2838 |
. . . . . . . 8
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)}) β (π·βπ€) β β€) |
29 | 24, 28 | fsumzcl 15681 |
. . . . . . 7
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€) β β€) |
30 | 29 | adantr 482 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ Β¬ 2
β₯ (β―β{π£
β π β£ Β¬ 2
β₯ (π·βπ£)})) β Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€) β β€) |
31 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π£ = π€ β (π·βπ£) = (π·βπ€)) |
32 | 31 | breq2d 5161 |
. . . . . . . . . . . . 13
β’ (π£ = π€ β (2 β₯ (π·βπ£) β 2 β₯ (π·βπ€))) |
33 | 32 | notbid 318 |
. . . . . . . . . . . 12
β’ (π£ = π€ β (Β¬ 2 β₯ (π·βπ£) β Β¬ 2 β₯ (π·βπ€))) |
34 | 33 | elrab 3684 |
. . . . . . . . . . 11
β’ (π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} β (π€ β π β§ Β¬ 2 β₯ (π·βπ€))) |
35 | 34 | simprbi 498 |
. . . . . . . . . 10
β’ (π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} β Β¬ 2 β₯ (π·βπ€)) |
36 | 35 | adantl 483 |
. . . . . . . . 9
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)}) β Β¬ 2 β₯ (π·βπ€)) |
37 | 24, 28, 36 | sumodd 16331 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β (2 β₯
(β―β{π£ β
π β£ Β¬ 2 β₯
(π·βπ£)}) β 2 β₯ Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€))) |
38 | 37 | notbid 318 |
. . . . . . 7
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β (Β¬ 2
β₯ (β―β{π£
β π β£ Β¬ 2
β₯ (π·βπ£)}) β Β¬ 2 β₯
Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€))) |
39 | 38 | biimpa 478 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ Β¬ 2
β₯ (β―β{π£
β π β£ Β¬ 2
β₯ (π·βπ£)})) β Β¬ 2 β₯
Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€)) |
40 | | rabfi 9269 |
. . . . . . . . 9
β’ (π β Fin β {π£ β π β£ 2 β₯ (π·βπ£)} β Fin) |
41 | 40 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β {π£ β π β£ 2 β₯ (π·βπ£)} β Fin) |
42 | | elrabi 3678 |
. . . . . . . . . . 11
β’ (π€ β {π£ β π β£ 2 β₯ (π·βπ£)} β π€ β π) |
43 | 15, 42, 17 | syl2an 597 |
. . . . . . . . . 10
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β {π£ β π β£ 2 β₯ (π·βπ£)}) β ((VtxDegβπΊ)βπ€) β
β0) |
44 | 43 | nn0zd 12584 |
. . . . . . . . 9
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β {π£ β π β£ 2 β₯ (π·βπ£)}) β ((VtxDegβπΊ)βπ€) β β€) |
45 | 13, 44 | eqeltrid 2838 |
. . . . . . . 8
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β {π£ β π β£ 2 β₯ (π·βπ£)}) β (π·βπ€) β β€) |
46 | 41, 45 | fsumzcl 15681 |
. . . . . . 7
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€) β β€) |
47 | 46 | adantr 482 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ Β¬ 2
β₯ (β―β{π£
β π β£ Β¬ 2
β₯ (π·βπ£)})) β Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€) β β€) |
48 | 32 | elrab 3684 |
. . . . . . . . . 10
β’ (π€ β {π£ β π β£ 2 β₯ (π·βπ£)} β (π€ β π β§ 2 β₯ (π·βπ€))) |
49 | 48 | simprbi 498 |
. . . . . . . . 9
β’ (π€ β {π£ β π β£ 2 β₯ (π·βπ£)} β 2 β₯ (π·βπ€)) |
50 | 49 | adantl 483 |
. . . . . . . 8
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ π€ β {π£ β π β£ 2 β₯ (π·βπ£)}) β 2 β₯ (π·βπ€)) |
51 | 41, 45, 50 | sumeven 16330 |
. . . . . . 7
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β 2 β₯
Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€)) |
52 | 51 | adantr 482 |
. . . . . 6
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ Β¬ 2
β₯ (β―β{π£
β π β£ Β¬ 2
β₯ (π·βπ£)})) β 2 β₯
Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€)) |
53 | | opeo 16308 |
. . . . . 6
β’
(((Ξ£π€ β
{π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€) β β€ β§ Β¬ 2 β₯
Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€)) β§ (Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€) β β€ β§ 2 β₯ Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€))) β Β¬ 2 β₯ (Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€) + Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€))) |
54 | 30, 39, 47, 52, 53 | syl22anc 838 |
. . . . 5
β’ (((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β§ Β¬ 2
β₯ (β―β{π£
β π β£ Β¬ 2
β₯ (π·βπ£)})) β Β¬ 2 β₯
(Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€) + Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€))) |
55 | 54 | ex 414 |
. . . 4
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β (Β¬ 2
β₯ (β―β{π£
β π β£ Β¬ 2
β₯ (π·βπ£)}) β Β¬ 2 β₯
(Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€) + Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€)))) |
56 | 55 | con4d 115 |
. . 3
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β (2 β₯
(Ξ£π€ β {π£ β π β£ Β¬ 2 β₯ (π·βπ£)} (π·βπ€) + Ξ£π€ β {π£ β π β£ 2 β₯ (π·βπ£)} (π·βπ€)) β 2 β₯ (β―β{π£ β π β£ Β¬ 2 β₯ (π·βπ£)}))) |
57 | 22, 56 | sylbid 239 |
. 2
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β (2 β₯
Ξ£π€ β π (π·βπ€) β 2 β₯ (β―β{π£ β π β£ Β¬ 2 β₯ (π·βπ£)}))) |
58 | 4, 57 | mpd 15 |
1
β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β 2 β₯
(β―β{π£ β
π β£ Β¬ 2 β₯
(π·βπ£)})) |