Step | Hyp | Ref
| Expression |
1 | | cyclprop 28744 |
. . 3
β’ (πΉ(CyclesβπΊ)π β (πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) |
2 | | pthiswlk 28678 |
. . . . 5
β’ (πΉ(PathsβπΊ)π β πΉ(WalksβπΊ)π) |
3 | | upgr3v3e3cycl.e |
. . . . . . . . . 10
β’ πΈ = (EdgβπΊ) |
4 | 3 | upgrwlkvtxedg 28596 |
. . . . . . . . 9
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π) β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ) |
5 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’
((β―βπΉ) =
3 β (πβ(β―βπΉ)) = (πβ3)) |
6 | 5 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ) =
3 β ((πβ0) =
(πβ(β―βπΉ)) β (πβ0) = (πβ3))) |
7 | 6 | anbi2d 630 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) =
3 β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)))) |
8 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’
((β―βπΉ) =
3 β (0..^(β―βπΉ)) = (0..^3)) |
9 | | fzo0to3tp 13659 |
. . . . . . . . . . . . . . . 16
β’ (0..^3) =
{0, 1, 2} |
10 | 8, 9 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’
((β―βπΉ) =
3 β (0..^(β―βπΉ)) = {0, 1, 2}) |
11 | 10 | raleqdv 3314 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ) =
3 β (βπ β
(0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ β βπ β {0, 1, 2} {(πβπ), (πβ(π + 1))} β πΈ)) |
12 | | c0ex 11150 |
. . . . . . . . . . . . . . 15
β’ 0 β
V |
13 | | 1ex 11152 |
. . . . . . . . . . . . . . 15
β’ 1 β
V |
14 | | 2ex 12231 |
. . . . . . . . . . . . . . 15
β’ 2 β
V |
15 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (πβπ) = (πβ0)) |
16 | | fv0p1e1 12277 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (πβ(π + 1)) = (πβ1)) |
17 | 15, 16 | preq12d 4703 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β {(πβπ), (πβ(π + 1))} = {(πβ0), (πβ1)}) |
18 | 17 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β ({(πβπ), (πβ(π + 1))} β πΈ β {(πβ0), (πβ1)} β πΈ)) |
19 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β (πβπ) = (πβ1)) |
20 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 1 β (π + 1) = (1 + 1)) |
21 | | 1p1e2 12279 |
. . . . . . . . . . . . . . . . . . 19
β’ (1 + 1) =
2 |
22 | 20, 21 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 1 β (π + 1) = 2) |
23 | 22 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β (πβ(π + 1)) = (πβ2)) |
24 | 19, 23 | preq12d 4703 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β {(πβπ), (πβ(π + 1))} = {(πβ1), (πβ2)}) |
25 | 24 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β ({(πβπ), (πβ(π + 1))} β πΈ β {(πβ1), (πβ2)} β πΈ)) |
26 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π = 2 β (πβπ) = (πβ2)) |
27 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 2 β (π + 1) = (2 + 1)) |
28 | | 2p1e3 12296 |
. . . . . . . . . . . . . . . . . . 19
β’ (2 + 1) =
3 |
29 | 27, 28 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 2 β (π + 1) = 3) |
30 | 29 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = 2 β (πβ(π + 1)) = (πβ3)) |
31 | 26, 30 | preq12d 4703 |
. . . . . . . . . . . . . . . 16
β’ (π = 2 β {(πβπ), (πβ(π + 1))} = {(πβ2), (πβ3)}) |
32 | 31 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π = 2 β ({(πβπ), (πβ(π + 1))} β πΈ β {(πβ2), (πβ3)} β πΈ)) |
33 | 12, 13, 14, 18, 25, 32 | raltp 4667 |
. . . . . . . . . . . . . 14
β’
(βπ β
{0, 1, 2} {(πβπ), (πβ(π + 1))} β πΈ β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ)) |
34 | 11, 33 | bitrdi 287 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) =
3 β (βπ β
(0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ))) |
35 | 7, 34 | anbi12d 632 |
. . . . . . . . . . . 12
β’
((β―βπΉ) =
3 β (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β§ βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ) β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ)))) |
36 | | upgr3v3e3cycl.v |
. . . . . . . . . . . . . . . . . . 19
β’ π = (VtxβπΊ) |
37 | 36 | wlkp 28567 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ(WalksβπΊ)π β π:(0...(β―βπΉ))βΆπ) |
38 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπΉ) =
3 β (0...(β―βπΉ)) = (0...3)) |
39 | 38 | feq2d 6655 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπΉ) =
3 β (π:(0...(β―βπΉ))βΆπ β π:(0...3)βΆπ)) |
40 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:(0...3)βΆπ β π:(0...3)βΆπ) |
41 | | 3nn0 12432 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 3 β
β0 |
42 | | 0elfz 13539 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (3 β
β0 β 0 β (0...3)) |
43 | 41, 42 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:(0...3)βΆπ β 0 β
(0...3)) |
44 | 40, 43 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π:(0...3)βΆπ β (πβ0) β π) |
45 | | 1nn0 12430 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 β
β0 |
46 | | 1lt3 12327 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 <
3 |
47 | | fvffz0 13560 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((3
β β0 β§ 1 β β0 β§ 1 < 3)
β§ π:(0...3)βΆπ) β (πβ1) β π) |
48 | 47 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((3
β β0 β§ 1 β β0 β§ 1 < 3)
β (π:(0...3)βΆπ β (πβ1) β π)) |
49 | 41, 45, 46, 48 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π:(0...3)βΆπ β (πβ1) β π) |
50 | | 2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
β0 |
51 | | 2lt3 12326 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 <
3 |
52 | | fvffz0 13560 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((3
β β0 β§ 2 β β0 β§ 2 < 3)
β§ π:(0...3)βΆπ) β (πβ2) β π) |
53 | 52 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((3
β β0 β§ 2 β β0 β§ 2 < 3)
β (π:(0...3)βΆπ β (πβ2) β π)) |
54 | 41, 50, 51, 53 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π:(0...3)βΆπ β (πβ2) β π) |
55 | 44, 49, 54 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π:(0...3)βΆπ β ((πβ0) β π β§ (πβ1) β π β§ (πβ2) β π)) |
56 | 39, 55 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπΉ) =
3 β (π:(0...(β―βπΉ))βΆπ β ((πβ0) β π β§ (πβ1) β π β§ (πβ2) β π))) |
57 | 56 | com12 32 |
. . . . . . . . . . . . . . . . . 18
β’ (π:(0...(β―βπΉ))βΆπ β ((β―βπΉ) = 3 β ((πβ0) β π β§ (πβ1) β π β§ (πβ2) β π))) |
58 | 2, 37, 57 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ(PathsβπΊ)π β ((β―βπΉ) = 3 β ((πβ0) β π β§ (πβ1) β π β§ (πβ2) β π))) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β ((β―βπΉ) = 3 β ((πβ0) β π β§ (πβ1) β π β§ (πβ2) β π))) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ)) β ((β―βπΉ) = 3 β ((πβ0) β π β§ (πβ1) β π β§ (πβ2) β π))) |
61 | 60 | impcom 409 |
. . . . . . . . . . . . . 14
β’
(((β―βπΉ)
= 3 β§ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ))) β ((πβ0) β π β§ (πβ1) β π β§ (πβ2) β π)) |
62 | | preq2 4696 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβ3) = (πβ0) β {(πβ2), (πβ3)} = {(πβ2), (πβ0)}) |
63 | 62 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβ0) = (πβ3) β {(πβ2), (πβ3)} = {(πβ2), (πβ0)}) |
64 | 63 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β {(πβ2), (πβ3)} = {(πβ2), (πβ0)}) |
65 | 64 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β ({(πβ2), (πβ3)} β πΈ β {(πβ2), (πβ0)} β πΈ)) |
66 | 65 | 3anbi3d 1443 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ) β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ0)} β πΈ))) |
67 | 66 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ)) β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ0)} β πΈ)) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((β―βπΉ)
= 3 β§ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ))) β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ0)} β πΈ)) |
69 | | simpll 766 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β πΉ(PathsβπΊ)π) |
70 | | breq2 5110 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπΉ) =
3 β (1 < (β―βπΉ) β 1 < 3)) |
71 | 46, 70 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπΉ) =
3 β 1 < (β―βπΉ)) |
72 | 71 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β 1 <
(β―βπΉ)) |
73 | | 3nn 12233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 3 β
β |
74 | | lbfzo0 13613 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (0 β
(0..^3) β 3 β β) |
75 | 73, 74 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β
(0..^3) |
76 | 75, 8 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπΉ) =
3 β 0 β (0..^(β―βπΉ))) |
77 | 76 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β 0 β
(0..^(β―βπΉ))) |
78 | | pthdadjvtx 28681 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ 0 β
(0..^(β―βπΉ)))
β (πβ0) β
(πβ(0 +
1))) |
79 | | 1e0p1 12661 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 = (0 +
1) |
80 | 79 | fveq2i 6846 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πβ1) = (πβ(0 + 1)) |
81 | 80 | neeq2i 3010 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβ0) β (πβ1) β (πβ0) β (πβ(0 +
1))) |
82 | 78, 81 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ 0 β
(0..^(β―βπΉ)))
β (πβ0) β
(πβ1)) |
83 | 69, 72, 77, 82 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β (πβ0) β (πβ1)) |
84 | | elfzo0 13614 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1 β
(0..^3) β (1 β β0 β§ 3 β β β§ 1
< 3)) |
85 | 45, 73, 46, 84 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 1 β
(0..^3) |
86 | 85, 8 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπΉ) =
3 β 1 β (0..^(β―βπΉ))) |
87 | 86 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β 1 β
(0..^(β―βπΉ))) |
88 | | pthdadjvtx 28681 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ 1 β
(0..^(β―βπΉ)))
β (πβ1) β
(πβ(1 +
1))) |
89 | | df-2 12217 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 = (1 +
1) |
90 | 89 | fveq2i 6846 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πβ2) = (πβ(1 + 1)) |
91 | 90 | neeq2i 3010 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβ1) β (πβ2) β (πβ1) β (πβ(1 +
1))) |
92 | 88, 91 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ 1 β
(0..^(β―βπΉ)))
β (πβ1) β
(πβ2)) |
93 | 69, 72, 87, 92 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β (πβ1) β (πβ2)) |
94 | | elfzo0 13614 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (2 β
(0..^3) β (2 β β0 β§ 3 β β β§ 2
< 3)) |
95 | 50, 73, 51, 94 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
(0..^3) |
96 | 95, 8 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπΉ) =
3 β 2 β (0..^(β―βπΉ))) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β 2 β
(0..^(β―βπΉ))) |
98 | | pthdadjvtx 28681 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ 2 β
(0..^(β―βπΉ)))
β (πβ2) β
(πβ(2 +
1))) |
99 | 69, 72, 97, 98 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β (πβ2) β (πβ(2 + 1))) |
100 | | neeq2 3008 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πβ0) = (πβ3) β ((πβ2) β (πβ0) β (πβ2) β (πβ3))) |
101 | | df-3 12218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 3 = (2 +
1) |
102 | 101 | fveq2i 6846 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πβ3) = (πβ(2 + 1)) |
103 | 102 | neeq2i 3010 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πβ2) β (πβ3) β (πβ2) β (πβ(2 +
1))) |
104 | 100, 103 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβ0) = (πβ3) β ((πβ2) β (πβ0) β (πβ2) β (πβ(2 + 1)))) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β ((πβ2) β (πβ0) β (πβ2) β (πβ(2 + 1)))) |
106 | 105 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β ((πβ2) β (πβ0) β (πβ2) β (πβ(2 +
1)))) |
107 | 99, 106 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β (πβ2) β (πβ0)) |
108 | 83, 93, 107 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ (β―βπΉ) = 3) β ((πβ0) β (πβ1) β§ (πβ1) β (πβ2) β§ (πβ2) β (πβ0))) |
109 | 108 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β ((β―βπΉ) = 3 β ((πβ0) β (πβ1) β§ (πβ1) β (πβ2) β§ (πβ2) β (πβ0)))) |
110 | 109 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ)) β ((β―βπΉ) = 3 β ((πβ0) β (πβ1) β§ (πβ1) β (πβ2) β§ (πβ2) β (πβ0)))) |
111 | 110 | impcom 409 |
. . . . . . . . . . . . . 14
β’
(((β―βπΉ)
= 3 β§ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ))) β ((πβ0) β (πβ1) β§ (πβ1) β (πβ2) β§ (πβ2) β (πβ0))) |
112 | | preq1 4695 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ0) β {π, π} = {(πβ0), π}) |
113 | 112 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ0) β ({π, π} β πΈ β {(πβ0), π} β πΈ)) |
114 | | preq2 4696 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ0) β {π, π} = {π, (πβ0)}) |
115 | 114 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ0) β ({π, π} β πΈ β {π, (πβ0)} β πΈ)) |
116 | 113, 115 | 3anbi13d 1439 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ0) β (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β ({(πβ0), π} β πΈ β§ {π, π} β πΈ β§ {π, (πβ0)} β πΈ))) |
117 | | neeq1 3007 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ0) β (π β π β (πβ0) β π)) |
118 | | neeq2 3008 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ0) β (π β π β π β (πβ0))) |
119 | 117, 118 | 3anbi13d 1439 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ0) β ((π β π β§ π β π β§ π β π) β ((πβ0) β π β§ π β π β§ π β (πβ0)))) |
120 | 116, 119 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = (πβ0) β ((({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)) β (({(πβ0), π} β πΈ β§ {π, π} β πΈ β§ {π, (πβ0)} β πΈ) β§ ((πβ0) β π β§ π β π β§ π β (πβ0))))) |
121 | | preq2 4696 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ1) β {(πβ0), π} = {(πβ0), (πβ1)}) |
122 | 121 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ1) β ({(πβ0), π} β πΈ β {(πβ0), (πβ1)} β πΈ)) |
123 | | preq1 4695 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ1) β {π, π} = {(πβ1), π}) |
124 | 123 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ1) β ({π, π} β πΈ β {(πβ1), π} β πΈ)) |
125 | 122, 124 | 3anbi12d 1438 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ1) β (({(πβ0), π} β πΈ β§ {π, π} β πΈ β§ {π, (πβ0)} β πΈ) β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ β§ {π, (πβ0)} β πΈ))) |
126 | | neeq2 3008 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ1) β ((πβ0) β π β (πβ0) β (πβ1))) |
127 | | neeq1 3007 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ1) β (π β π β (πβ1) β π)) |
128 | 126, 127 | 3anbi12d 1438 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ1) β (((πβ0) β π β§ π β π β§ π β (πβ0)) β ((πβ0) β (πβ1) β§ (πβ1) β π β§ π β (πβ0)))) |
129 | 125, 128 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = (πβ1) β ((({(πβ0), π} β πΈ β§ {π, π} β πΈ β§ {π, (πβ0)} β πΈ) β§ ((πβ0) β π β§ π β π β§ π β (πβ0))) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ β§ {π, (πβ0)} β πΈ) β§ ((πβ0) β (πβ1) β§ (πβ1) β π β§ π β (πβ0))))) |
130 | | preq2 4696 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ2) β {(πβ1), π} = {(πβ1), (πβ2)}) |
131 | 130 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ2) β ({(πβ1), π} β πΈ β {(πβ1), (πβ2)} β πΈ)) |
132 | | preq1 4695 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ2) β {π, (πβ0)} = {(πβ2), (πβ0)}) |
133 | 132 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ2) β ({π, (πβ0)} β πΈ β {(πβ2), (πβ0)} β πΈ)) |
134 | 131, 133 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ2) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ β§ {π, (πβ0)} β πΈ) β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ0)} β πΈ))) |
135 | | neeq2 3008 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ2) β ((πβ1) β π β (πβ1) β (πβ2))) |
136 | | neeq1 3007 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ2) β (π β (πβ0) β (πβ2) β (πβ0))) |
137 | 135, 136 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ2) β (((πβ0) β (πβ1) β§ (πβ1) β π β§ π β (πβ0)) β ((πβ0) β (πβ1) β§ (πβ1) β (πβ2) β§ (πβ2) β (πβ0)))) |
138 | 134, 137 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = (πβ2) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ β§ {π, (πβ0)} β πΈ) β§ ((πβ0) β (πβ1) β§ (πβ1) β π β§ π β (πβ0))) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ0)} β πΈ) β§ ((πβ0) β (πβ1) β§ (πβ1) β (πβ2) β§ (πβ2) β (πβ0))))) |
139 | 120, 129,
138 | rspc3ev 3595 |
. . . . . . . . . . . . . 14
β’ ((((πβ0) β π β§ (πβ1) β π β§ (πβ2) β π) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ0)} β πΈ) β§ ((πβ0) β (πβ1) β§ (πβ1) β (πβ2) β§ (πβ2) β (πβ0)))) β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))) |
140 | 61, 68, 111, 139 | syl12anc 836 |
. . . . . . . . . . . . 13
β’
(((β―βπΉ)
= 3 β§ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ))) β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))) |
141 | 140 | ex 414 |
. . . . . . . . . . . 12
β’
((β―βπΉ) =
3 β (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ3)) β§ ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ β§ {(πβ2), (πβ3)} β πΈ)) β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)))) |
142 | 35, 141 | sylbid 239 |
. . . . . . . . . . 11
β’
((β―βπΉ) =
3 β (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β§ βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ) β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)))) |
143 | 142 | expd 417 |
. . . . . . . . . 10
β’
((β―βπΉ) =
3 β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))))) |
144 | 143 | com13 88 |
. . . . . . . . 9
β’
(βπ β
(0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β ((β―βπΉ) = 3 β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))))) |
145 | 4, 144 | syl 17 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π) β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β ((β―βπΉ) = 3 β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))))) |
146 | 145 | expcom 415 |
. . . . . . 7
β’ (πΉ(WalksβπΊ)π β (πΊ β UPGraph β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β ((β―βπΉ) = 3 β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)))))) |
147 | 146 | com23 86 |
. . . . . 6
β’ (πΉ(WalksβπΊ)π β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (πΊ β UPGraph β ((β―βπΉ) = 3 β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)))))) |
148 | 147 | expd 417 |
. . . . 5
β’ (πΉ(WalksβπΊ)π β (πΉ(PathsβπΊ)π β ((πβ0) = (πβ(β―βπΉ)) β (πΊ β UPGraph β ((β―βπΉ) = 3 β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))))))) |
149 | 2, 148 | mpcom 38 |
. . . 4
β’ (πΉ(PathsβπΊ)π β ((πβ0) = (πβ(β―βπΉ)) β (πΊ β UPGraph β ((β―βπΉ) = 3 β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)))))) |
150 | 149 | imp 408 |
. . 3
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (πΊ β UPGraph β ((β―βπΉ) = 3 β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))))) |
151 | 1, 150 | syl 17 |
. 2
β’ (πΉ(CyclesβπΊ)π β (πΊ β UPGraph β ((β―βπΉ) = 3 β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))))) |
152 | 151 | 3imp21 1115 |
1
β’ ((πΊ β UPGraph β§ πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 3) β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))) |