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 481 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃) |
| 5 | | eucrct2eupth.k |
. . . . . . . 8
⊢ 𝐾 = (𝐽 + 1) |
| 6 | 5 | eqcomi 2746 |
. . . . . . 7
⊢ (𝐽 + 1) = 𝐾 |
| 7 | 6 | oveq2i 7442 |
. . . . . 6
⊢ (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾) |
| 8 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1)) |
| 9 | | eucrct2eupth.j |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) |
| 10 | | elfzo0 13740 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) |
| 11 | | nncn 12274 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 12 | 11 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ) |
| 13 | 10, 12 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ) |
| 14 | | npcan1 11688 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
| 15 | 9, 13, 14 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
| 16 | 8, 15 | sylan9eq 2797 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁) |
| 17 | 16 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁)) |
| 18 | | eucrct2eupth.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 = (♯‘𝐹)) |
| 19 | 18 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹))) |
| 20 | | eucrct2eupth1.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃) |
| 21 | | crctiswlk 29816 |
. . . . . . . . . . . 12
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
| 22 | 2 | wlkf 29632 |
. . . . . . . . . . . 12
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
| 24 | 20, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
| 25 | | cshwn 14835 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹) |
| 27 | 19, 26 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹) |
| 28 | 27 | adantl 481 |
. . . . . . 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 29837 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐹) ∈
ℕ0) |
| 33 | | fz0sn0fz1 13685 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹)
∈ ℕ0 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹)))) |
| 34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0...(♯‘𝐹)) = ({0} ∪
(1...(♯‘𝐹)))) |
| 35 | 34 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))))) |
| 36 | | elun 4153 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ({0} ∪
(1...(♯‘𝐹)))
↔ (𝑥 ∈ {0} ∨
𝑥 ∈
(1...(♯‘𝐹)))) |
| 37 | 35, 36 | bitrdi 287 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))) |
| 38 | | elsni 4643 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {0} → 𝑥 = 0) |
| 39 | | 0le0 12367 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
0 |
| 40 | 38, 39 | eqbrtrdi 5182 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {0} → 𝑥 ≤ 0) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → 𝑥 ≤ 0) |
| 42 | 41 | iftrued 4533 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁))) |
| 43 | 18 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘(♯‘𝐹))) |
| 44 | | crctprop 29812 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) |
| 45 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑁) = (𝑃‘0)) |
| 50 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁)) |
| 51 | 9, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 52 | 51 | addlidd 11462 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0 + 𝑁) = 𝑁) |
| 53 | 50, 52 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑥 + 𝑁) = 𝑁) |
| 54 | 53 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑁)) |
| 55 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → (𝑃‘𝑥) = (𝑃‘0)) |
| 56 | 55 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑥) = (𝑃‘0)) |
| 57 | 49, 54, 56 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥)) |
| 58 | 38, 57 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥)) |
| 59 | 42, 58 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)) |
| 60 | 59 | ex 412 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))) |
| 61 | | elfznn 13593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
(1...(♯‘𝐹))
→ 𝑥 ∈
ℕ) |
| 62 | | nnnle0 12299 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ → ¬
𝑥 ≤ 0) |
| 63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
(1...(♯‘𝐹))
→ ¬ 𝑥 ≤
0) |
| 64 | 63 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0) |
| 65 | 64 | iffalsed 4536 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁))) |
| 66 | 61 | nncnd 12282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
(1...(♯‘𝐹))
→ 𝑥 ∈
ℂ) |
| 67 | 66 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ) |
| 68 | 51 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ) |
| 69 | 67, 68 | pncand 11621 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥) |
| 70 | 69 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃‘𝑥)) |
| 71 | 65, 70 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)) |
| 72 | 71 | ex 412 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))) |
| 73 | 60, 72 | jaod 860 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))) |
| 74 | 37, 73 | sylbid 240 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))) |
| 75 | 74 | imp 406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)) |
| 76 | 75 | mpteq2dva 5242 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥))) |
| 77 | 76 | adantl 481 |
. . . . . 6
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥))) |
| 78 | 5 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (𝑁 − 𝐾) = (𝑁 − (𝐽 + 1)) |
| 79 | 8 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1))) |
| 80 | 15 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁 − 𝑁)) |
| 81 | 51 | subidd 11608 |
. . . . . . . . . . . 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 5155 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁 − 𝐾) ↔ 𝑥 ≤ 0)) |
| 86 | 5 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1)) |
| 87 | 86 | fveq2i 6909 |
. . . . . . . . 9
⊢ (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1))) |
| 88 | 8 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1))) |
| 89 | 15 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁)) |
| 90 | 88, 89 | sylan9eq 2797 |
. . . . . . . . . 10
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁)) |
| 91 | 90 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁))) |
| 92 | 87, 91 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁))) |
| 93 | 86 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁) |
| 94 | 93 | fveq2i 6909 |
. . . . . . . . 9
⊢ (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) |
| 95 | 88 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁)) |
| 96 | 89 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁)) |
| 97 | 95, 96 | sylan9eq 2797 |
. . . . . . . . . 10
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁)) |
| 98 | 97 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁))) |
| 99 | 94, 98 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁))) |
| 100 | 85, 92, 99 | ifbieq12d 4554 |
. . . . . . 7
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) |
| 101 | 100 | mpteq2dv 5244 |
. . . . . 6
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))) |
| 102 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) |
| 103 | 1 | wlkp 29634 |
. . . . . . . . 9
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 104 | | ffn 6736 |
. . . . . . . . 9
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...(♯‘𝐹))) |
| 105 | 102, 103,
104 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 Fn (0...(♯‘𝐹))) |
| 106 | 105 | adantl 481 |
. . . . . . 7
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹))) |
| 107 | | dffn5 6967 |
. . . . . . 7
⊢ (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥))) |
| 108 | 106, 107 | sylib 218 |
. . . . . 6
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥))) |
| 109 | 77, 101, 108 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃) |
| 110 | 4, 30, 109 | 3brtr4d 5175 |
. . . 4
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
| 111 | 20 | adantl 481 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃) |
| 112 | 111, 30, 109 | 3brtr4d 5175 |
. . . 4
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
| 113 | | eucrct2eupth1.s |
. . . 4
⊢
(Vtx‘𝑆) =
𝑉 |
| 114 | | elfzolt3 13709 |
. . . . . . 7
⊢ (𝐽 ∈ (0..^𝑁) → 0 < 𝑁) |
| 115 | 9, 114 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 < 𝑁) |
| 116 | | elfzoelz 13699 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) |
| 117 | 9, 116 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℤ) |
| 118 | 117 | peano2zd 12725 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 + 1) ∈ ℤ) |
| 119 | 5, 118 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 120 | | cshwlen 14837 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) →
(♯‘(𝐹 cyclShift
𝐾)) = (♯‘𝐹)) |
| 121 | 120 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾))) |
| 122 | 24, 119, 121 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾))) |
| 123 | 18, 122 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → 𝑁 = (♯‘(𝐹 cyclShift 𝐾))) |
| 124 | 115, 123 | breqtrd 5169 |
. . . . 5
⊢ (𝜑 → 0 <
(♯‘(𝐹 cyclShift
𝐾))) |
| 125 | 124 | adantl 481 |
. . . 4
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾))) |
| 126 | 123 | adantl 481 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾))) |
| 127 | 126 | oveq1d 7446 |
. . . 4
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1)) |
| 128 | | eucrct2eupth.e |
. . . . . 6
⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽})))) |
| 129 | 128 | adantl 481 |
. . . . 5
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽})))) |
| 130 | 24, 18, 9 | 3jca 1129 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁))) |
| 131 | 130 | adantl 481 |
. . . . . . . 8
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁))) |
| 132 | | cshimadifsn0 14869 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1)))) |
| 133 | 131, 132 | syl 17 |
. . . . . . 7
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1)))) |
| 134 | 7 | imaeq1i 6075 |
. . . . . . 7
⊢ ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))) |
| 135 | 133, 134 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))) |
| 136 | 135 | reseq2d 5997 |
. . . . 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 30263 |
. . 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 13718 |
. . . . . . . 8
⊢
(0..^𝑁) ⊆
(0...𝑁) |
| 145 | 18 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (0...𝑁) = (0...(♯‘𝐹))) |
| 146 | 144, 145 | sseqtrid 4026 |
. . . . . . 7
⊢ (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹))) |
| 147 | 146 | resmptd 6058 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
| 148 | | elfzoel2 13698 |
. . . . . . . 8
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ) |
| 149 | | fzoval 13700 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(0..^𝑁) = (0...(𝑁 − 1))) |
| 150 | 9, 148, 149 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (0..^𝑁) = (0...(𝑁 − 1))) |
| 151 | 150 | reseq2d 5997 |
. . . . . 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 481 |
. . 3
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))) |
| 155 | 140, 142,
154 | 3brtr4d 5175 |
. 2
⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄) |
| 156 | 20 | adantl 481 |
. . . 4
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃) |
| 157 | | peano2nn0 12566 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ ℕ0
→ (𝐽 + 1) ∈
ℕ0) |
| 158 | 157 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈
ℕ0) |
| 159 | 158 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈
ℕ0) |
| 160 | | simpl2 1193 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ) |
| 161 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 1 ∈
ℂ) |
| 162 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 ∈ ℕ0
→ 𝐽 ∈
ℂ) |
| 163 | 162 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ) |
| 164 | 12, 161, 163 | subadd2d 11639 |
. . . . . . . . . . . . . . 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 2978 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1))) |
| 169 | 157 | nn0red 12588 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ ℕ0
→ (𝐽 + 1) ∈
ℝ) |
| 170 | 169 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ) |
| 171 | | nnre 12273 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 172 | 171 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ) |
| 173 | | nn0z 12638 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 ∈ ℕ0
→ 𝐽 ∈
ℤ) |
| 174 | | nnz 12634 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 175 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁)) |
| 176 | 173, 174,
175 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁)) |
| 177 | 176 | biimp3a 1471 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁) |
| 178 | 170, 172,
177 | leltned 11414 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁 ↔ 𝑁 ≠ (𝐽 + 1))) |
| 179 | 178 | biimprd 248 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁)) |
| 180 | 168, 179 | sylbid 240 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁)) |
| 181 | 180 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁) |
| 182 | 159, 160,
181 | 3jca 1129 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)) |
| 183 | 182 | ex 412 |
. . . . . . . . 9
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))) |
| 184 | 10, 183 | sylbi 217 |
. . . . . . . 8
⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))) |
| 185 | | elfzo0 13740 |
. . . . . . . 8
⊢ ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)) |
| 186 | 184, 185 | imbitrrdi 252 |
. . . . . . 7
⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁))) |
| 187 | 9, 186 | syl 17 |
. . . . . 6
⊢ (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁))) |
| 188 | 187 | impcom 407 |
. . . . 5
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁)) |
| 189 | 5 | a1i 11 |
. . . . 5
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1)) |
| 190 | 18 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐹) = 𝑁) |
| 191 | 190 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁)) |
| 192 | 191 | adantl 481 |
. . . . 5
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁)) |
| 193 | 188, 189,
192 | 3eltr4d 2856 |
. . . 4
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹))) |
| 194 | | eqid 2737 |
. . . 4
⊢ (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾) |
| 195 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈
(0...(♯‘𝐹))
↦ if(𝑥 ≤
((♯‘𝐹) −
𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) |
| 196 | 3 | adantl 481 |
. . . 4
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃) |
| 197 | 1, 2, 156, 31, 193, 194, 195, 196 | eucrctshift 30262 |
. . 3
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) |
| 198 | | simprl 771 |
. . . . 5
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))) |
| 199 | | simprr 773 |
. . . . 5
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))) |
| 200 | 124 | ad2antlr 727 |
. . . . 5
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾))) |
| 201 | 123 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1)) |
| 202 | 201 | ad2antlr 727 |
. . . . 5
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1)) |
| 203 | 128 | adantl 481 |
. . . . . . 7
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽})))) |
| 204 | 130 | adantl 481 |
. . . . . . . . . 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 5997 |
. . . . . . 7
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))) |
| 208 | 203, 207 | eqtrd 2777 |
. . . . . 6
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))) |
| 209 | 208 | adantr 480 |
. . . . 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 30263 |
. . . 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 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁 − 𝐾)) |
| 214 | 213 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾))) |
| 215 | 214 | adantl 481 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾))) |
| 216 | 190 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁)) |
| 217 | 216 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁))) |
| 218 | 217 | adantl 481 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁))) |
| 219 | 215, 218 | ifbieq2d 4552 |
. . . . . . . . 9
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) |
| 220 | 219 | mpteq2dv 5244 |
. . . . . . . 8
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))) |
| 221 | 150 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁)) |
| 222 | 221 | adantl 481 |
. . . . . . . 8
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁)) |
| 223 | 220, 222 | reseq12d 5998 |
. . . . . . 7
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁))) |
| 224 | 18 | adantl 481 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹)) |
| 225 | 224 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹))) |
| 226 | 144, 225 | sseqtrid 4026 |
. . . . . . . 8
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹))) |
| 227 | 226 | resmptd 6058 |
. . . . . . 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 480 |
. . . 4
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))) |
| 231 | 211, 212,
230 | 3brtr4d 5175 |
. . 3
⊢ (((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄) |
| 232 | 197, 231 | mpdan 687 |
. 2
⊢ ((¬
𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄) |
| 233 | 155, 232 | pm2.61ian 812 |
1
⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄) |