Step | Hyp | Ref
| Expression |
1 | | cyclprop 28744 |
. . 3
β’ (πΉ(CyclesβπΊ)π β (πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) |
2 | | pthiswlk 28678 |
. . . . 5
β’ (πΉ(PathsβπΊ)π β πΉ(WalksβπΊ)π) |
3 | | upgr4cycl4dv4e.e |
. . . . . . . . . 10
β’ πΈ = (EdgβπΊ) |
4 | 3 | upgrwlkvtxedg 28596 |
. . . . . . . . 9
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π) β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ) |
5 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’
((β―βπΉ) =
4 β (πβ(β―βπΉ)) = (πβ4)) |
6 | 5 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ) =
4 β ((πβ0) =
(πβ(β―βπΉ)) β (πβ0) = (πβ4))) |
7 | 6 | anbi2d 630 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) =
4 β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (πΉ(PathsβπΊ)π β§ (πβ0) = (πβ4)))) |
8 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’
((β―βπΉ) =
4 β (0..^(β―βπΉ)) = (0..^4)) |
9 | | fzo0to42pr 13660 |
. . . . . . . . . . . . . . . 16
β’ (0..^4) =
({0, 1} βͺ {2, 3}) |
10 | 8, 9 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’
((β―βπΉ) =
4 β (0..^(β―βπΉ)) = ({0, 1} βͺ {2, 3})) |
11 | 10 | raleqdv 3314 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ) =
4 β (βπ β
(0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ β βπ β ({0, 1} βͺ {2, 3}){(πβπ), (πβ(π + 1))} β πΈ)) |
12 | | ralunb 4152 |
. . . . . . . . . . . . . . 15
β’
(βπ β
({0, 1} βͺ {2, 3}){(πβπ), (πβ(π + 1))} β πΈ β (βπ β {0, 1} {(πβπ), (πβ(π + 1))} β πΈ β§ βπ β {2, 3} {(πβπ), (πβ(π + 1))} β πΈ)) |
13 | | c0ex 11150 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
V |
14 | | 1ex 11152 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
V |
15 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (πβπ) = (πβ0)) |
16 | | fv0p1e1 12277 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (πβ(π + 1)) = (πβ1)) |
17 | 15, 16 | preq12d 4703 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β {(πβπ), (πβ(π + 1))} = {(πβ0), (πβ1)}) |
18 | 17 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β ({(πβπ), (πβ(π + 1))} β πΈ β {(πβ0), (πβ1)} β πΈ)) |
19 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 1 β (πβπ) = (πβ1)) |
20 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 1 β (π + 1) = (1 + 1)) |
21 | | 1p1e2 12279 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 + 1) =
2 |
22 | 20, 21 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 1 β (π + 1) = 2) |
23 | 22 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 1 β (πβ(π + 1)) = (πβ2)) |
24 | 19, 23 | preq12d 4703 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 1 β {(πβπ), (πβ(π + 1))} = {(πβ1), (πβ2)}) |
25 | 24 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β ({(πβπ), (πβ(π + 1))} β πΈ β {(πβ1), (πβ2)} β πΈ)) |
26 | 13, 14, 18, 25 | ralpr 4662 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
{0, 1} {(πβπ), (πβ(π + 1))} β πΈ β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ)) |
27 | | 2ex 12231 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
V |
28 | | 3ex 12236 |
. . . . . . . . . . . . . . . . 17
β’ 3 β
V |
29 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 2 β (πβπ) = (πβ2)) |
30 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 2 β (π + 1) = (2 + 1)) |
31 | | 2p1e3 12296 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (2 + 1) =
3 |
32 | 30, 31 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 2 β (π + 1) = 3) |
33 | 32 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 2 β (πβ(π + 1)) = (πβ3)) |
34 | 29, 33 | preq12d 4703 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 2 β {(πβπ), (πβ(π + 1))} = {(πβ2), (πβ3)}) |
35 | 34 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = 2 β ({(πβπ), (πβ(π + 1))} β πΈ β {(πβ2), (πβ3)} β πΈ)) |
36 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 3 β (πβπ) = (πβ3)) |
37 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 3 β (π + 1) = (3 + 1)) |
38 | | 3p1e4 12299 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (3 + 1) =
4 |
39 | 37, 38 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 3 β (π + 1) = 4) |
40 | 39 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 3 β (πβ(π + 1)) = (πβ4)) |
41 | 36, 40 | preq12d 4703 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 3 β {(πβπ), (πβ(π + 1))} = {(πβ3), (πβ4)}) |
42 | 41 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = 3 β ({(πβπ), (πβ(π + 1))} β πΈ β {(πβ3), (πβ4)} β πΈ)) |
43 | 27, 28, 35, 42 | ralpr 4662 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
{2, 3} {(πβπ), (πβ(π + 1))} β πΈ β ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ)) |
44 | 26, 43 | anbi12i 628 |
. . . . . . . . . . . . . . 15
β’
((βπ β
{0, 1} {(πβπ), (πβ(π + 1))} β πΈ β§ βπ β {2, 3} {(πβπ), (πβ(π + 1))} β πΈ) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ))) |
45 | 12, 44 | bitri 275 |
. . . . . . . . . . . . . 14
β’
(βπ β
({0, 1} βͺ {2, 3}){(πβπ), (πβ(π + 1))} β πΈ β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ))) |
46 | 11, 45 | bitrdi 287 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) =
4 β (βπ β
(0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ)))) |
47 | 7, 46 | anbi12d 632 |
. . . . . . . . . . . 12
β’
((β―βπΉ) =
4 β (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β§ βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ) β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ4)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ))))) |
48 | | preq2 4696 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβ4) = (πβ0) β {(πβ3), (πβ4)} = {(πβ3), (πβ0)}) |
49 | 48 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβ4) = (πβ0) β ({(πβ3), (πβ4)} β πΈ β {(πβ3), (πβ0)} β πΈ)) |
50 | 49 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβ0) = (πβ4) β ({(πβ3), (πβ4)} β πΈ β {(πβ3), (πβ0)} β πΈ)) |
51 | 50 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβ0) = (πβ4) β (({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ) β ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) |
52 | 51 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
β’ ((πβ0) = (πβ4) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ)) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ)))) |
53 | 52 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’
((((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β§ (πβ0) = (πβ4)) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ)) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ)))) |
54 | | 4nn0 12433 |
. . . . . . . . . . . . . . . . . . 19
β’ 4 β
β0 |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’
(((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β 4 β
β0) |
56 | | upgr4cycl4dv4e.v |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = (VtxβπΊ) |
57 | 56 | wlkp 28567 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΉ(WalksβπΊ)π β π:(0...(β―βπΉ))βΆπ) |
58 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπΉ) =
4 β (0...(β―βπΉ)) = (0...4)) |
59 | 58 | feq2d 6655 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπΉ) =
4 β (π:(0...(β―βπΉ))βΆπ β π:(0...4)βΆπ)) |
60 | 59 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π:(0...(β―βπΉ))βΆπ β ((β―βπΉ) = 4 β π:(0...4)βΆπ)) |
61 | 2, 57, 60 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉ(PathsβπΊ)π β ((β―βπΉ) = 4 β π:(0...4)βΆπ)) |
62 | 61 | impcom 409 |
. . . . . . . . . . . . . . . . . 18
β’
(((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β π:(0...4)βΆπ) |
63 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4 β
β0 β 4 β β0) |
64 | | 0nn0 12429 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 β
β0 |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4 β
β0 β 0 β β0) |
66 | | 4pos 12261 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 <
4 |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4 β
β0 β 0 < 4) |
68 | 63, 65, 67 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (4 β
β0 β (4 β β0 β§ 0 β
β0 β§ 0 < 4)) |
69 | | fvffz0 13560 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((4
β β0 β§ 0 β β0 β§ 0 < 4)
β§ π:(0...4)βΆπ) β (πβ0) β π) |
70 | 68, 69 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((4
β β0 β§ π:(0...4)βΆπ) β (πβ0) β π) |
71 | 70 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((β―βπΉ) = 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) β (πβ0) β π) |
72 | | 1nn0 12430 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 1 β
β0 |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4 β
β0 β 1 β β0) |
74 | | 1lt4 12330 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 1 <
4 |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4 β
β0 β 1 < 4) |
76 | 63, 73, 75 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (4 β
β0 β (4 β β0 β§ 1 β
β0 β§ 1 < 4)) |
77 | | fvffz0 13560 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((4
β β0 β§ 1 β β0 β§ 1 < 4)
β§ π:(0...4)βΆπ) β (πβ1) β π) |
78 | 76, 77 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((4
β β0 β§ π:(0...4)βΆπ) β (πβ1) β π) |
79 | 78 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((β―βπΉ) = 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) β (πβ1) β π) |
80 | | 2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 2 β
β0 |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (4 β
β0 β 2 β β0) |
82 | | 2lt4 12329 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 2 <
4 |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (4 β
β0 β 2 < 4) |
84 | 63, 81, 83 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4 β
β0 β (4 β β0 β§ 2 β
β0 β§ 2 < 4)) |
85 | | fvffz0 13560 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((4
β β0 β§ 2 β β0 β§ 2 < 4)
β§ π:(0...4)βΆπ) β (πβ2) β π) |
86 | 84, 85 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((4
β β0 β§ π:(0...4)βΆπ) β (πβ2) β π) |
87 | 86 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((β―βπΉ) = 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) β (πβ2) β π) |
88 | | 3nn0 12432 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 3 β
β0 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (4 β
β0 β 3 β β0) |
90 | | 3lt4 12328 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 3 <
4 |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (4 β
β0 β 3 < 4) |
92 | 63, 89, 91 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4 β
β0 β (4 β β0 β§ 3 β
β0 β§ 3 < 4)) |
93 | | fvffz0 13560 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((4
β β0 β§ 3 β β0 β§ 3 < 4)
β§ π:(0...4)βΆπ) β (πβ3) β π) |
94 | 92, 93 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((4
β β0 β§ π:(0...4)βΆπ) β (πβ3) β π) |
95 | 94 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((β―βπΉ) = 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) β (πβ3) β π) |
96 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((β―βπΉ) = 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) |
97 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β πΉ(PathsβπΊ)π) |
98 | | breq2 5110 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπΉ) =
4 β (1 < (β―βπΉ) β 1 < 4)) |
99 | 74, 98 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπΉ) =
4 β 1 < (β―βπΉ)) |
100 | 99 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β 1 <
(β―βπΉ)) |
101 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β (β―βπΉ) = 4) |
102 | 8 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β
(0..^(β―βπΉ)) =
(0..^4)) |
103 | | 4nn 12237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ 4 β
β |
104 | | lbfzo0 13613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (0 β
(0..^4) β 4 β β) |
105 | 103, 104 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 0 β
(0..^4) |
106 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((0..^(β―βπΉ)) = (0..^4) β (0 β
(0..^(β―βπΉ))
β 0 β (0..^4))) |
107 | 105, 106 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((0..^(β―βπΉ)) = (0..^4) β 0 β
(0..^(β―βπΉ))) |
108 | 107 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπΉ)
= 4 β§ (0..^(β―βπΉ)) = (0..^4)) β 0 β
(0..^(β―βπΉ))) |
109 | | pthdadjvtx 28681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ 0 β
(0..^(β―βπΉ)))
β (πβ0) β
(πβ(0 +
1))) |
110 | 108, 109 | syl3an3 1166 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ0) β (πβ(0 + 1))) |
111 | | 1e0p1 12661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 1 = (0 +
1) |
112 | 111 | fveq2i 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πβ1) = (πβ(0 + 1)) |
113 | 112 | neeq2i 3010 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβ0) β (πβ1) β (πβ0) β (πβ(0 +
1))) |
114 | 110, 113 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ0) β (πβ1)) |
115 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β πΉ(PathsβπΊ)π) |
116 | | elfzo0 13614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (2 β
(0..^4) β (2 β β0 β§ 4 β β β§ 2
< 4)) |
117 | 80, 103, 82, 116 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 2 β
(0..^4) |
118 | | 2ne0 12258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 2 β
0 |
119 | | fzo1fzo0n0 13624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (2 β
(1..^4) β (2 β (0..^4) β§ 2 β 0)) |
120 | 117, 118,
119 | mpbir2an 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 2 β
(1..^4) |
121 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((β―βπΉ) =
4 β (1..^(β―βπΉ)) = (1..^4)) |
122 | 120, 121 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((β―βπΉ) =
4 β 2 β (1..^(β―βπΉ))) |
123 | | 0elfz 13539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (4 β
β0 β 0 β (0...4)) |
124 | 54, 123 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 0 β
(0...4) |
125 | 124, 58 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((β―βπΉ) =
4 β 0 β (0...(β―βπΉ))) |
126 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((β―βπΉ) =
4 β 2 β 0) |
127 | 122, 125,
126 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((β―βπΉ) =
4 β (2 β (1..^(β―βπΉ)) β§ 0 β (0...(β―βπΉ)) β§ 2 β
0)) |
128 | 127 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((β―βπΉ)
= 4 β§ (0..^(β―βπΉ)) = (0..^4)) β (2 β
(1..^(β―βπΉ))
β§ 0 β (0...(β―βπΉ)) β§ 2 β 0)) |
129 | 128 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (2 β (1..^(β―βπΉ)) β§ 0 β (0...(β―βπΉ)) β§ 2 β
0)) |
130 | | pthdivtx 28680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ(PathsβπΊ)π β§ (2 β (1..^(β―βπΉ)) β§ 0 β
(0...(β―βπΉ))
β§ 2 β 0)) β (πβ2) β (πβ0)) |
131 | 115, 129,
130 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ2) β (πβ0)) |
132 | 131 | necomd 3000 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ0) β (πβ2)) |
133 | | elfzo0 13614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (3 β
(0..^4) β (3 β β0 β§ 4 β β β§ 3
< 4)) |
134 | 88, 103, 90, 133 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 3 β
(0..^4) |
135 | | 3ne0 12260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 3 β
0 |
136 | | fzo1fzo0n0 13624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (3 β
(1..^4) β (3 β (0..^4) β§ 3 β 0)) |
137 | 134, 135,
136 | mpbir2an 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 3 β
(1..^4) |
138 | 137, 121 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((β―βπΉ) =
4 β 3 β (1..^(β―βπΉ))) |
139 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((β―βπΉ) =
4 β 3 β 0) |
140 | 138, 125,
139 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((β―βπΉ) =
4 β (3 β (1..^(β―βπΉ)) β§ 0 β (0...(β―βπΉ)) β§ 3 β
0)) |
141 | 140 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((β―βπΉ)
= 4 β§ (0..^(β―βπΉ)) = (0..^4)) β (3 β
(1..^(β―βπΉ))
β§ 0 β (0...(β―βπΉ)) β§ 3 β 0)) |
142 | 141 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (3 β (1..^(β―βπΉ)) β§ 0 β (0...(β―βπΉ)) β§ 3 β
0)) |
143 | | pthdivtx 28680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ(PathsβπΊ)π β§ (3 β (1..^(β―βπΉ)) β§ 0 β
(0...(β―βπΉ))
β§ 3 β 0)) β (πβ3) β (πβ0)) |
144 | 115, 142,
143 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ3) β (πβ0)) |
145 | 144 | necomd 3000 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ0) β (πβ3)) |
146 | 114, 132,
145 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β ((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β (πβ3))) |
147 | | elfzo0 13614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (1 β
(0..^4) β (1 β β0 β§ 4 β β β§ 1
< 4)) |
148 | 72, 103, 74, 147 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 1 β
(0..^4) |
149 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((0..^(β―βπΉ)) = (0..^4) β (1 β
(0..^(β―βπΉ))
β 1 β (0..^4))) |
150 | 148, 149 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((0..^(β―βπΉ)) = (0..^4) β 1 β
(0..^(β―βπΉ))) |
151 | 150 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπΉ)
= 4 β§ (0..^(β―βπΉ)) = (0..^4)) β 1 β
(0..^(β―βπΉ))) |
152 | | pthdadjvtx 28681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ 1 β
(0..^(β―βπΉ)))
β (πβ1) β
(πβ(1 +
1))) |
153 | 151, 152 | syl3an3 1166 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ1) β (πβ(1 + 1))) |
154 | | df-2 12217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 2 = (1 +
1) |
155 | 154 | fveq2i 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πβ2) = (πβ(1 + 1)) |
156 | 155 | neeq2i 3010 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβ1) β (πβ2) β (πβ1) β (πβ(1 +
1))) |
157 | 153, 156 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ1) β (πβ2)) |
158 | | ax-1ne0 11121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 1 β
0 |
159 | | fzo1fzo0n0 13624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (1 β
(1..^4) β (1 β (0..^4) β§ 1 β 0)) |
160 | 148, 158,
159 | mpbir2an 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ 1 β
(1..^4) |
161 | 160, 121 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((β―βπΉ) =
4 β 1 β (1..^(β―βπΉ))) |
162 | | 3re 12234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 3 β
β |
163 | | 4re 12238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 4 β
β |
164 | 162, 163,
90 | ltleii 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 3 β€
4 |
165 | | elfz2nn0 13533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (3 β
(0...4) β (3 β β0 β§ 4 β β0
β§ 3 β€ 4)) |
166 | 88, 54, 164, 165 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ 3 β
(0...4) |
167 | 166, 58 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((β―βπΉ) =
4 β 3 β (0...(β―βπΉ))) |
168 | | 1re 11156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 1 β
β |
169 | | 1lt3 12327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 1 <
3 |
170 | 168, 169 | ltneii 11269 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ 1 β
3 |
171 | 170 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((β―βπΉ) =
4 β 1 β 3) |
172 | 161, 167,
171 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((β―βπΉ) =
4 β (1 β (1..^(β―βπΉ)) β§ 3 β (0...(β―βπΉ)) β§ 1 β
3)) |
173 | 172 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπΉ)
= 4 β§ (0..^(β―βπΉ)) = (0..^4)) β (1 β
(1..^(β―βπΉ))
β§ 3 β (0...(β―βπΉ)) β§ 1 β 3)) |
174 | 173 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (1 β (1..^(β―βπΉ)) β§ 3 β (0...(β―βπΉ)) β§ 1 β
3)) |
175 | | pthdivtx 28680 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉ(PathsβπΊ)π β§ (1 β (1..^(β―βπΉ)) β§ 3 β
(0...(β―βπΉ))
β§ 1 β 3)) β (πβ1) β (πβ3)) |
176 | 115, 174,
175 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ1) β (πβ3)) |
177 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((0..^(β―βπΉ)) = (0..^4) β (2 β
(0..^(β―βπΉ))
β 2 β (0..^4))) |
178 | 117, 177 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((0..^(β―βπΉ)) = (0..^4) β 2 β
(0..^(β―βπΉ))) |
179 | 178 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπΉ)
= 4 β§ (0..^(β―βπΉ)) = (0..^4)) β 2 β
(0..^(β―βπΉ))) |
180 | | pthdadjvtx 28681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ 2 β
(0..^(β―βπΉ)))
β (πβ2) β
(πβ(2 +
1))) |
181 | 179, 180 | syl3an3 1166 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ2) β (πβ(2 + 1))) |
182 | | df-3 12218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 3 = (2 +
1) |
183 | 182 | fveq2i 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πβ3) = (πβ(2 + 1)) |
184 | 183 | neeq2i 3010 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβ2) β (πβ3) β (πβ2) β (πβ(2 +
1))) |
185 | 181, 184 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (πβ2) β (πβ3)) |
186 | 157, 176,
185 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β ((πβ1) β (πβ2) β§ (πβ1) β (πβ3) β§ (πβ2) β (πβ3))) |
187 | 146, 186 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ ((β―βπΉ) = 4 β§
(0..^(β―βπΉ)) =
(0..^4))) β (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β (πβ3)) β§ ((πβ1) β (πβ2) β§ (πβ1) β (πβ3) β§ (πβ2) β (πβ3)))) |
188 | 97, 100, 101, 102, 187 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β (πβ3)) β§ ((πβ1) β (πβ2) β§ (πβ1) β (πβ3) β§ (πβ2) β (πβ3)))) |
189 | 188 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((β―βπΉ) = 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) β (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β (πβ3)) β§ ((πβ1) β (πβ2) β§ (πβ1) β (πβ3) β§ (πβ2) β (πβ3)))) |
190 | | preq2 4696 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (πβ2) β {(πβ1), π} = {(πβ1), (πβ2)}) |
191 | 190 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ2) β ({(πβ1), π} β πΈ β {(πβ1), (πβ2)} β πΈ)) |
192 | 191 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πβ2) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ))) |
193 | | preq1 4695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (πβ2) β {π, π} = {(πβ2), π}) |
194 | 193 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ2) β ({π, π} β πΈ β {(πβ2), π} β πΈ)) |
195 | 194 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πβ2) β (({π, π} β πΈ β§ {π, (πβ0)} β πΈ) β ({(πβ2), π} β πΈ β§ {π, (πβ0)} β πΈ))) |
196 | 192, 195 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (πβ2) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), π} β πΈ β§ {π, (πβ0)} β πΈ)))) |
197 | | neeq2 3008 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ2) β ((πβ0) β π β (πβ0) β (πβ2))) |
198 | 197 | 3anbi2d 1442 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πβ2) β (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β ((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β π))) |
199 | | neeq2 3008 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ2) β ((πβ1) β π β (πβ1) β (πβ2))) |
200 | | neeq1 3007 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ2) β (π β π β (πβ2) β π)) |
201 | 199, 200 | 3anbi13d 1439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πβ2) β (((πβ1) β π β§ (πβ1) β π β§ π β π) β ((πβ1) β (πβ2) β§ (πβ1) β π β§ (πβ2) β π))) |
202 | 198, 201 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (πβ2) β ((((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)) β (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β π) β§ ((πβ1) β (πβ2) β§ (πβ1) β π β§ (πβ2) β π)))) |
203 | 196, 202 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πβ2) β (((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π))) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β π) β§ ((πβ1) β (πβ2) β§ (πβ1) β π β§ (πβ2) β π))))) |
204 | | preq2 4696 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (πβ3) β {(πβ2), π} = {(πβ2), (πβ3)}) |
205 | 204 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ3) β ({(πβ2), π} β πΈ β {(πβ2), (πβ3)} β πΈ)) |
206 | | preq1 4695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (πβ3) β {π, (πβ0)} = {(πβ3), (πβ0)}) |
207 | 206 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ3) β ({π, (πβ0)} β πΈ β {(πβ3), (πβ0)} β πΈ)) |
208 | 205, 207 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πβ3) β (({(πβ2), π} β πΈ β§ {π, (πβ0)} β πΈ) β ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) |
209 | 208 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (πβ3) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), π} β πΈ β§ {π, (πβ0)} β πΈ)) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ)))) |
210 | | neeq2 3008 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ3) β ((πβ0) β π β (πβ0) β (πβ3))) |
211 | 210 | 3anbi3d 1443 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πβ3) β (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β π) β ((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β (πβ3)))) |
212 | | neeq2 3008 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ3) β ((πβ1) β π β (πβ1) β (πβ3))) |
213 | | neeq2 3008 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πβ3) β ((πβ2) β π β (πβ2) β (πβ3))) |
214 | 212, 213 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πβ3) β (((πβ1) β (πβ2) β§ (πβ1) β π β§ (πβ2) β π) β ((πβ1) β (πβ2) β§ (πβ1) β (πβ3) β§ (πβ2) β (πβ3)))) |
215 | 211, 214 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (πβ3) β ((((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β π) β§ ((πβ1) β (πβ2) β§ (πβ1) β π β§ (πβ2) β π)) β (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β (πβ3)) β§ ((πβ1) β (πβ2) β§ (πβ1) β (πβ3) β§ (πβ2) β (πβ3))))) |
216 | 209, 215 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πβ3) β (((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β π) β§ ((πβ1) β (πβ2) β§ (πβ1) β π β§ (πβ2) β π))) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β (πβ3)) β§ ((πβ1) β (πβ2) β§ (πβ1) β (πβ3) β§ (πβ2) β (πβ3)))))) |
217 | 203, 216 | rspc2ev 3593 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβ2) β π β§ (πβ3) β π β§ ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ0) β (πβ3)) β§ ((πβ1) β (πβ2) β§ (πβ1) β (πβ3) β§ (πβ2) β (πβ3))))) β βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)))) |
218 | 87, 95, 96, 189, 217 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((β―βπΉ) = 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) β βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)))) |
219 | 71, 79, 218 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((β―βπΉ) = 4 β§ πΉ(PathsβπΊ)π) β§ (4 β β0 β§
π:(0...4)βΆπ)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ))) β ((πβ0) β π β§ (πβ1) β π β§ βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π))))) |
220 | 219 | exp31 421 |
. . . . . . . . . . . . . . . . . 18
β’
(((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β ((4 β β0
β§ π:(0...4)βΆπ) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ)) β ((πβ0) β π β§ (πβ1) β π β§ βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π))))))) |
221 | 55, 62, 220 | mp2and 698 |
. . . . . . . . . . . . . . . . 17
β’
(((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ)) β ((πβ0) β π β§ (πβ1) β π β§ βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)))))) |
222 | 221 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β§ (πβ0) = (πβ4)) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ0)} β πΈ)) β ((πβ0) β π β§ (πβ1) β π β§ βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)))))) |
223 | 53, 222 | sylbid 239 |
. . . . . . . . . . . . . . 15
β’
((((β―βπΉ)
= 4 β§ πΉ(PathsβπΊ)π) β§ (πβ0) = (πβ4)) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ)) β ((πβ0) β π β§ (πβ1) β π β§ βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)))))) |
224 | 223 | exp31 421 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ) =
4 β (πΉ(PathsβπΊ)π β ((πβ0) = (πβ4) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ)) β ((πβ0) β π β§ (πβ1) β π β§ βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)))))))) |
225 | 224 | imp4c 425 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) =
4 β (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ4)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ))) β ((πβ0) β π β§ (πβ1) β π β§ βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)))))) |
226 | | preq1 4695 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ0) β {π, π} = {(πβ0), π}) |
227 | 226 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ0) β ({π, π} β πΈ β {(πβ0), π} β πΈ)) |
228 | 227 | anbi1d 631 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ0) β (({π, π} β πΈ β§ {π, π} β πΈ) β ({(πβ0), π} β πΈ β§ {π, π} β πΈ))) |
229 | | preq2 4696 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ0) β {π, π} = {π, (πβ0)}) |
230 | 229 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ0) β ({π, π} β πΈ β {π, (πβ0)} β πΈ)) |
231 | 230 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ0) β (({π, π} β πΈ β§ {π, π} β πΈ) β ({π, π} β πΈ β§ {π, (πβ0)} β πΈ))) |
232 | 228, 231 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ0) β ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β (({(πβ0), π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)))) |
233 | | neeq1 3007 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ0) β (π β π β (πβ0) β π)) |
234 | | neeq1 3007 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ0) β (π β π β (πβ0) β π)) |
235 | | neeq1 3007 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ0) β (π β π β (πβ0) β π)) |
236 | 233, 234,
235 | 3anbi123d 1437 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ0) β ((π β π β§ π β π β§ π β π) β ((πβ0) β π β§ (πβ0) β π β§ (πβ0) β π))) |
237 | 236 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ0) β (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)) β (((πβ0) β π β§ (πβ0) β π β§ (πβ0) β π) β§ (π β π β§ π β π β§ π β π)))) |
238 | 232, 237 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = (πβ0) β (((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))) β ((({(πβ0), π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β π β§ (πβ0) β π β§ (πβ0) β π) β§ (π β π β§ π β π β§ π β π))))) |
239 | 238 | 2rexbidv 3214 |
. . . . . . . . . . . . . 14
β’ (π = (πβ0) β (βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))) β βπ β π βπ β π ((({(πβ0), π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β π β§ (πβ0) β π β§ (πβ0) β π) β§ (π β π β§ π β π β§ π β π))))) |
240 | | preq2 4696 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ1) β {(πβ0), π} = {(πβ0), (πβ1)}) |
241 | 240 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ1) β ({(πβ0), π} β πΈ β {(πβ0), (πβ1)} β πΈ)) |
242 | | preq1 4695 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ1) β {π, π} = {(πβ1), π}) |
243 | 242 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ1) β ({π, π} β πΈ β {(πβ1), π} β πΈ)) |
244 | 241, 243 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ1) β (({(πβ0), π} β πΈ β§ {π, π} β πΈ) β ({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ))) |
245 | 244 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ1) β ((({(πβ0), π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)))) |
246 | | neeq2 3008 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ1) β ((πβ0) β π β (πβ0) β (πβ1))) |
247 | 246 | 3anbi1d 1441 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ1) β (((πβ0) β π β§ (πβ0) β π β§ (πβ0) β π) β ((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π))) |
248 | | neeq1 3007 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ1) β (π β π β (πβ1) β π)) |
249 | | neeq1 3007 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ1) β (π β π β (πβ1) β π)) |
250 | 248, 249 | 3anbi12d 1438 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ1) β ((π β π β§ π β π β§ π β π) β ((πβ1) β π β§ (πβ1) β π β§ π β π))) |
251 | 247, 250 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ1) β ((((πβ0) β π β§ (πβ0) β π β§ (πβ0) β π) β§ (π β π β§ π β π β§ π β π)) β (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)))) |
252 | 245, 251 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = (πβ1) β (((({(πβ0), π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β π β§ (πβ0) β π β§ (πβ0) β π) β§ (π β π β§ π β π β§ π β π))) β ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π))))) |
253 | 252 | 2rexbidv 3214 |
. . . . . . . . . . . . . 14
β’ (π = (πβ1) β (βπ β π βπ β π ((({(πβ0), π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β π β§ (πβ0) β π β§ (πβ0) β π) β§ (π β π β§ π β π β§ π β π))) β βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π))))) |
254 | 239, 253 | rspc2ev 3593 |
. . . . . . . . . . . . 13
β’ (((πβ0) β π β§ (πβ1) β π β§ βπ β π βπ β π ((({(πβ0), (πβ1)} β πΈ β§ {(πβ1), π} β πΈ) β§ ({π, π} β πΈ β§ {π, (πβ0)} β πΈ)) β§ (((πβ0) β (πβ1) β§ (πβ0) β π β§ (πβ0) β π) β§ ((πβ1) β π β§ (πβ1) β π β§ π β π)))) β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) |
255 | 225, 254 | syl6 35 |
. . . . . . . . . . . 12
β’
((β―βπΉ) =
4 β (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ4)) β§ (({(πβ0), (πβ1)} β πΈ β§ {(πβ1), (πβ2)} β πΈ) β§ ({(πβ2), (πβ3)} β πΈ β§ {(πβ3), (πβ4)} β πΈ))) β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))))) |
256 | 47, 255 | sylbid 239 |
. . . . . . . . . . 11
β’
((β―βπΉ) =
4 β (((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β§ βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ) β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))))) |
257 | 256 | expd 417 |
. . . . . . . . . 10
β’
((β―βπΉ) =
4 β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))))) |
258 | 257 | com13 88 |
. . . . . . . . 9
β’
(βπ β
(0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β ((β―βπΉ) = 4 β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))))) |
259 | 4, 258 | syl 17 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π) β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β ((β―βπΉ) = 4 β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))))) |
260 | 259 | expcom 415 |
. . . . . . 7
β’ (πΉ(WalksβπΊ)π β (πΊ β UPGraph β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β ((β―βπΉ) = 4 β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))))))) |
261 | 260 | com23 86 |
. . . . . 6
β’ (πΉ(WalksβπΊ)π β ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (πΊ β UPGraph β ((β―βπΉ) = 4 β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))))))) |
262 | 261 | expd 417 |
. . . . 5
β’ (πΉ(WalksβπΊ)π β (πΉ(PathsβπΊ)π β ((πβ0) = (πβ(β―βπΉ)) β (πΊ β UPGraph β ((β―βπΉ) = 4 β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))))))) |
263 | 2, 262 | mpcom 38 |
. . . 4
β’ (πΉ(PathsβπΊ)π β ((πβ0) = (πβ(β―βπΉ)) β (πΊ β UPGraph β ((β―βπΉ) = 4 β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))))))) |
264 | 263 | imp 408 |
. . 3
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (πΊ β UPGraph β ((β―βπΉ) = 4 β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))))) |
265 | 1, 264 | syl 17 |
. 2
β’ (πΉ(CyclesβπΊ)π β (πΊ β UPGraph β ((β―βπΉ) = 4 β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))))) |
266 | 265 | 3imp21 1115 |
1
β’ ((πΊ β UPGraph β§ πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 4) β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) |