Step | Hyp | Ref
| Expression |
1 | | eucrct2eupth1.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | | eucrct2eupth1.i |
. . . 4
β’ πΌ = (iEdgβπΊ) |
3 | | eucrct2eupth1.d |
. . . . . 6
β’ (π β πΉ(EulerPathsβπΊ)π) |
4 | 3 | adantl 483 |
. . . . 5
β’ ((π½ = (π β 1) β§ π) β πΉ(EulerPathsβπΊ)π) |
5 | | eucrct2eupth.k |
. . . . . . . 8
β’ πΎ = (π½ + 1) |
6 | 5 | eqcomi 2746 |
. . . . . . 7
β’ (π½ + 1) = πΎ |
7 | 6 | oveq2i 7369 |
. . . . . 6
β’ (πΉ cyclShift (π½ + 1)) = (πΉ cyclShift πΎ) |
8 | | oveq1 7365 |
. . . . . . . . 9
β’ (π½ = (π β 1) β (π½ + 1) = ((π β 1) + 1)) |
9 | | eucrct2eupth.j |
. . . . . . . . . 10
β’ (π β π½ β (0..^π)) |
10 | | elfzo0 13614 |
. . . . . . . . . . 11
β’ (π½ β (0..^π) β (π½ β β0 β§ π β β β§ π½ < π)) |
11 | | nncn 12162 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
12 | 11 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β π β β) |
13 | 10, 12 | sylbi 216 |
. . . . . . . . . 10
β’ (π½ β (0..^π) β π β β) |
14 | | npcan1 11581 |
. . . . . . . . . 10
β’ (π β β β ((π β 1) + 1) = π) |
15 | 9, 13, 14 | 3syl 18 |
. . . . . . . . 9
β’ (π β ((π β 1) + 1) = π) |
16 | 8, 15 | sylan9eq 2797 |
. . . . . . . 8
β’ ((π½ = (π β 1) β§ π) β (π½ + 1) = π) |
17 | 16 | oveq2d 7374 |
. . . . . . 7
β’ ((π½ = (π β 1) β§ π) β (πΉ cyclShift (π½ + 1)) = (πΉ cyclShift π)) |
18 | | eucrct2eupth.n |
. . . . . . . . . 10
β’ (π β π = (β―βπΉ)) |
19 | 18 | oveq2d 7374 |
. . . . . . . . 9
β’ (π β (πΉ cyclShift π) = (πΉ cyclShift (β―βπΉ))) |
20 | | eucrct2eupth1.c |
. . . . . . . . . . 11
β’ (π β πΉ(CircuitsβπΊ)π) |
21 | | crctiswlk 28747 |
. . . . . . . . . . . 12
β’ (πΉ(CircuitsβπΊ)π β πΉ(WalksβπΊ)π) |
22 | 2 | wlkf 28565 |
. . . . . . . . . . . 12
β’ (πΉ(WalksβπΊ)π β πΉ β Word dom πΌ) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
β’ (πΉ(CircuitsβπΊ)π β πΉ β Word dom πΌ) |
24 | 20, 23 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ β Word dom πΌ) |
25 | | cshwn 14686 |
. . . . . . . . . 10
β’ (πΉ β Word dom πΌ β (πΉ cyclShift (β―βπΉ)) = πΉ) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
β’ (π β (πΉ cyclShift (β―βπΉ)) = πΉ) |
27 | 19, 26 | eqtrd 2777 |
. . . . . . . 8
β’ (π β (πΉ cyclShift π) = πΉ) |
28 | 27 | adantl 483 |
. . . . . . 7
β’ ((π½ = (π β 1) β§ π) β (πΉ cyclShift π) = πΉ) |
29 | 17, 28 | eqtrd 2777 |
. . . . . 6
β’ ((π½ = (π β 1) β§ π) β (πΉ cyclShift (π½ + 1)) = πΉ) |
30 | 7, 29 | eqtr3id 2791 |
. . . . 5
β’ ((π½ = (π β 1) β§ π) β (πΉ cyclShift πΎ) = πΉ) |
31 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(β―βπΉ) =
(β―βπΉ) |
32 | 1, 2, 20, 31 | crctcshlem1 28765 |
. . . . . . . . . . . . 13
β’ (π β (β―βπΉ) β
β0) |
33 | | fz0sn0fz1 13559 |
. . . . . . . . . . . . 13
β’
((β―βπΉ)
β β0 β (0...(β―βπΉ)) = ({0} βͺ (1...(β―βπΉ)))) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (0...(β―βπΉ)) = ({0} βͺ
(1...(β―βπΉ)))) |
35 | 34 | eleq2d 2824 |
. . . . . . . . . . 11
β’ (π β (π₯ β (0...(β―βπΉ)) β π₯ β ({0} βͺ (1...(β―βπΉ))))) |
36 | | elun 4109 |
. . . . . . . . . . 11
β’ (π₯ β ({0} βͺ
(1...(β―βπΉ)))
β (π₯ β {0} β¨
π₯ β
(1...(β―βπΉ)))) |
37 | 35, 36 | bitrdi 287 |
. . . . . . . . . 10
β’ (π β (π₯ β (0...(β―βπΉ)) β (π₯ β {0} β¨ π₯ β (1...(β―βπΉ))))) |
38 | | elsni 4604 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β {0} β π₯ = 0) |
39 | | 0le0 12255 |
. . . . . . . . . . . . . . . 16
β’ 0 β€
0 |
40 | 38, 39 | eqbrtrdi 5145 |
. . . . . . . . . . . . . . 15
β’ (π₯ β {0} β π₯ β€ 0) |
41 | 40 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β {0}) β π₯ β€ 0) |
42 | 41 | iftrued 4495 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β {0}) β if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = (πβ(π₯ + π))) |
43 | 18 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πβπ) = (πβ(β―βπΉ))) |
44 | | crctprop 28743 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ(CircuitsβπΊ)π β (πΉ(TrailsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) |
45 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ(TrailsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (πβ0) = (πβ(β―βπΉ))) |
46 | 45 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ(TrailsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ))) β (πβ(β―βπΉ)) = (πβ0)) |
47 | 20, 44, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πβ(β―βπΉ)) = (πβ0)) |
48 | 43, 47 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβπ) = (πβ0)) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ = 0) β (πβπ) = (πβ0)) |
50 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = 0 β (π₯ + π) = (0 + π)) |
51 | 9, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
52 | 51 | addid2d 11357 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0 + π) = π) |
53 | 50, 52 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ = 0) β (π₯ + π) = π) |
54 | 53 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ = 0) β (πβ(π₯ + π)) = (πβπ)) |
55 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = 0 β (πβπ₯) = (πβ0)) |
56 | 55 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ = 0) β (πβπ₯) = (πβ0)) |
57 | 49, 54, 56 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ = 0) β (πβ(π₯ + π)) = (πβπ₯)) |
58 | 38, 57 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β {0}) β (πβ(π₯ + π)) = (πβπ₯)) |
59 | 42, 58 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β {0}) β if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = (πβπ₯)) |
60 | 59 | ex 414 |
. . . . . . . . . . 11
β’ (π β (π₯ β {0} β if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = (πβπ₯))) |
61 | | elfznn 13471 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β
(1...(β―βπΉ))
β π₯ β
β) |
62 | | nnnle0 12187 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β Β¬
π₯ β€ 0) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π₯ β
(1...(β―βπΉ))
β Β¬ π₯ β€
0) |
64 | 63 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...(β―βπΉ))) β Β¬ π₯ β€ 0) |
65 | 64 | iffalsed 4498 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...(β―βπΉ))) β if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = (πβ((π₯ + π) β π))) |
66 | 61 | nncnd 12170 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β
(1...(β―βπΉ))
β π₯ β
β) |
67 | 66 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1...(β―βπΉ))) β π₯ β β) |
68 | 51 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1...(β―βπΉ))) β π β β) |
69 | 67, 68 | pncand 11514 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...(β―βπΉ))) β ((π₯ + π) β π) = π₯) |
70 | 69 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...(β―βπΉ))) β (πβ((π₯ + π) β π)) = (πβπ₯)) |
71 | 65, 70 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...(β―βπΉ))) β if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = (πβπ₯)) |
72 | 71 | ex 414 |
. . . . . . . . . . 11
β’ (π β (π₯ β (1...(β―βπΉ)) β if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = (πβπ₯))) |
73 | 60, 72 | jaod 858 |
. . . . . . . . . 10
β’ (π β ((π₯ β {0} β¨ π₯ β (1...(β―βπΉ))) β if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = (πβπ₯))) |
74 | 37, 73 | sylbid 239 |
. . . . . . . . 9
β’ (π β (π₯ β (0...(β―βπΉ)) β if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = (πβπ₯))) |
75 | 74 | imp 408 |
. . . . . . . 8
β’ ((π β§ π₯ β (0...(β―βπΉ))) β if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = (πβπ₯)) |
76 | 75 | mpteq2dva 5206 |
. . . . . . 7
β’ (π β (π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) = (π₯ β (0...(β―βπΉ)) β¦ (πβπ₯))) |
77 | 76 | adantl 483 |
. . . . . 6
β’ ((π½ = (π β 1) β§ π) β (π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) = (π₯ β (0...(β―βπΉ)) β¦ (πβπ₯))) |
78 | 5 | oveq2i 7369 |
. . . . . . . . . 10
β’ (π β πΎ) = (π β (π½ + 1)) |
79 | 8 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π½ = (π β 1) β (π β (π½ + 1)) = (π β ((π β 1) + 1))) |
80 | 15 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π β (π β ((π β 1) + 1)) = (π β π)) |
81 | 51 | subidd 11501 |
. . . . . . . . . . . 12
β’ (π β (π β π) = 0) |
82 | 80, 81 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β (π β ((π β 1) + 1)) = 0) |
83 | 79, 82 | sylan9eq 2797 |
. . . . . . . . . 10
β’ ((π½ = (π β 1) β§ π) β (π β (π½ + 1)) = 0) |
84 | 78, 83 | eqtrid 2789 |
. . . . . . . . 9
β’ ((π½ = (π β 1) β§ π) β (π β πΎ) = 0) |
85 | 84 | breq2d 5118 |
. . . . . . . 8
β’ ((π½ = (π β 1) β§ π) β (π₯ β€ (π β πΎ) β π₯ β€ 0)) |
86 | 5 | oveq2i 7369 |
. . . . . . . . . 10
β’ (π₯ + πΎ) = (π₯ + (π½ + 1)) |
87 | 86 | fveq2i 6846 |
. . . . . . . . 9
β’ (πβ(π₯ + πΎ)) = (πβ(π₯ + (π½ + 1))) |
88 | 8 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π½ = (π β 1) β (π₯ + (π½ + 1)) = (π₯ + ((π β 1) + 1))) |
89 | 15 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π β (π₯ + ((π β 1) + 1)) = (π₯ + π)) |
90 | 88, 89 | sylan9eq 2797 |
. . . . . . . . . 10
β’ ((π½ = (π β 1) β§ π) β (π₯ + (π½ + 1)) = (π₯ + π)) |
91 | 90 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π½ = (π β 1) β§ π) β (πβ(π₯ + (π½ + 1))) = (πβ(π₯ + π))) |
92 | 87, 91 | eqtrid 2789 |
. . . . . . . 8
β’ ((π½ = (π β 1) β§ π) β (πβ(π₯ + πΎ)) = (πβ(π₯ + π))) |
93 | 86 | oveq1i 7368 |
. . . . . . . . . 10
β’ ((π₯ + πΎ) β π) = ((π₯ + (π½ + 1)) β π) |
94 | 93 | fveq2i 6846 |
. . . . . . . . 9
β’ (πβ((π₯ + πΎ) β π)) = (πβ((π₯ + (π½ + 1)) β π)) |
95 | 88 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π½ = (π β 1) β ((π₯ + (π½ + 1)) β π) = ((π₯ + ((π β 1) + 1)) β π)) |
96 | 89 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π β ((π₯ + ((π β 1) + 1)) β π) = ((π₯ + π) β π)) |
97 | 95, 96 | sylan9eq 2797 |
. . . . . . . . . 10
β’ ((π½ = (π β 1) β§ π) β ((π₯ + (π½ + 1)) β π) = ((π₯ + π) β π)) |
98 | 97 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π½ = (π β 1) β§ π) β (πβ((π₯ + (π½ + 1)) β π)) = (πβ((π₯ + π) β π))) |
99 | 94, 98 | eqtrid 2789 |
. . . . . . . 8
β’ ((π½ = (π β 1) β§ π) β (πβ((π₯ + πΎ) β π)) = (πβ((π₯ + π) β π))) |
100 | 85, 92, 99 | ifbieq12d 4515 |
. . . . . . 7
β’ ((π½ = (π β 1) β§ π) β if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π))) = if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) |
101 | 100 | mpteq2dv 5208 |
. . . . . 6
β’ ((π½ = (π β 1) β§ π) β (π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) = (π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ 0, (πβ(π₯ + π)), (πβ((π₯ + π) β π))))) |
102 | 20, 21 | syl 17 |
. . . . . . . . 9
β’ (π β πΉ(WalksβπΊ)π) |
103 | 1 | wlkp 28567 |
. . . . . . . . 9
β’ (πΉ(WalksβπΊ)π β π:(0...(β―βπΉ))βΆπ) |
104 | | ffn 6669 |
. . . . . . . . 9
β’ (π:(0...(β―βπΉ))βΆπ β π Fn (0...(β―βπΉ))) |
105 | 102, 103,
104 | 3syl 18 |
. . . . . . . 8
β’ (π β π Fn (0...(β―βπΉ))) |
106 | 105 | adantl 483 |
. . . . . . 7
β’ ((π½ = (π β 1) β§ π) β π Fn (0...(β―βπΉ))) |
107 | | dffn5 6902 |
. . . . . . 7
β’ (π Fn (0...(β―βπΉ)) β π = (π₯ β (0...(β―βπΉ)) β¦ (πβπ₯))) |
108 | 106, 107 | sylib 217 |
. . . . . 6
β’ ((π½ = (π β 1) β§ π) β π = (π₯ β (0...(β―βπΉ)) β¦ (πβπ₯))) |
109 | 77, 101, 108 | 3eqtr4d 2787 |
. . . . 5
β’ ((π½ = (π β 1) β§ π) β (π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) = π) |
110 | 4, 30, 109 | 3brtr4d 5138 |
. . . 4
β’ ((π½ = (π β 1) β§ π) β (πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π))))) |
111 | 20 | adantl 483 |
. . . . 5
β’ ((π½ = (π β 1) β§ π) β πΉ(CircuitsβπΊ)π) |
112 | 111, 30, 109 | 3brtr4d 5138 |
. . . 4
β’ ((π½ = (π β 1) β§ π) β (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π))))) |
113 | | eucrct2eupth1.s |
. . . 4
β’
(Vtxβπ) =
π |
114 | | elfzolt3 13583 |
. . . . . . 7
β’ (π½ β (0..^π) β 0 < π) |
115 | 9, 114 | syl 17 |
. . . . . 6
β’ (π β 0 < π) |
116 | | elfzoelz 13573 |
. . . . . . . . . . 11
β’ (π½ β (0..^π) β π½ β β€) |
117 | 9, 116 | syl 17 |
. . . . . . . . . 10
β’ (π β π½ β β€) |
118 | 117 | peano2zd 12611 |
. . . . . . . . 9
β’ (π β (π½ + 1) β β€) |
119 | 5, 118 | eqeltrid 2842 |
. . . . . . . 8
β’ (π β πΎ β β€) |
120 | | cshwlen 14688 |
. . . . . . . . 9
β’ ((πΉ β Word dom πΌ β§ πΎ β β€) β
(β―β(πΉ cyclShift
πΎ)) = (β―βπΉ)) |
121 | 120 | eqcomd 2743 |
. . . . . . . 8
β’ ((πΉ β Word dom πΌ β§ πΎ β β€) β (β―βπΉ) = (β―β(πΉ cyclShift πΎ))) |
122 | 24, 119, 121 | syl2anc 585 |
. . . . . . 7
β’ (π β (β―βπΉ) = (β―β(πΉ cyclShift πΎ))) |
123 | 18, 122 | eqtrd 2777 |
. . . . . 6
β’ (π β π = (β―β(πΉ cyclShift πΎ))) |
124 | 115, 123 | breqtrd 5132 |
. . . . 5
β’ (π β 0 <
(β―β(πΉ cyclShift
πΎ))) |
125 | 124 | adantl 483 |
. . . 4
β’ ((π½ = (π β 1) β§ π) β 0 < (β―β(πΉ cyclShift πΎ))) |
126 | 123 | adantl 483 |
. . . . 5
β’ ((π½ = (π β 1) β§ π) β π = (β―β(πΉ cyclShift πΎ))) |
127 | 126 | oveq1d 7373 |
. . . 4
β’ ((π½ = (π β 1) β§ π) β (π β 1) = ((β―β(πΉ cyclShift πΎ)) β 1)) |
128 | | eucrct2eupth.e |
. . . . . 6
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β ((0..^π) β {π½})))) |
129 | 128 | adantl 483 |
. . . . 5
β’ ((π½ = (π β 1) β§ π) β (iEdgβπ) = (πΌ βΎ (πΉ β ((0..^π) β {π½})))) |
130 | 24, 18, 9 | 3jca 1129 |
. . . . . . . . 9
β’ (π β (πΉ β Word dom πΌ β§ π = (β―βπΉ) β§ π½ β (0..^π))) |
131 | 130 | adantl 483 |
. . . . . . . 8
β’ ((π½ = (π β 1) β§ π) β (πΉ β Word dom πΌ β§ π = (β―βπΉ) β§ π½ β (0..^π))) |
132 | | cshimadifsn0 14720 |
. . . . . . . 8
β’ ((πΉ β Word dom πΌ β§ π = (β―βπΉ) β§ π½ β (0..^π)) β (πΉ β ((0..^π) β {π½})) = ((πΉ cyclShift (π½ + 1)) β (0..^(π β 1)))) |
133 | 131, 132 | syl 17 |
. . . . . . 7
β’ ((π½ = (π β 1) β§ π) β (πΉ β ((0..^π) β {π½})) = ((πΉ cyclShift (π½ + 1)) β (0..^(π β 1)))) |
134 | 7 | imaeq1i 6011 |
. . . . . . 7
β’ ((πΉ cyclShift (π½ + 1)) β (0..^(π β 1))) = ((πΉ cyclShift πΎ) β (0..^(π β 1))) |
135 | 133, 134 | eqtrdi 2793 |
. . . . . 6
β’ ((π½ = (π β 1) β§ π) β (πΉ β ((0..^π) β {π½})) = ((πΉ cyclShift πΎ) β (0..^(π β 1)))) |
136 | 135 | reseq2d 5938 |
. . . . 5
β’ ((π½ = (π β 1) β§ π) β (πΌ βΎ (πΉ β ((0..^π) β {π½}))) = (πΌ βΎ ((πΉ cyclShift πΎ) β (0..^(π β 1))))) |
137 | 129, 136 | eqtrd 2777 |
. . . 4
β’ ((π½ = (π β 1) β§ π) β (iEdgβπ) = (πΌ βΎ ((πΉ cyclShift πΎ) β (0..^(π β 1))))) |
138 | | eqid 2737 |
. . . 4
β’ ((πΉ cyclShift πΎ) prefix (π β 1)) = ((πΉ cyclShift πΎ) prefix (π β 1)) |
139 | | eqid 2737 |
. . . 4
β’ ((π₯ β
(0...(β―βπΉ))
β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0...(π β 1))) = ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0...(π β 1))) |
140 | 1, 2, 110, 112, 113, 125, 127, 137, 138, 139 | eucrct2eupth1 29191 |
. . 3
β’ ((π½ = (π β 1) β§ π) β ((πΉ cyclShift πΎ) prefix (π β 1))(EulerPathsβπ)((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0...(π β 1)))) |
141 | | eucrct2eupth.h |
. . . 4
β’ π» = ((πΉ cyclShift πΎ) prefix (π β 1)) |
142 | 141 | a1i 11 |
. . 3
β’ ((π½ = (π β 1) β§ π) β π» = ((πΉ cyclShift πΎ) prefix (π β 1))) |
143 | | eucrct2eupth.q |
. . . . 5
β’ π = (π₯ β (0..^π) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) |
144 | | fzossfz 13592 |
. . . . . . . 8
β’
(0..^π) β
(0...π) |
145 | 18 | oveq2d 7374 |
. . . . . . . 8
β’ (π β (0...π) = (0...(β―βπΉ))) |
146 | 144, 145 | sseqtrid 3997 |
. . . . . . 7
β’ (π β (0..^π) β (0...(β―βπΉ))) |
147 | 146 | resmptd 5995 |
. . . . . 6
β’ (π β ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0..^π)) = (π₯ β (0..^π) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π))))) |
148 | | elfzoel2 13572 |
. . . . . . . 8
β’ (π½ β (0..^π) β π β β€) |
149 | | fzoval 13574 |
. . . . . . . 8
β’ (π β β€ β
(0..^π) = (0...(π β 1))) |
150 | 9, 148, 149 | 3syl 18 |
. . . . . . 7
β’ (π β (0..^π) = (0...(π β 1))) |
151 | 150 | reseq2d 5938 |
. . . . . 6
β’ (π β ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0..^π)) = ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0...(π β 1)))) |
152 | 147, 151 | eqtr3d 2779 |
. . . . 5
β’ (π β (π₯ β (0..^π) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) = ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0...(π β 1)))) |
153 | 143, 152 | eqtrid 2789 |
. . . 4
β’ (π β π = ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0...(π β 1)))) |
154 | 153 | adantl 483 |
. . 3
β’ ((π½ = (π β 1) β§ π) β π = ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0...(π β 1)))) |
155 | 140, 142,
154 | 3brtr4d 5138 |
. 2
β’ ((π½ = (π β 1) β§ π) β π»(EulerPathsβπ)π) |
156 | 20 | adantl 483 |
. . . 4
β’ ((Β¬
π½ = (π β 1) β§ π) β πΉ(CircuitsβπΊ)π) |
157 | | peano2nn0 12454 |
. . . . . . . . . . . . 13
β’ (π½ β β0
β (π½ + 1) β
β0) |
158 | 157 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β (π½ + 1) β
β0) |
159 | 158 | adantr 482 |
. . . . . . . . . . 11
β’ (((π½ β β0
β§ π β β
β§ π½ < π) β§ Β¬ π½ = (π β 1)) β (π½ + 1) β
β0) |
160 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π½ β β0
β§ π β β
β§ π½ < π) β§ Β¬ π½ = (π β 1)) β π β β) |
161 | | 1cnd 11151 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β 1 β
β) |
162 | | nn0cn 12424 |
. . . . . . . . . . . . . . . . 17
β’ (π½ β β0
β π½ β
β) |
163 | 162 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β π½ β β) |
164 | 12, 161, 163 | subadd2d 11532 |
. . . . . . . . . . . . . . 15
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β ((π β 1) = π½ β (π½ + 1) = π)) |
165 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
β’ (π½ = (π β 1) β (π β 1) = π½) |
166 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
β’ (π = (π½ + 1) β (π½ + 1) = π) |
167 | 164, 165,
166 | 3bitr4g 314 |
. . . . . . . . . . . . . 14
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β (π½ = (π β 1) β π = (π½ + 1))) |
168 | 167 | necon3bbid 2982 |
. . . . . . . . . . . . 13
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β (Β¬ π½ = (π β 1) β π β (π½ + 1))) |
169 | 157 | nn0red 12475 |
. . . . . . . . . . . . . . . 16
β’ (π½ β β0
β (π½ + 1) β
β) |
170 | 169 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β (π½ + 1) β β) |
171 | | nnre 12161 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
172 | 171 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β π β β) |
173 | | nn0z 12525 |
. . . . . . . . . . . . . . . . 17
β’ (π½ β β0
β π½ β
β€) |
174 | | nnz 12521 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β€) |
175 | | zltp1le 12554 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β β€ β§ π β β€) β (π½ < π β (π½ + 1) β€ π)) |
176 | 173, 174,
175 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β β0
β§ π β β)
β (π½ < π β (π½ + 1) β€ π)) |
177 | 176 | biimp3a 1470 |
. . . . . . . . . . . . . . 15
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β (π½ + 1) β€ π) |
178 | 170, 172,
177 | leltned 11309 |
. . . . . . . . . . . . . 14
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β ((π½ + 1) < π β π β (π½ + 1))) |
179 | 178 | biimprd 248 |
. . . . . . . . . . . . 13
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β (π β (π½ + 1) β (π½ + 1) < π)) |
180 | 168, 179 | sylbid 239 |
. . . . . . . . . . . 12
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β (Β¬ π½ = (π β 1) β (π½ + 1) < π)) |
181 | 180 | imp 408 |
. . . . . . . . . . 11
β’ (((π½ β β0
β§ π β β
β§ π½ < π) β§ Β¬ π½ = (π β 1)) β (π½ + 1) < π) |
182 | 159, 160,
181 | 3jca 1129 |
. . . . . . . . . 10
β’ (((π½ β β0
β§ π β β
β§ π½ < π) β§ Β¬ π½ = (π β 1)) β ((π½ + 1) β β0 β§ π β β β§ (π½ + 1) < π)) |
183 | 182 | ex 414 |
. . . . . . . . 9
β’ ((π½ β β0
β§ π β β
β§ π½ < π) β (Β¬ π½ = (π β 1) β ((π½ + 1) β β0 β§ π β β β§ (π½ + 1) < π))) |
184 | 10, 183 | sylbi 216 |
. . . . . . . 8
β’ (π½ β (0..^π) β (Β¬ π½ = (π β 1) β ((π½ + 1) β β0 β§ π β β β§ (π½ + 1) < π))) |
185 | | elfzo0 13614 |
. . . . . . . 8
β’ ((π½ + 1) β (0..^π) β ((π½ + 1) β β0 β§ π β β β§ (π½ + 1) < π)) |
186 | 184, 185 | syl6ibr 252 |
. . . . . . 7
β’ (π½ β (0..^π) β (Β¬ π½ = (π β 1) β (π½ + 1) β (0..^π))) |
187 | 9, 186 | syl 17 |
. . . . . 6
β’ (π β (Β¬ π½ = (π β 1) β (π½ + 1) β (0..^π))) |
188 | 187 | impcom 409 |
. . . . 5
β’ ((Β¬
π½ = (π β 1) β§ π) β (π½ + 1) β (0..^π)) |
189 | 5 | a1i 11 |
. . . . 5
β’ ((Β¬
π½ = (π β 1) β§ π) β πΎ = (π½ + 1)) |
190 | 18 | eqcomd 2743 |
. . . . . . 7
β’ (π β (β―βπΉ) = π) |
191 | 190 | oveq2d 7374 |
. . . . . 6
β’ (π β (0..^(β―βπΉ)) = (0..^π)) |
192 | 191 | adantl 483 |
. . . . 5
β’ ((Β¬
π½ = (π β 1) β§ π) β (0..^(β―βπΉ)) = (0..^π)) |
193 | 188, 189,
192 | 3eltr4d 2853 |
. . . 4
β’ ((Β¬
π½ = (π β 1) β§ π) β πΎ β (0..^(β―βπΉ))) |
194 | | eqid 2737 |
. . . 4
β’ (πΉ cyclShift πΎ) = (πΉ cyclShift πΎ) |
195 | | eqid 2737 |
. . . 4
β’ (π₯ β
(0...(β―βπΉ))
β¦ if(π₯ β€
((β―βπΉ) β
πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) = (π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) |
196 | 3 | adantl 483 |
. . . 4
β’ ((Β¬
π½ = (π β 1) β§ π) β πΉ(EulerPathsβπΊ)π) |
197 | 1, 2, 156, 31, 193, 194, 195, 196 | eucrctshift 29190 |
. . 3
β’ ((Β¬
π½ = (π β 1) β§ π) β ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) |
198 | | simprl 770 |
. . . . 5
β’ (((Β¬
π½ = (π β 1) β§ π) β§ ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) β (πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ)))))) |
199 | | simprr 772 |
. . . . 5
β’ (((Β¬
π½ = (π β 1) β§ π) β§ ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) β (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ)))))) |
200 | 124 | ad2antlr 726 |
. . . . 5
β’ (((Β¬
π½ = (π β 1) β§ π) β§ ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) β 0 < (β―β(πΉ cyclShift πΎ))) |
201 | 123 | oveq1d 7373 |
. . . . . 6
β’ (π β (π β 1) = ((β―β(πΉ cyclShift πΎ)) β 1)) |
202 | 201 | ad2antlr 726 |
. . . . 5
β’ (((Β¬
π½ = (π β 1) β§ π) β§ ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) β (π β 1) = ((β―β(πΉ cyclShift πΎ)) β 1)) |
203 | 128 | adantl 483 |
. . . . . . 7
β’ ((Β¬
π½ = (π β 1) β§ π) β (iEdgβπ) = (πΌ βΎ (πΉ β ((0..^π) β {π½})))) |
204 | 130 | adantl 483 |
. . . . . . . . . 10
β’ ((Β¬
π½ = (π β 1) β§ π) β (πΉ β Word dom πΌ β§ π = (β―βπΉ) β§ π½ β (0..^π))) |
205 | 204, 132 | syl 17 |
. . . . . . . . 9
β’ ((Β¬
π½ = (π β 1) β§ π) β (πΉ β ((0..^π) β {π½})) = ((πΉ cyclShift (π½ + 1)) β (0..^(π β 1)))) |
206 | 205, 134 | eqtrdi 2793 |
. . . . . . . 8
β’ ((Β¬
π½ = (π β 1) β§ π) β (πΉ β ((0..^π) β {π½})) = ((πΉ cyclShift πΎ) β (0..^(π β 1)))) |
207 | 206 | reseq2d 5938 |
. . . . . . 7
β’ ((Β¬
π½ = (π β 1) β§ π) β (πΌ βΎ (πΉ β ((0..^π) β {π½}))) = (πΌ βΎ ((πΉ cyclShift πΎ) β (0..^(π β 1))))) |
208 | 203, 207 | eqtrd 2777 |
. . . . . 6
β’ ((Β¬
π½ = (π β 1) β§ π) β (iEdgβπ) = (πΌ βΎ ((πΉ cyclShift πΎ) β (0..^(π β 1))))) |
209 | 208 | adantr 482 |
. . . . 5
β’ (((Β¬
π½ = (π β 1) β§ π) β§ ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) β (iEdgβπ) = (πΌ βΎ ((πΉ cyclShift πΎ) β (0..^(π β 1))))) |
210 | | eqid 2737 |
. . . . 5
β’ ((π₯ β
(0...(β―βπΉ))
β¦ if(π₯ β€
((β―βπΉ) β
πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) βΎ (0...(π β 1))) = ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) βΎ (0...(π β 1))) |
211 | 1, 2, 198, 199, 113, 200, 202, 209, 138, 210 | eucrct2eupth1 29191 |
. . . 4
β’ (((Β¬
π½ = (π β 1) β§ π) β§ ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) β ((πΉ cyclShift πΎ) prefix (π β 1))(EulerPathsβπ)((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) βΎ (0...(π β 1)))) |
212 | 141 | a1i 11 |
. . . 4
β’ (((Β¬
π½ = (π β 1) β§ π) β§ ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) β π» = ((πΉ cyclShift πΎ) prefix (π β 1))) |
213 | 190 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π β ((β―βπΉ) β πΎ) = (π β πΎ)) |
214 | 213 | breq2d 5118 |
. . . . . . . . . . 11
β’ (π β (π₯ β€ ((β―βπΉ) β πΎ) β π₯ β€ (π β πΎ))) |
215 | 214 | adantl 483 |
. . . . . . . . . 10
β’ ((Β¬
π½ = (π β 1) β§ π) β (π₯ β€ ((β―βπΉ) β πΎ) β π₯ β€ (π β πΎ))) |
216 | 190 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π β ((π₯ + πΎ) β (β―βπΉ)) = ((π₯ + πΎ) β π)) |
217 | 216 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π β (πβ((π₯ + πΎ) β (β―βπΉ))) = (πβ((π₯ + πΎ) β π))) |
218 | 217 | adantl 483 |
. . . . . . . . . 10
β’ ((Β¬
π½ = (π β 1) β§ π) β (πβ((π₯ + πΎ) β (β―βπΉ))) = (πβ((π₯ + πΎ) β π))) |
219 | 215, 218 | ifbieq2d 4513 |
. . . . . . . . 9
β’ ((Β¬
π½ = (π β 1) β§ π) β if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ)))) = if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) |
220 | 219 | mpteq2dv 5208 |
. . . . . . . 8
β’ ((Β¬
π½ = (π β 1) β§ π) β (π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) = (π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π))))) |
221 | 150 | eqcomd 2743 |
. . . . . . . . 9
β’ (π β (0...(π β 1)) = (0..^π)) |
222 | 221 | adantl 483 |
. . . . . . . 8
β’ ((Β¬
π½ = (π β 1) β§ π) β (0...(π β 1)) = (0..^π)) |
223 | 220, 222 | reseq12d 5939 |
. . . . . . 7
β’ ((Β¬
π½ = (π β 1) β§ π) β ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) βΎ (0...(π β 1))) = ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0..^π))) |
224 | 18 | adantl 483 |
. . . . . . . . . 10
β’ ((Β¬
π½ = (π β 1) β§ π) β π = (β―βπΉ)) |
225 | 224 | oveq2d 7374 |
. . . . . . . . 9
β’ ((Β¬
π½ = (π β 1) β§ π) β (0...π) = (0...(β―βπΉ))) |
226 | 144, 225 | sseqtrid 3997 |
. . . . . . . 8
β’ ((Β¬
π½ = (π β 1) β§ π) β (0..^π) β (0...(β―βπΉ))) |
227 | 226 | resmptd 5995 |
. . . . . . 7
β’ ((Β¬
π½ = (π β 1) β§ π) β ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) βΎ (0..^π)) = (π₯ β (0..^π) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π))))) |
228 | 223, 227 | eqtrd 2777 |
. . . . . 6
β’ ((Β¬
π½ = (π β 1) β§ π) β ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) βΎ (0...(π β 1))) = (π₯ β (0..^π) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π))))) |
229 | 143, 228 | eqtr4id 2796 |
. . . . 5
β’ ((Β¬
π½ = (π β 1) β§ π) β π = ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) βΎ (0...(π β 1)))) |
230 | 229 | adantr 482 |
. . . 4
β’ (((Β¬
π½ = (π β 1) β§ π) β§ ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) β π = ((π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) βΎ (0...(π β 1)))) |
231 | 211, 212,
230 | 3brtr4d 5138 |
. . 3
β’ (((Β¬
π½ = (π β 1) β§ π) β§ ((πΉ cyclShift πΎ)(EulerPathsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))) β§ (πΉ cyclShift πΎ)(CircuitsβπΊ)(π₯ β (0...(β―βπΉ)) β¦ if(π₯ β€ ((β―βπΉ) β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β (β―βπΉ))))))) β π»(EulerPathsβπ)π) |
232 | 197, 231 | mpdan 686 |
. 2
β’ ((Β¬
π½ = (π β 1) β§ π) β π»(EulerPathsβπ)π) |
233 | 155, 232 | pm2.61ian 811 |
1
β’ (π β π»(EulerPathsβπ)π) |