Step | Hyp | Ref
| Expression |
1 | | eupth2.v |
. . . . . . 7
β’ π = (VtxβπΊ) |
2 | | eupth2.i |
. . . . . . 7
β’ πΌ = (iEdgβπΊ) |
3 | | eupth2.g |
. . . . . . 7
β’ (π β πΊ β UPGraph) |
4 | | eupth2.f |
. . . . . . 7
β’ (π β Fun πΌ) |
5 | | eupth2.p |
. . . . . . 7
β’ (π β πΉ(EulerPathsβπΊ)π) |
6 | | eqid 2737 |
. . . . . . 7
β’
β¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β© = β¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β© |
7 | 1, 2, 3, 4, 5, 6 | eupthvdres 29182 |
. . . . . 6
β’ (π β (VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©) =
(VtxDegβπΊ)) |
8 | 7 | fveq1d 6845 |
. . . . 5
β’ (π β ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©)βπ₯) = ((VtxDegβπΊ)βπ₯)) |
9 | 8 | breq2d 5118 |
. . . 4
β’ (π β (2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯) β 2 β₯ ((VtxDegβπΊ)βπ₯))) |
10 | 9 | notbid 318 |
. . 3
β’ (π β (Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯) β Β¬ 2 β₯ ((VtxDegβπΊ)βπ₯))) |
11 | 10 | rabbidv 3416 |
. 2
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯)} = {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) |
12 | | eupthiswlk 29159 |
. . . 4
β’ (πΉ(EulerPathsβπΊ)π β πΉ(WalksβπΊ)π) |
13 | | wlkcl 28566 |
. . . 4
β’ (πΉ(WalksβπΊ)π β (β―βπΉ) β
β0) |
14 | 5, 12, 13 | 3syl 18 |
. . 3
β’ (π β (β―βπΉ) β
β0) |
15 | | nn0re 12423 |
. . . . 5
β’
((β―βπΉ)
β β0 β (β―βπΉ) β β) |
16 | 15 | leidd 11722 |
. . . 4
β’
((β―βπΉ)
β β0 β (β―βπΉ) β€ (β―βπΉ)) |
17 | | breq1 5109 |
. . . . . . 7
β’ (π = 0 β (π β€ (β―βπΉ) β 0 β€ (β―βπΉ))) |
18 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (0..^π) = (0..^0)) |
19 | 18 | imaeq2d 6014 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (πΉ β (0..^π)) = (πΉ β (0..^0))) |
20 | 19 | reseq2d 5938 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (πΌ βΎ (πΉ β (0..^π))) = (πΌ βΎ (πΉ β (0..^0)))) |
21 | 20 | opeq2d 4838 |
. . . . . . . . . . . . 13
β’ (π = 0 β β¨π, (πΌ βΎ (πΉ β (0..^π)))β© = β¨π, (πΌ βΎ (πΉ β (0..^0)))β©) |
22 | 21 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π = 0 β
(VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©) = (VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©)) |
23 | 22 | fveq1d 6845 |
. . . . . . . . . . 11
β’ (π = 0 β
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) = ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©)βπ₯)) |
24 | 23 | breq2d 5118 |
. . . . . . . . . 10
β’ (π = 0 β (2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) β 2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©)βπ₯))) |
25 | 24 | notbid 318 |
. . . . . . . . 9
β’ (π = 0 β (Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) β Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯))) |
26 | 25 | rabbidv 3416 |
. . . . . . . 8
β’ (π = 0 β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)}) |
27 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = 0 β (πβπ) = (πβ0)) |
28 | 27 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π = 0 β ((πβ0) = (πβπ) β (πβ0) = (πβ0))) |
29 | 27 | preq2d 4702 |
. . . . . . . . 9
β’ (π = 0 β {(πβ0), (πβπ)} = {(πβ0), (πβ0)}) |
30 | 28, 29 | ifbieq2d 4513 |
. . . . . . . 8
β’ (π = 0 β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) = if((πβ0) = (πβ0), β
, {(πβ0), (πβ0)})) |
31 | 26, 30 | eqeq12d 2753 |
. . . . . . 7
β’ (π = 0 β ({π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)}
= if((πβ0) = (πβ0), β
, {(πβ0), (πβ0)}))) |
32 | 17, 31 | imbi12d 345 |
. . . . . 6
β’ (π = 0 β ((π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) β (0 β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)}
= if((πβ0) = (πβ0), β
, {(πβ0), (πβ0)})))) |
33 | 32 | imbi2d 341 |
. . . . 5
β’ (π = 0 β ((π β (π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π β (0 β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)}
= if((πβ0) = (πβ0), β
, {(πβ0), (πβ0)}))))) |
34 | | breq1 5109 |
. . . . . . 7
β’ (π = π β (π β€ (β―βπΉ) β π β€ (β―βπΉ))) |
35 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (0..^π) = (0..^π)) |
36 | 35 | imaeq2d 6014 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉ β (0..^π)) = (πΉ β (0..^π))) |
37 | 36 | reseq2d 5938 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΌ βΎ (πΉ β (0..^π))) = (πΌ βΎ (πΉ β (0..^π)))) |
38 | 37 | opeq2d 4838 |
. . . . . . . . . . . . 13
β’ (π = π β β¨π, (πΌ βΎ (πΉ β (0..^π)))β© = β¨π, (πΌ βΎ (πΉ β (0..^π)))β©) |
39 | 38 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π = π β (VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©) = (VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©)) |
40 | 39 | fveq1d 6845 |
. . . . . . . . . . 11
β’ (π = π β ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) = ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)) |
41 | 40 | breq2d 5118 |
. . . . . . . . . 10
β’ (π = π β (2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) β 2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©)βπ₯))) |
42 | 41 | notbid 318 |
. . . . . . . . 9
β’ (π = π β (Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) β Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯))) |
43 | 42 | rabbidv 3416 |
. . . . . . . 8
β’ (π = π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)}) |
44 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
45 | 44 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π = π β ((πβ0) = (πβπ) β (πβ0) = (πβπ))) |
46 | 44 | preq2d 4702 |
. . . . . . . . 9
β’ (π = π β {(πβ0), (πβπ)} = {(πβ0), (πβπ)}) |
47 | 45, 46 | ifbieq2d 4513 |
. . . . . . . 8
β’ (π = π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) |
48 | 43, 47 | eqeq12d 2753 |
. . . . . . 7
β’ (π = π β ({π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
49 | 34, 48 | imbi12d 345 |
. . . . . 6
β’ (π = π β ((π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) β (π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})))) |
50 | 49 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β (π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π β (π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))))) |
51 | | breq1 5109 |
. . . . . . 7
β’ (π = (π + 1) β (π β€ (β―βπΉ) β (π + 1) β€ (β―βπΉ))) |
52 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (0..^π) = (0..^(π + 1))) |
53 | 52 | imaeq2d 6014 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (πΉ β (0..^π)) = (πΉ β (0..^(π + 1)))) |
54 | 53 | reseq2d 5938 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (πΌ βΎ (πΉ β (0..^π))) = (πΌ βΎ (πΉ β (0..^(π + 1))))) |
55 | 54 | opeq2d 4838 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β β¨π, (πΌ βΎ (πΉ β (0..^π)))β© = β¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©) |
56 | 55 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β (VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©) = (VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©)) |
57 | 56 | fveq1d 6845 |
. . . . . . . . . . 11
β’ (π = (π + 1) β ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) = ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)) |
58 | 57 | breq2d 5118 |
. . . . . . . . . 10
β’ (π = (π + 1) β (2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) β 2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯))) |
59 | 58 | notbid 318 |
. . . . . . . . 9
β’ (π = (π + 1) β (Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) β Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯))) |
60 | 59 | rabbidv 3416 |
. . . . . . . 8
β’ (π = (π + 1) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)}) |
61 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
62 | 61 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π = (π + 1) β ((πβ0) = (πβπ) β (πβ0) = (πβ(π + 1)))) |
63 | 61 | preq2d 4702 |
. . . . . . . . 9
β’ (π = (π + 1) β {(πβ0), (πβπ)} = {(πβ0), (πβ(π + 1))}) |
64 | 62, 63 | ifbieq2d 4513 |
. . . . . . . 8
β’ (π = (π + 1) β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})) |
65 | 60, 64 | eqeq12d 2753 |
. . . . . . 7
β’ (π = (π + 1) β ({π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
66 | 51, 65 | imbi12d 345 |
. . . . . 6
β’ (π = (π + 1) β ((π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) β ((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
67 | 66 | imbi2d 341 |
. . . . 5
β’ (π = (π + 1) β ((π β (π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π β ((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))))) |
68 | | breq1 5109 |
. . . . . . 7
β’ (π = (β―βπΉ) β (π β€ (β―βπΉ) β (β―βπΉ) β€ (β―βπΉ))) |
69 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’ (π = (β―βπΉ) β (0..^π) = (0..^(β―βπΉ))) |
70 | 69 | imaeq2d 6014 |
. . . . . . . . . . . . . . 15
β’ (π = (β―βπΉ) β (πΉ β (0..^π)) = (πΉ β (0..^(β―βπΉ)))) |
71 | 70 | reseq2d 5938 |
. . . . . . . . . . . . . 14
β’ (π = (β―βπΉ) β (πΌ βΎ (πΉ β (0..^π))) = (πΌ βΎ (πΉ β (0..^(β―βπΉ))))) |
72 | 71 | opeq2d 4838 |
. . . . . . . . . . . . 13
β’ (π = (β―βπΉ) β β¨π, (πΌ βΎ (πΉ β (0..^π)))β© = β¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©) |
73 | 72 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π = (β―βπΉ) β
(VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©) = (VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©)) |
74 | 73 | fveq1d 6845 |
. . . . . . . . . . 11
β’ (π = (β―βπΉ) β
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) = ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©)βπ₯)) |
75 | 74 | breq2d 5118 |
. . . . . . . . . 10
β’ (π = (β―βπΉ) β (2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) β 2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©)βπ₯))) |
76 | 75 | notbid 318 |
. . . . . . . . 9
β’ (π = (β―βπΉ) β (Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯) β Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯))) |
77 | 76 | rabbidv 3416 |
. . . . . . . 8
β’ (π = (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯)}) |
78 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = (β―βπΉ) β (πβπ) = (πβ(β―βπΉ))) |
79 | 78 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π = (β―βπΉ) β ((πβ0) = (πβπ) β (πβ0) = (πβ(β―βπΉ)))) |
80 | 78 | preq2d 4702 |
. . . . . . . . 9
β’ (π = (β―βπΉ) β {(πβ0), (πβπ)} = {(πβ0), (πβ(β―βπΉ))}) |
81 | 79, 80 | ifbieq2d 4513 |
. . . . . . . 8
β’ (π = (β―βπΉ) β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) = if((πβ0) = (πβ(β―βπΉ)), β
, {(πβ0), (πβ(β―βπΉ))})) |
82 | 77, 81 | eqeq12d 2753 |
. . . . . . 7
β’ (π = (β―βπΉ) β ({π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯)} = if((πβ0) = (πβ(β―βπΉ)), β
, {(πβ0), (πβ(β―βπΉ))}))) |
83 | 68, 82 | imbi12d 345 |
. . . . . 6
β’ (π = (β―βπΉ) β ((π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) β ((β―βπΉ) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯)} = if((πβ0) = (πβ(β―βπΉ)), β
, {(πβ0), (πβ(β―βπΉ))})))) |
84 | 83 | imbi2d 341 |
. . . . 5
β’ (π = (β―βπΉ) β ((π β (π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π β ((β―βπΉ) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯)} = if((πβ0) = (πβ(β―βπΉ)), β
, {(πβ0), (πβ(β―βπΉ))}))))) |
85 | 1, 2, 3, 4, 5 | eupth2lemb 29184 |
. . . . . . 7
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)}
= β
) |
86 | | eqid 2737 |
. . . . . . . 8
β’ (πβ0) = (πβ0) |
87 | 86 | iftruei 4494 |
. . . . . . 7
β’ if((πβ0) = (πβ0), β
, {(πβ0), (πβ0)}) = β
|
88 | 85, 87 | eqtr4di 2795 |
. . . . . 6
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)}
= if((πβ0) = (πβ0), β
, {(πβ0), (πβ0)})) |
89 | 88 | a1d 25 |
. . . . 5
β’ (π β (0 β€
(β―βπΉ) β
{π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^0)))β©)βπ₯)}
= if((πβ0) = (πβ0), β
, {(πβ0), (πβ0)}))) |
90 | 1, 2, 3, 4, 5 | eupth2lems 29185 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) β ((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
91 | 90 | expcom 415 |
. . . . . 6
β’ (π β β0
β (π β ((π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) β ((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))))) |
92 | 91 | a2d 29 |
. . . . 5
β’ (π β β0
β ((π β (π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π β ((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))))) |
93 | 33, 50, 67, 84, 89, 92 | nn0ind 12599 |
. . . 4
β’
((β―βπΉ)
β β0 β (π β ((β―βπΉ) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯)} = if((πβ0) = (πβ(β―βπΉ)), β
, {(πβ0), (πβ(β―βπΉ))})))) |
94 | 16, 93 | mpid 44 |
. . 3
β’
((β―βπΉ)
β β0 β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯)} = if((πβ0) = (πβ(β―βπΉ)), β
, {(πβ0), (πβ(β―βπΉ))}))) |
95 | 14, 94 | mpcom 38 |
. 2
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β
(0..^(β―βπΉ))))β©)βπ₯)} = if((πβ0) = (πβ(β―βπΉ)), β
, {(πβ0), (πβ(β―βπΉ))})) |
96 | 11, 95 | eqtr3d 2779 |
1
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} = if((πβ0) = (πβ(β―βπΉ)), β
, {(πβ0), (πβ(β―βπΉ))})) |