Step | Hyp | Ref
| Expression |
1 | | nn0re 12423 |
. . . . . 6
β’ (π β β0
β π β
β) |
2 | 1 | adantl 483 |
. . . . 5
β’ ((π β§ π β β0) β π β
β) |
3 | 2 | lep1d 12087 |
. . . 4
β’ ((π β§ π β β0) β π β€ (π + 1)) |
4 | | peano2re 11329 |
. . . . . 6
β’ (π β β β (π + 1) β
β) |
5 | 2, 4 | syl 17 |
. . . . 5
β’ ((π β§ π β β0) β (π + 1) β
β) |
6 | | eupth2.p |
. . . . . . . 8
β’ (π β πΉ(EulerPathsβπΊ)π) |
7 | | eupthiswlk 29159 |
. . . . . . . 8
β’ (πΉ(EulerPathsβπΊ)π β πΉ(WalksβπΊ)π) |
8 | | wlkcl 28566 |
. . . . . . . 8
β’ (πΉ(WalksβπΊ)π β (β―βπΉ) β
β0) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . . 7
β’ (π β (β―βπΉ) β
β0) |
10 | 9 | nn0red 12475 |
. . . . . 6
β’ (π β (β―βπΉ) β
β) |
11 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ π β β0) β
(β―βπΉ) β
β) |
12 | | letr 11250 |
. . . . 5
β’ ((π β β β§ (π + 1) β β β§
(β―βπΉ) β
β) β ((π β€
(π + 1) β§ (π + 1) β€ (β―βπΉ)) β π β€ (β―βπΉ))) |
13 | 2, 5, 11, 12 | syl3anc 1372 |
. . . 4
β’ ((π β§ π β β0) β ((π β€ (π + 1) β§ (π + 1) β€ (β―βπΉ)) β π β€ (β―βπΉ))) |
14 | 3, 13 | mpand 694 |
. . 3
β’ ((π β§ π β β0) β ((π + 1) β€ (β―βπΉ) β π β€ (β―βπΉ))) |
15 | 14 | imim1d 82 |
. 2
β’ ((π β§ π β β0) β ((π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) β ((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})))) |
16 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯) = ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ¦)) |
17 | 16 | breq2d 5118 |
. . . . . . . 8
β’ (π₯ = π¦ β (2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯) β 2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ¦))) |
18 | 17 | notbid 318 |
. . . . . . 7
β’ (π₯ = π¦ β (Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯) β Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ¦))) |
19 | 18 | elrab 3646 |
. . . . . 6
β’ (π¦ β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} β (π¦ β π β§ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ¦))) |
20 | | eupth2.v |
. . . . . . . . 9
β’ π = (VtxβπΊ) |
21 | | eupth2.i |
. . . . . . . . 9
β’ πΌ = (iEdgβπΊ) |
22 | | eupth2.g |
. . . . . . . . . 10
β’ (π β πΊ β UPGraph) |
23 | 22 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β§ π¦ β π) β πΊ β UPGraph) |
24 | | eupth2.f |
. . . . . . . . . 10
β’ (π β Fun πΌ) |
25 | 24 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β§ π¦ β π) β Fun πΌ) |
26 | 6 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β§ π¦ β π) β πΉ(EulerPathsβπΊ)π) |
27 | | eqid 2737 |
. . . . . . . . 9
β’
β¨π, (πΌ βΎ (πΉ β (0..^π)))β© = β¨π, (πΌ βΎ (πΉ β (0..^π)))β© |
28 | | eqid 2737 |
. . . . . . . . 9
β’
β¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β© = β¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β© |
29 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β π β
β0) |
30 | 29 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β§ π¦ β π) β π β β0) |
31 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π + 1) β€ (β―βπΉ)) |
32 | 31 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β§ π¦ β π) β (π + 1) β€ (β―βπΉ)) |
33 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β§ π¦ β π) β π¦ β π) |
34 | | simplrr 777 |
. . . . . . . . 9
β’ ((((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β§ π¦ β π) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) |
35 | 20, 21, 23, 25, 26, 27, 28, 30, 32, 33, 34 | eupth2lem3 29183 |
. . . . . . . 8
β’ ((((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β§ π¦ β π) β (Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ¦) β π¦ β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
36 | 35 | pm5.32da 580 |
. . . . . . 7
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β ((π¦ β π β§ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ¦)) β (π¦ β π β§ π¦ β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
37 | | 0elpw 5312 |
. . . . . . . . . . 11
β’ β
β π« π |
38 | 20 | wlkepvtx 28611 |
. . . . . . . . . . . . . . . 16
β’ (πΉ(WalksβπΊ)π β ((πβ0) β π β§ (πβ(β―βπΉ)) β π)) |
39 | 38 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (πΉ(WalksβπΊ)π β (πβ0) β π) |
40 | 6, 7, 39 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (πβ0) β π) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (πβ0) β π) |
42 | 20 | wlkp 28567 |
. . . . . . . . . . . . . . . 16
β’ (πΉ(WalksβπΊ)π β π:(0...(β―βπΉ))βΆπ) |
43 | 6, 7, 42 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β π:(0...(β―βπΉ))βΆπ) |
44 | 43 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β π:(0...(β―βπΉ))βΆπ) |
45 | | peano2nn0 12454 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (π + 1) β
β0) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β0) β (π + 1) β
β0) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π + 1) β
β0) |
48 | | nn0uz 12806 |
. . . . . . . . . . . . . . . . 17
β’
β0 = (β€β₯β0) |
49 | 47, 48 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π + 1) β
(β€β₯β0)) |
50 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (β―βπΉ) β
β0) |
51 | 50 | nn0zd 12526 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (β―βπΉ) β β€) |
52 | | elfz5 13434 |
. . . . . . . . . . . . . . . 16
β’ (((π + 1) β
(β€β₯β0) β§ (β―βπΉ) β β€) β ((π + 1) β
(0...(β―βπΉ))
β (π + 1) β€
(β―βπΉ))) |
53 | 49, 51, 52 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β ((π + 1) β (0...(β―βπΉ)) β (π + 1) β€ (β―βπΉ))) |
54 | 31, 53 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π + 1) β (0...(β―βπΉ))) |
55 | 44, 54 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (πβ(π + 1)) β π) |
56 | 41, 55 | prssd 4783 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β {(πβ0), (πβ(π + 1))} β π) |
57 | | prex 5390 |
. . . . . . . . . . . . 13
β’ {(πβ0), (πβ(π + 1))} β V |
58 | 57 | elpw 4565 |
. . . . . . . . . . . 12
β’ ({(πβ0), (πβ(π + 1))} β π« π β {(πβ0), (πβ(π + 1))} β π) |
59 | 56, 58 | sylibr 233 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β {(πβ0), (πβ(π + 1))} β π« π) |
60 | | ifcl 4532 |
. . . . . . . . . . 11
β’ ((β
β π« π β§
{(πβ0), (πβ(π + 1))} β π« π) β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}) β π« π) |
61 | 37, 59, 60 | sylancr 588 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}) β π« π) |
62 | 61 | elpwid 4570 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}) β π) |
63 | 62 | sseld 3944 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π¦ β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}) β π¦ β π)) |
64 | 63 | pm4.71rd 564 |
. . . . . . 7
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π¦ β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}) β (π¦ β π β§ π¦ β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
65 | 36, 64 | bitr4d 282 |
. . . . . 6
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β ((π¦ β π β§ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ¦)) β π¦ β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
66 | 19, 65 | bitrid 283 |
. . . . 5
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β (π¦ β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} β π¦ β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
67 | 66 | eqrdv 2735 |
. . . 4
β’ (((π β§ π β β0) β§ ((π + 1) β€ (β―βπΉ) β§ {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})) |
68 | 67 | exp32 422 |
. . 3
β’ ((π β§ π β β0) β ((π + 1) β€ (β―βπΉ) β ({π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
69 | 68 | a2d 29 |
. 2
β’ ((π β§ π β β0) β (((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) β ((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |
70 | 15, 69 | syld 47 |
1
β’ ((π β§ π β β0) β ((π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) β ((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯
((VtxDegββ¨π,
(πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))})))) |