Step | Hyp | Ref
| Expression |
1 | | isacycgr 33803 |
. . 3
β’ (πΊ β ComplUSGraph β
(πΊ β AcyclicGraph
β Β¬ βπβπ(π(CyclesβπΊ)π β§ π β β
))) |
2 | | 3nn0 12439 |
. . . . . . 7
β’ 3 β
β0 |
3 | | cusgracyclt3v.1 |
. . . . . . . . 9
β’ π = (VtxβπΊ) |
4 | 3 | fvexi 6860 |
. . . . . . . 8
β’ π β V |
5 | | hashxnn0 14248 |
. . . . . . . 8
β’ (π β V β
(β―βπ) β
β0*) |
6 | 4, 5 | ax-mp 5 |
. . . . . . 7
β’
(β―βπ)
β β0* |
7 | | xnn0lem1lt 13172 |
. . . . . . 7
β’ ((3
β β0 β§ (β―βπ) β β0*)
β (3 β€ (β―βπ) β (3 β 1) <
(β―βπ))) |
8 | 2, 6, 7 | mp2an 691 |
. . . . . 6
β’ (3 β€
(β―βπ) β (3
β 1) < (β―βπ)) |
9 | | 3re 12241 |
. . . . . . . 8
β’ 3 β
β |
10 | 9 | rexri 11221 |
. . . . . . 7
β’ 3 β
β* |
11 | | xnn0xr 12498 |
. . . . . . . 8
β’
((β―βπ)
β β0* β (β―βπ) β
β*) |
12 | 6, 11 | ax-mp 5 |
. . . . . . 7
β’
(β―βπ)
β β* |
13 | | xrlenlt 11228 |
. . . . . . 7
β’ ((3
β β* β§ (β―βπ) β β*) β (3 β€
(β―βπ) β
Β¬ (β―βπ)
< 3)) |
14 | 10, 12, 13 | mp2an 691 |
. . . . . 6
β’ (3 β€
(β―βπ) β
Β¬ (β―βπ)
< 3) |
15 | | 3m1e2 12289 |
. . . . . . 7
β’ (3
β 1) = 2 |
16 | 15 | breq1i 5116 |
. . . . . 6
β’ ((3
β 1) < (β―βπ) β 2 < (β―βπ)) |
17 | 8, 14, 16 | 3bitr3i 301 |
. . . . 5
β’ (Β¬
(β―βπ) < 3
β 2 < (β―βπ)) |
18 | 3 | cusgr3cyclex 33794 |
. . . . . . 7
β’ ((πΊ β ComplUSGraph β§ 2
< (β―βπ))
β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
19 | | 3ne0 12267 |
. . . . . . . . . . 11
β’ 3 β
0 |
20 | | neeq1 3003 |
. . . . . . . . . . 11
β’
((β―βπ) =
3 β ((β―βπ)
β 0 β 3 β 0)) |
21 | 19, 20 | mpbiri 258 |
. . . . . . . . . 10
β’
((β―βπ) =
3 β (β―βπ)
β 0) |
22 | | hasheq0 14272 |
. . . . . . . . . . . 12
β’ (π β V β
((β―βπ) = 0
β π =
β
)) |
23 | 22 | elv 3453 |
. . . . . . . . . . 11
β’
((β―βπ) =
0 β π =
β
) |
24 | 23 | necon3bii 2993 |
. . . . . . . . . 10
β’
((β―βπ)
β 0 β π β
β
) |
25 | 21, 24 | sylib 217 |
. . . . . . . . 9
β’
((β―βπ) =
3 β π β
β
) |
26 | 25 | anim2i 618 |
. . . . . . . 8
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 3) β (π(CyclesβπΊ)π β§ π β β
)) |
27 | 26 | 2eximi 1839 |
. . . . . . 7
β’
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπβπ(π(CyclesβπΊ)π β§ π β β
)) |
28 | 18, 27 | syl 17 |
. . . . . 6
β’ ((πΊ β ComplUSGraph β§ 2
< (β―βπ))
β βπβπ(π(CyclesβπΊ)π β§ π β β
)) |
29 | 28 | ex 414 |
. . . . 5
β’ (πΊ β ComplUSGraph β (2
< (β―βπ)
β βπβπ(π(CyclesβπΊ)π β§ π β β
))) |
30 | 17, 29 | biimtrid 241 |
. . . 4
β’ (πΊ β ComplUSGraph β
(Β¬ (β―βπ)
< 3 β βπβπ(π(CyclesβπΊ)π β§ π β β
))) |
31 | 30 | con1d 145 |
. . 3
β’ (πΊ β ComplUSGraph β
(Β¬ βπβπ(π(CyclesβπΊ)π β§ π β β
) β (β―βπ) < 3)) |
32 | 1, 31 | sylbid 239 |
. 2
β’ (πΊ β ComplUSGraph β
(πΊ β AcyclicGraph
β (β―βπ)
< 3)) |
33 | | cusgrusgr 28416 |
. . . . . . 7
β’ (πΊ β ComplUSGraph β
πΊ β
USGraph) |
34 | 3 | usgrcyclgt2v 33789 |
. . . . . . . 8
β’ ((πΊ β USGraph β§ π(CyclesβπΊ)π β§ π β β
) β 2 <
(β―βπ)) |
35 | 34 | 3expib 1123 |
. . . . . . 7
β’ (πΊ β USGraph β ((π(CyclesβπΊ)π β§ π β β
) β 2 <
(β―βπ))) |
36 | 33, 35 | syl 17 |
. . . . . 6
β’ (πΊ β ComplUSGraph β
((π(CyclesβπΊ)π β§ π β β
) β 2 <
(β―βπ))) |
37 | 36, 17 | syl6ibr 252 |
. . . . 5
β’ (πΊ β ComplUSGraph β
((π(CyclesβπΊ)π β§ π β β
) β Β¬
(β―βπ) <
3)) |
38 | 37 | exlimdvv 1938 |
. . . 4
β’ (πΊ β ComplUSGraph β
(βπβπ(π(CyclesβπΊ)π β§ π β β
) β Β¬
(β―βπ) <
3)) |
39 | 38 | con2d 134 |
. . 3
β’ (πΊ β ComplUSGraph β
((β―βπ) < 3
β Β¬ βπβπ(π(CyclesβπΊ)π β§ π β β
))) |
40 | 39, 1 | sylibrd 259 |
. 2
β’ (πΊ β ComplUSGraph β
((β―βπ) < 3
β πΊ β
AcyclicGraph)) |
41 | 32, 40 | impbid 211 |
1
β’ (πΊ β ComplUSGraph β
(πΊ β AcyclicGraph
β (β―βπ)
< 3)) |