Step | Hyp | Ref
| Expression |
1 | | 2pthnloop.i |
. . . 4
β’ πΌ = (iEdgβπΊ) |
2 | 1 | 2pthnloop 28728 |
. . 3
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ)) β βπ β
(0..^(β―βπΉ))2
β€ (β―β(πΌβ(πΉβπ)))) |
3 | 2 | 3adant1 1131 |
. 2
β’ ((πΊ β UPGraph β§ πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ)) β βπ β
(0..^(β―βπΉ))2
β€ (β―β(πΌβ(πΉβπ)))) |
4 | | pthiswlk 28724 |
. . . . . . 7
β’ (πΉ(PathsβπΊ)π β πΉ(WalksβπΊ)π) |
5 | 1 | wlkf 28611 |
. . . . . . 7
β’ (πΉ(WalksβπΊ)π β πΉ β Word dom πΌ) |
6 | | simp2 1138 |
. . . . . . . . . 10
β’ ((πΉ β Word dom πΌ β§ πΊ β UPGraph β§ π β (0..^(β―βπΉ))) β πΊ β UPGraph) |
7 | | wrdsymbcl 14424 |
. . . . . . . . . 10
β’ ((πΉ β Word dom πΌ β§ π β (0..^(β―βπΉ))) β (πΉβπ) β dom πΌ) |
8 | 1 | upgrle2 28105 |
. . . . . . . . . 10
β’ ((πΊ β UPGraph β§ (πΉβπ) β dom πΌ) β (β―β(πΌβ(πΉβπ))) β€ 2) |
9 | 6, 7, 8 | 3imp3i2an 1346 |
. . . . . . . . 9
β’ ((πΉ β Word dom πΌ β§ πΊ β UPGraph β§ π β (0..^(β―βπΉ))) β (β―β(πΌβ(πΉβπ))) β€ 2) |
10 | | fvex 6859 |
. . . . . . . . . . . . 13
β’ (πΌβ(πΉβπ)) β V |
11 | | hashxnn0 14248 |
. . . . . . . . . . . . 13
β’ ((πΌβ(πΉβπ)) β V β (β―β(πΌβ(πΉβπ))) β
β0*) |
12 | | xnn0xr 12498 |
. . . . . . . . . . . . 13
β’
((β―β(πΌβ(πΉβπ))) β β0*
β (β―β(πΌβ(πΉβπ))) β
β*) |
13 | 10, 11, 12 | mp2b 10 |
. . . . . . . . . . . 12
β’
(β―β(πΌβ(πΉβπ))) β
β* |
14 | | 2re 12235 |
. . . . . . . . . . . . 13
β’ 2 β
β |
15 | 14 | rexri 11221 |
. . . . . . . . . . . 12
β’ 2 β
β* |
16 | 13, 15 | pm3.2i 472 |
. . . . . . . . . . 11
β’
((β―β(πΌβ(πΉβπ))) β β* β§ 2 β
β*) |
17 | | xrletri3 13082 |
. . . . . . . . . . 11
β’
(((β―β(πΌβ(πΉβπ))) β β* β§ 2 β
β*) β ((β―β(πΌβ(πΉβπ))) = 2 β ((β―β(πΌβ(πΉβπ))) β€ 2 β§ 2 β€ (β―β(πΌβ(πΉβπ)))))) |
18 | 16, 17 | mp1i 13 |
. . . . . . . . . 10
β’ ((πΉ β Word dom πΌ β§ πΊ β UPGraph β§ π β (0..^(β―βπΉ))) β ((β―β(πΌβ(πΉβπ))) = 2 β ((β―β(πΌβ(πΉβπ))) β€ 2 β§ 2 β€ (β―β(πΌβ(πΉβπ)))))) |
19 | 18 | biimprd 248 |
. . . . . . . . 9
β’ ((πΉ β Word dom πΌ β§ πΊ β UPGraph β§ π β (0..^(β―βπΉ))) β (((β―β(πΌβ(πΉβπ))) β€ 2 β§ 2 β€ (β―β(πΌβ(πΉβπ)))) β (β―β(πΌβ(πΉβπ))) = 2)) |
20 | 9, 19 | mpand 694 |
. . . . . . . 8
β’ ((πΉ β Word dom πΌ β§ πΊ β UPGraph β§ π β (0..^(β―βπΉ))) β (2 β€ (β―β(πΌβ(πΉβπ))) β (β―β(πΌβ(πΉβπ))) = 2)) |
21 | 20 | 3exp 1120 |
. . . . . . 7
β’ (πΉ β Word dom πΌ β (πΊ β UPGraph β (π β (0..^(β―βπΉ)) β (2 β€ (β―β(πΌβ(πΉβπ))) β (β―β(πΌβ(πΉβπ))) = 2)))) |
22 | 4, 5, 21 | 3syl 18 |
. . . . . 6
β’ (πΉ(PathsβπΊ)π β (πΊ β UPGraph β (π β (0..^(β―βπΉ)) β (2 β€ (β―β(πΌβ(πΉβπ))) β (β―β(πΌβ(πΉβπ))) = 2)))) |
23 | 22 | impcom 409 |
. . . . 5
β’ ((πΊ β UPGraph β§ πΉ(PathsβπΊ)π) β (π β (0..^(β―βπΉ)) β (2 β€ (β―β(πΌβ(πΉβπ))) β (β―β(πΌβ(πΉβπ))) = 2))) |
24 | 23 | 3adant3 1133 |
. . . 4
β’ ((πΊ β UPGraph β§ πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ)) β (π β (0..^(β―βπΉ)) β (2 β€ (β―β(πΌβ(πΉβπ))) β (β―β(πΌβ(πΉβπ))) = 2))) |
25 | 24 | imp 408 |
. . 3
β’ (((πΊ β UPGraph β§ πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ)) β§ π β (0..^(β―βπΉ))) β (2 β€ (β―β(πΌβ(πΉβπ))) β (β―β(πΌβ(πΉβπ))) = 2)) |
26 | 25 | ralimdva 3161 |
. 2
β’ ((πΊ β UPGraph β§ πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ)) β (βπ β
(0..^(β―βπΉ))2
β€ (β―β(πΌβ(πΉβπ))) β βπ β (0..^(β―βπΉ))(β―β(πΌβ(πΉβπ))) = 2)) |
27 | 3, 26 | mpd 15 |
1
β’ ((πΊ β UPGraph β§ πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ)) β βπ β
(0..^(β―βπΉ))(β―β(πΌβ(πΉβπ))) = 2) |