Step | Hyp | Ref
| Expression |
1 | | cycliswlk 28532 |
. . . . . . . 8
β’ (πΉ(CyclesβπΊ)π β πΉ(WalksβπΊ)π) |
2 | | wlkcl 28349 |
. . . . . . . 8
β’ (πΉ(WalksβπΊ)π β (β―βπΉ) β
β0) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (πΉ(CyclesβπΊ)π β (β―βπΉ) β
β0) |
4 | 3 | nn0red 12408 |
. . . . . 6
β’ (πΉ(CyclesβπΊ)π β (β―βπΉ) β β) |
5 | 4 | adantr 482 |
. . . . 5
β’ ((πΉ(CyclesβπΊ)π β§ πΉ β β
) β (β―βπΉ) β
β) |
6 | 2 | nn0ge0d 12410 |
. . . . . . 7
β’ (πΉ(WalksβπΊ)π β 0 β€ (β―βπΉ)) |
7 | 1, 6 | syl 17 |
. . . . . 6
β’ (πΉ(CyclesβπΊ)π β 0 β€ (β―βπΉ)) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((πΉ(CyclesβπΊ)π β§ πΉ β β
) β 0 β€
(β―βπΉ)) |
9 | | relwlk 28360 |
. . . . . . . 8
β’ Rel
(WalksβπΊ) |
10 | 9 | brrelex1i 5685 |
. . . . . . 7
β’ (πΉ(WalksβπΊ)π β πΉ β V) |
11 | | hasheq0 14191 |
. . . . . . . . 9
β’ (πΉ β V β
((β―βπΉ) = 0
β πΉ =
β
)) |
12 | 11 | necon3bid 2987 |
. . . . . . . 8
β’ (πΉ β V β
((β―βπΉ) β 0
β πΉ β
β
)) |
13 | 12 | bicomd 222 |
. . . . . . 7
β’ (πΉ β V β (πΉ β β
β
(β―βπΉ) β
0)) |
14 | 1, 10, 13 | 3syl 18 |
. . . . . 6
β’ (πΉ(CyclesβπΊ)π β (πΉ β β
β (β―βπΉ) β 0)) |
15 | 14 | biimpa 478 |
. . . . 5
β’ ((πΉ(CyclesβπΊ)π β§ πΉ β β
) β (β―βπΉ) β 0) |
16 | 5, 8, 15 | ne0gt0d 11226 |
. . . 4
β’ ((πΉ(CyclesβπΊ)π β§ πΉ β β
) β 0 <
(β―βπΉ)) |
17 | 16 | 3adant1 1131 |
. . 3
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π β§ πΉ β β
) β 0 <
(β―βπΉ)) |
18 | | usgrumgr 27916 |
. . . . 5
β’ (πΊ β USGraph β πΊ β
UMGraph) |
19 | | umgrn1cycl 28538 |
. . . . 5
β’ ((πΊ β UMGraph β§ πΉ(CyclesβπΊ)π) β (β―βπΉ) β 1) |
20 | 18, 19 | sylan 581 |
. . . 4
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π) β (β―βπΉ) β 1) |
21 | 20 | 3adant3 1133 |
. . 3
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π β§ πΉ β β
) β (β―βπΉ) β 1) |
22 | | 0nn0 12362 |
. . . . . 6
β’ 0 β
β0 |
23 | | nn0ltp1ne 33463 |
. . . . . 6
β’ ((0
β β0 β§ (β―βπΉ) β β0) β ((0 +
1) < (β―βπΉ)
β (0 < (β―βπΉ) β§ (β―βπΉ) β (0 + 1)))) |
24 | 22, 3, 23 | sylancr 588 |
. . . . 5
β’ (πΉ(CyclesβπΊ)π β ((0 + 1) < (β―βπΉ) β (0 <
(β―βπΉ) β§
(β―βπΉ) β (0 +
1)))) |
25 | | 0p1e1 12209 |
. . . . . 6
β’ (0 + 1) =
1 |
26 | 25 | breq1i 5111 |
. . . . 5
β’ ((0 + 1)
< (β―βπΉ)
β 1 < (β―βπΉ)) |
27 | 25 | neeq2i 3008 |
. . . . . 6
β’
((β―βπΉ)
β (0 + 1) β (β―βπΉ) β 1) |
28 | 27 | anbi2i 624 |
. . . . 5
β’ ((0 <
(β―βπΉ) β§
(β―βπΉ) β (0 +
1)) β (0 < (β―βπΉ) β§ (β―βπΉ) β 1)) |
29 | 24, 26, 28 | 3bitr3g 313 |
. . . 4
β’ (πΉ(CyclesβπΊ)π β (1 < (β―βπΉ) β (0 <
(β―βπΉ) β§
(β―βπΉ) β
1))) |
30 | 29 | 3ad2ant2 1135 |
. . 3
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π β§ πΉ β β
) β (1 <
(β―βπΉ) β (0
< (β―βπΉ)
β§ (β―βπΉ)
β 1))) |
31 | 17, 21, 30 | mpbir2and 712 |
. 2
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π β§ πΉ β β
) β 1 <
(β―βπΉ)) |
32 | | usgrn2cycl 28540 |
. . 3
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π) β (β―βπΉ) β 2) |
33 | 32 | 3adant3 1133 |
. 2
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π β§ πΉ β β
) β (β―βπΉ) β 2) |
34 | | df-2 12150 |
. . . . . 6
β’ 2 = (1 +
1) |
35 | 34 | breq1i 5111 |
. . . . 5
β’ (2 <
(β―βπΉ) β (1
+ 1) < (β―βπΉ)) |
36 | | 1nn0 12363 |
. . . . . 6
β’ 1 β
β0 |
37 | | nn0ltp1ne 33463 |
. . . . . 6
β’ ((1
β β0 β§ (β―βπΉ) β β0) β ((1 +
1) < (β―βπΉ)
β (1 < (β―βπΉ) β§ (β―βπΉ) β (1 + 1)))) |
38 | 36, 3, 37 | sylancr 588 |
. . . . 5
β’ (πΉ(CyclesβπΊ)π β ((1 + 1) < (β―βπΉ) β (1 <
(β―βπΉ) β§
(β―βπΉ) β (1 +
1)))) |
39 | 35, 38 | bitrid 283 |
. . . 4
β’ (πΉ(CyclesβπΊ)π β (2 < (β―βπΉ) β (1 <
(β―βπΉ) β§
(β―βπΉ) β (1 +
1)))) |
40 | 39 | 3ad2ant2 1135 |
. . 3
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π β§ πΉ β β
) β (2 <
(β―βπΉ) β (1
< (β―βπΉ)
β§ (β―βπΉ)
β (1 + 1)))) |
41 | 34 | neeq2i 3008 |
. . . 4
β’
((β―βπΉ)
β 2 β (β―βπΉ) β (1 + 1)) |
42 | 41 | anbi2i 624 |
. . 3
β’ ((1 <
(β―βπΉ) β§
(β―βπΉ) β 2)
β (1 < (β―βπΉ) β§ (β―βπΉ) β (1 + 1))) |
43 | 40, 42 | bitr4di 289 |
. 2
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π β§ πΉ β β
) β (2 <
(β―βπΉ) β (1
< (β―βπΉ)
β§ (β―βπΉ)
β 2))) |
44 | 31, 33, 43 | mpbir2and 712 |
1
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π β§ πΉ β β
) β 2 <
(β―βπΉ)) |