Proof of Theorem eucrct2eupth
Step | Hyp | Ref
| Expression |
1 | | eucrct2eupth1.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | eucrct2eupth1.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝐺) |
3 | | eucrct2eupth1.d |
. . . . . 6
⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) |
4 | 3 | adantl 482 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃) |
5 | | eucrct2eupth.k |
. . . . . . . 8
⊢ 𝐾 = (𝐽 + 1) |
6 | 5 | eqcomi 2749 |
. . . . . . 7
⊢ (𝐽 + 1) = 𝐾 |
7 | 6 | oveq2i 7283 |
. . . . . 6
⊢ (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾) |
8 | | oveq1 7279 |
. . . . . . . . 9
⊢ (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1)) |
9 | | eucrct2eupth.j |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) |
10 | | elfzo0 13439 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) |
11 | | nncn 11992 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
12 | 11 | 3ad2ant2 1133 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ) |
13 | 10, 12 | sylbi 216 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ) |
14 | | npcan1 11411 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
15 | 9, 13, 14 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
16 | 8, 15 | sylan9eq 2800 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁) |
17 | 16 | oveq2d 7288 |
. . . . . . 7
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁)) |
18 | | eucrct2eupth.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 = (♯‘𝐹)) |
19 | 18 | oveq2d 7288 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹))) |
20 | | eucrct2eupth1.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃) |
21 | | crctiswlk 28173 |
. . . . . . . . . . . 12
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
22 | 2 | wlkf 27992 |
. . . . . . . . . . . 12
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
24 | 20, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
25 | | cshwn 14521 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹) |
27 | 19, 26 | eqtrd 2780 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹) |
28 | 27 | adantl 482 |
. . . . . . 7
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹) |
29 | 17, 28 | eqtrd 2780 |
. . . . . 6
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹) |
30 | 7, 29 | eqtr3id 2794 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹) |
31 | | eqid 2740 |
. . . . . . . . . . . . . 14
⊢
(♯‘𝐹) =
(♯‘𝐹) |
32 | 1, 2, 20, 31 | crctcshlem1 28191 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐹) ∈
ℕ0) |
33 | | fz0sn0fz1 13384 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹)
∈ ℕ0 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹)))) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0...(♯‘𝐹)) = ({0} ∪
(1...(♯‘𝐹)))) |
35 | 34 | eleq2d 2826 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))))) |
36 | | elun 4088 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ({0} ∪
(1...(♯‘𝐹)))
↔ (𝑥 ∈ {0} ∨
𝑥 ∈
(1...(♯‘𝐹)))) |
37 | 35, 36 | bitrdi 287 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))) |
38 | | elsni 4584 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {0} → 𝑥 = 0) |
39 | | 0le0 12085 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
0 |
40 | 38, 39 | eqbrtrdi 5118 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {0} → 𝑥 ≤ 0) |
41 | 40 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → 𝑥 ≤ 0) |
42 | 41 | iftrued 4473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁))) |
43 | 18 | fveq2d 6775 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘(♯‘𝐹))) |
44 | | crctprop 28169 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) |
45 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) = (𝑃‘(♯‘𝐹))) |
46 | 45 | eqcomd 2746 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) = (𝑃‘0)) |
47 | 20, 44, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑃‘(♯‘𝐹)) = (𝑃‘0)) |
48 | 43, 47 | eqtrd 2780 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0)) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑁) = (𝑃‘0)) |
50 | | oveq1 7279 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁)) |
51 | 9, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℂ) |
52 | 51 | addid2d 11187 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0 + 𝑁) = 𝑁) |
53 | 50, 52 | sylan9eqr 2802 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑥 + 𝑁) = 𝑁) |
54 | 53 | fveq2d 6775 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑁)) |
55 | | fveq2 6771 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → (𝑃‘𝑥) = (𝑃‘0)) |
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑥) = (𝑃‘0)) |
57 | 49, 54, 56 | 3eqtr4d 2790 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥)) |
58 | 38, 57 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥)) |
59 | 42, 58 | eqtrd 2780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)) |
60 | 59 | ex 413 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))) |
61 | | elfznn 13296 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
(1...(♯‘𝐹))
→ 𝑥 ∈
ℕ) |
62 | | nnnle0 12017 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ → ¬
𝑥 ≤ 0) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
(1...(♯‘𝐹))
→ ¬ 𝑥 ≤
0) |
64 | 63 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0) |
65 | 64 | iffalsed 4476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁))) |
66 | 61 | nncnd 12000 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
(1...(♯‘𝐹))
→ 𝑥 ∈
ℂ) |
67 | 66 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ) |
68 | 51 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ) |
69 | 67, 68 | pncand 11344 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥) |
70 | 69 | fveq2d 6775 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃‘𝑥)) |
71 | 65, 70 | eqtrd 2780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)) |
72 | 71 | ex 413 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))) |
73 | 60, 72 | jaod 856 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))) |
74 | 37, 73 | sylbid 239 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))) |
75 | 74 | imp 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)) |
76 | 75 | mpteq2dva 5179 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥))) |
77 | 76 | adantl 482 |
. . . . . 6
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥))) |
78 | 5 | oveq2i 7283 |
. . . . . . . . . 10
⊢ (𝑁 − 𝐾) = (𝑁 − (𝐽 + 1)) |
79 | 8 | oveq2d 7288 |
. . . . . . . . . . 11
⊢ (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1))) |
80 | 15 | oveq2d 7288 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁 − 𝑁)) |
81 | 51 | subidd 11331 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − 𝑁) = 0) |
82 | 80, 81 | eqtrd 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0) |
83 | 79, 82 | sylan9eq 2800 |
. . . . . . . . . 10
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0) |
84 | 78, 83 | eqtrid 2792 |
. . . . . . . . 9
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 𝐾) = 0) |
85 | 84 | breq2d 5091 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁 − 𝐾) ↔ 𝑥 ≤ 0)) |
86 | 5 | oveq2i 7283 |
. . . . . . . . . 10
⊢ (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1)) |
87 | 86 | fveq2i 6774 |
. . . . . . . . 9
⊢ (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1))) |
88 | 8 | oveq2d 7288 |
. . . . . . . . . . 11
⊢ (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1))) |
89 | 15 | oveq2d 7288 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁)) |
90 | 88, 89 | sylan9eq 2800 |
. . . . . . . . . 10
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁)) |
91 | 90 | fveq2d 6775 |
. . . . . . . . 9
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁))) |
92 | 87, 91 | eqtrid 2792 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁))) |
93 | 86 | oveq1i 7282 |
. . . . . . . . . 10
⊢ ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁) |
94 | 93 | fveq2i 6774 |
. . . . . . . . 9
⊢ (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) |
95 | 88 | oveq1d 7287 |
. . . . . . . . . . 11
⊢ (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁)) |
96 | 89 | oveq1d 7287 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁)) |
97 | 95, 96 | sylan9eq 2800 |
. . . . . . . . . 10
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁)) |
98 | 97 | fveq2d 6775 |
. . . . . . . . 9
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁))) |
99 | 94, 98 | eqtrid 2792 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁))) |
100 | 85, 92, 99 | ifbieq12d 4493 |
. . . . . . 7
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) |
101 | 100 | mpteq2dv 5181 |
. . . . . 6
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))) |
102 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) |
103 | 1 | wlkp 27994 |
. . . . . . . . 9
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
104 | | ffn 6598 |
. . . . . . . . 9
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...(♯‘𝐹))) |
105 | 102, 103,
104 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 Fn (0...(♯‘𝐹))) |
106 | 105 | adantl 482 |
. . . . . . 7
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹))) |
107 | | dffn5 6825 |
. . . . . . 7
⊢ (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥))) |
108 | 106, 107 | sylib 217 |
. . . . . 6
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥))) |
109 | 77, 101, 108 | 3eqtr4d 2790 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃) |
110 | 4, 30, 109 | 3brtr4d 5111 |
. . . 4
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
111 | 20 | adantl 482 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃) |
112 | 111, 30, 109 | 3brtr4d 5111 |
. . . 4
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
113 | | eucrct2eupth1.s |
. . . 4
⊢
(Vtx‘𝑆) =
𝑉 |
114 | | elfzolt3 13408 |
. . . . . . 7
⊢ (𝐽 ∈ (0..^𝑁) → 0 < 𝑁) |
115 | 9, 114 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 < 𝑁) |
116 | | elfzoelz 13398 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) |
117 | 9, 116 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℤ) |
118 | 117 | peano2zd 12440 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 + 1) ∈ ℤ) |
119 | 5, 118 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) |
120 | | cshwlen 14523 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) →
(♯‘(𝐹 cyclShift
𝐾)) = (♯‘𝐹)) |
121 | 120 | eqcomd 2746 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾))) |
122 | 24, 119, 121 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾))) |
123 | 18, 122 | eqtrd 2780 |
. . . . . 6
⊢ (𝜑 → 𝑁 = (♯‘(𝐹 cyclShift 𝐾))) |
124 | 115, 123 | breqtrd 5105 |
. . . . 5
⊢ (𝜑 → 0 <
(♯‘(𝐹 cyclShift
𝐾))) |
125 | 124 | adantl 482 |
. . . 4
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾))) |
126 | 123 | adantl 482 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾))) |
127 | 126 | oveq1d 7287 |
. . . 4
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1)) |
128 | | eucrct2eupth.e |
. . . . . 6
⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽})))) |
129 | 128 | adantl 482 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽})))) |
130 | 24, 18, 9 | 3jca 1127 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁))) |
131 | 130 | adantl 482 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁))) |
132 | | cshimadifsn0 14554 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1)))) |
133 | 131, 132 | syl 17 |
. . . . . . 7
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1)))) |
134 | 7 | imaeq1i 5965 |
. . . . . . 7
⊢ ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))) |
135 | 133, 134 | eqtrdi 2796 |
. . . . . 6
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))) |
136 | 135 | reseq2d 5890 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))) |
137 | 129, 136 | eqtrd 2780 |
. . . 4
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))) |
138 | | eqid 2740 |
. . . 4
⊢ ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)) = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)) |
139 | | eqid 2740 |
. . . 4
⊢ ((𝑥 ∈
(0...(♯‘𝐹))
↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) |
140 | 1, 2, 110, 112, 113, 125, 127, 137, 138, 139 | eucrct2eupth1 28617 |
. . 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 13417 |
. . . . . . . 8
⊢
(0..^𝑁) ⊆
(0...𝑁) |
145 | 18 | oveq2d 7288 |
. . . . . . . 8
⊢ (𝜑 → (0...𝑁) = (0...(♯‘𝐹))) |
146 | 144, 145 | sseqtrid 3978 |
. . . . . . 7
⊢ (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹))) |
147 | 146 | resmptd 5947 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
148 | | elfzoel2 13397 |
. . . . . . . 8
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ) |
149 | | fzoval 13399 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(0..^𝑁) = (0...(𝑁 − 1))) |
150 | 9, 148, 149 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (0..^𝑁) = (0...(𝑁 − 1))) |
151 | 150 | reseq2d 5890 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))) |
152 | 147, 151 | eqtr3d 2782 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))) |
153 | 143, 152 | eqtrid 2792 |
. . . 4
⊢ (𝜑 → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))) |
154 | 153 | adantl 482 |
. . 3
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))) |
155 | 140, 142,
154 | 3brtr4d 5111 |
. 2
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄) |
156 | 20 | adantl 482 |
. . . 4
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃) |
157 | | peano2nn0 12284 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ ℕ0
→ (𝐽 + 1) ∈
ℕ0) |
158 | 157 | 3ad2ant1 1132 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈
ℕ0) |
159 | 158 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈
ℕ0) |
160 | | simpl2 1191 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ) |
161 | | 1cnd 10981 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 1 ∈
ℂ) |
162 | | nn0cn 12254 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 ∈ ℕ0
→ 𝐽 ∈
ℂ) |
163 | 162 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ) |
164 | 12, 161, 163 | subadd2d 11362 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁)) |
165 | | eqcom 2747 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽) |
166 | | eqcom 2747 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁) |
167 | 164, 165,
166 | 3bitr4g 314 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1))) |
168 | 167 | necon3bbid 2983 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1))) |
169 | 157 | nn0red 12305 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ ℕ0
→ (𝐽 + 1) ∈
ℝ) |
170 | 169 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ) |
171 | | nnre 11991 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
172 | 171 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ) |
173 | | nn0z 12354 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 ∈ ℕ0
→ 𝐽 ∈
ℤ) |
174 | | nnz 12353 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
175 | | zltp1le 12381 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁)) |
176 | 173, 174,
175 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁)) |
177 | 176 | biimp3a 1468 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁) |
178 | 170, 172,
177 | leltned 11139 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁 ↔ 𝑁 ≠ (𝐽 + 1))) |
179 | 178 | biimprd 247 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁)) |
180 | 168, 179 | sylbid 239 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁)) |
181 | 180 | imp 407 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁) |
182 | 159, 160,
181 | 3jca 1127 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)) |
183 | 182 | ex 413 |
. . . . . . . . 9
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))) |
184 | 10, 183 | sylbi 216 |
. . . . . . . 8
⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))) |
185 | | elfzo0 13439 |
. . . . . . . 8
⊢ ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)) |
186 | 184, 185 | syl6ibr 251 |
. . . . . . 7
⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁))) |
187 | 9, 186 | syl 17 |
. . . . . 6
⊢ (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁))) |
188 | 187 | impcom 408 |
. . . . 5
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁)) |
189 | 5 | a1i 11 |
. . . . 5
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1)) |
190 | 18 | eqcomd 2746 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐹) = 𝑁) |
191 | 190 | oveq2d 7288 |
. . . . . 6
⊢ (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁)) |
192 | 191 | adantl 482 |
. . . . 5
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁)) |
193 | 188, 189,
192 | 3eltr4d 2856 |
. . . 4
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹))) |
194 | | eqid 2740 |
. . . 4
⊢ (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾) |
195 | | eqid 2740 |
. . . 4
⊢ (𝑥 ∈
(0...(♯‘𝐹))
↦ if(𝑥 ≤
((♯‘𝐹) −
𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) |
196 | 3 | adantl 482 |
. . . 4
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃) |
197 | 1, 2, 156, 31, 193, 194, 195, 196 | eucrctshift 28616 |
. . 3
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) |
198 | | simprl 768 |
. . . . 5
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))) |
199 | | simprr 770 |
. . . . 5
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))) |
200 | 124 | ad2antlr 724 |
. . . . 5
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾))) |
201 | 123 | oveq1d 7287 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1)) |
202 | 201 | ad2antlr 724 |
. . . . 5
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1)) |
203 | 128 | adantl 482 |
. . . . . . 7
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽})))) |
204 | 130 | adantl 482 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁))) |
205 | 204, 132 | syl 17 |
. . . . . . . . 9
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1)))) |
206 | 205, 134 | eqtrdi 2796 |
. . . . . . . 8
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))) |
207 | 206 | reseq2d 5890 |
. . . . . . 7
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))) |
208 | 203, 207 | eqtrd 2780 |
. . . . . 6
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))) |
209 | 208 | adantr 481 |
. . . . 5
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))) |
210 | | eqid 2740 |
. . . . 5
⊢ ((𝑥 ∈
(0...(♯‘𝐹))
↦ if(𝑥 ≤
((♯‘𝐹) −
𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) |
211 | 1, 2, 198, 199, 113, 200, 202, 209, 138, 210 | eucrct2eupth1 28617 |
. . . 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 7287 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁 − 𝐾)) |
214 | 213 | breq2d 5091 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾))) |
215 | 214 | adantl 482 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾))) |
216 | 190 | oveq2d 7288 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁)) |
217 | 216 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁))) |
218 | 217 | adantl 482 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁))) |
219 | 215, 218 | ifbieq2d 4491 |
. . . . . . . . 9
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) |
220 | 219 | mpteq2dv 5181 |
. . . . . . . 8
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
221 | 150 | eqcomd 2746 |
. . . . . . . . 9
⊢ (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁)) |
222 | 221 | adantl 482 |
. . . . . . . 8
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁)) |
223 | 220, 222 | reseq12d 5891 |
. . . . . . 7
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁))) |
224 | 18 | adantl 482 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹)) |
225 | 224 | oveq2d 7288 |
. . . . . . . . 9
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹))) |
226 | 144, 225 | sseqtrid 3978 |
. . . . . . . 8
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹))) |
227 | 226 | resmptd 5947 |
. . . . . . 7
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
228 | 223, 227 | eqtrd 2780 |
. . . . . 6
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
229 | 143, 228 | eqtr4id 2799 |
. . . . 5
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))) |
230 | 229 | adantr 481 |
. . . 4
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))) |
231 | 211, 212,
230 | 3brtr4d 5111 |
. . 3
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄) |
232 | 197, 231 | mpdan 684 |
. 2
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄) |
233 | 155, 232 | pm2.61ian 809 |
1
⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄) |