Step | Hyp | Ref
| Expression |
1 | | isacycgr 34678 |
. . 3
β’ (πΊ β ComplUSGraph β
(πΊ β AcyclicGraph
β Β¬ βπβπ(π(CyclesβπΊ)π β§ π β β
))) |
2 | | 3nn0 12506 |
. . . . . . 7
β’ 3 β
β0 |
3 | | cusgracyclt3v.1 |
. . . . . . . . 9
β’ π = (VtxβπΊ) |
4 | 3 | fvexi 6905 |
. . . . . . . 8
β’ π β V |
5 | | hashxnn0 14316 |
. . . . . . . 8
β’ (π β V β
(β―βπ) β
β0*) |
6 | 4, 5 | ax-mp 5 |
. . . . . . 7
β’
(β―βπ)
β β0* |
7 | | xnn0lem1lt 13241 |
. . . . . . 7
β’ ((3
β β0 β§ (β―βπ) β β0*)
β (3 β€ (β―βπ) β (3 β 1) <
(β―βπ))) |
8 | 2, 6, 7 | mp2an 691 |
. . . . . 6
β’ (3 β€
(β―βπ) β (3
β 1) < (β―βπ)) |
9 | | 3re 12308 |
. . . . . . . 8
β’ 3 β
β |
10 | 9 | rexri 11288 |
. . . . . . 7
β’ 3 β
β* |
11 | | xnn0xr 12565 |
. . . . . . . 8
β’
((β―βπ)
β β0* β (β―βπ) β
β*) |
12 | 6, 11 | ax-mp 5 |
. . . . . . 7
β’
(β―βπ)
β β* |
13 | | xrlenlt 11295 |
. . . . . . 7
β’ ((3
β β* β§ (β―βπ) β β*) β (3 β€
(β―βπ) β
Β¬ (β―βπ)
< 3)) |
14 | 10, 12, 13 | mp2an 691 |
. . . . . 6
β’ (3 β€
(β―βπ) β
Β¬ (β―βπ)
< 3) |
15 | | 3m1e2 12356 |
. . . . . . 7
β’ (3
β 1) = 2 |
16 | 15 | breq1i 5149 |
. . . . . 6
β’ ((3
β 1) < (β―βπ) β 2 < (β―βπ)) |
17 | 8, 14, 16 | 3bitr3i 301 |
. . . . 5
β’ (Β¬
(β―βπ) < 3
β 2 < (β―βπ)) |
18 | 3 | cusgr3cyclex 34669 |
. . . . . . 7
β’ ((πΊ β ComplUSGraph β§ 2
< (β―βπ))
β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
19 | | 3ne0 12334 |
. . . . . . . . . . 11
β’ 3 β
0 |
20 | | neeq1 2998 |
. . . . . . . . . . 11
β’
((β―βπ) =
3 β ((β―βπ)
β 0 β 3 β 0)) |
21 | 19, 20 | mpbiri 258 |
. . . . . . . . . 10
β’
((β―βπ) =
3 β (β―βπ)
β 0) |
22 | | hasheq0 14340 |
. . . . . . . . . . . 12
β’ (π β V β
((β―βπ) = 0
β π =
β
)) |
23 | 22 | elv 3475 |
. . . . . . . . . . 11
β’
((β―βπ) =
0 β π =
β
) |
24 | 23 | necon3bii 2988 |
. . . . . . . . . 10
β’
((β―βπ)
β 0 β π β
β
) |
25 | 21, 24 | sylib 217 |
. . . . . . . . 9
β’
((β―βπ) =
3 β π β
β
) |
26 | 25 | anim2i 616 |
. . . . . . . 8
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 3) β (π(CyclesβπΊ)π β§ π β β
)) |
27 | 26 | 2eximi 1831 |
. . . . . . 7
β’
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπβπ(π(CyclesβπΊ)π β§ π β β
)) |
28 | 18, 27 | syl 17 |
. . . . . 6
β’ ((πΊ β ComplUSGraph β§ 2
< (β―βπ))
β βπβπ(π(CyclesβπΊ)π β§ π β β
)) |
29 | 28 | ex 412 |
. . . . 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 29206 |
. . . . . . 7
β’ (πΊ β ComplUSGraph β
πΊ β
USGraph) |
34 | 3 | usgrcyclgt2v 34664 |
. . . . . . . 8
β’ ((πΊ β USGraph β§ π(CyclesβπΊ)π β§ π β β
) β 2 <
(β―βπ)) |
35 | 34 | 3expib 1120 |
. . . . . . 7
β’ (πΊ β USGraph β ((π(CyclesβπΊ)π β§ π β β
) β 2 <
(β―βπ))) |
36 | 33, 35 | syl 17 |
. . . . . 6
β’ (πΊ β ComplUSGraph β
((π(CyclesβπΊ)π β§ π β β
) β 2 <
(β―βπ))) |
37 | 36, 17 | imbitrrdi 251 |
. . . . 5
β’ (πΊ β ComplUSGraph β
((π(CyclesβπΊ)π β§ π β β
) β Β¬
(β―βπ) <
3)) |
38 | 37 | exlimdvv 1930 |
. . . 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)) |