# Metamath Proof Explorer

## Theorem eucrct2eupth

Description: Removing one edge ( I( FJ ) ) from a graph G with an Eulerian circuit <. F , P >. results in a graph S with an Eulerian path <. H , Q >. . (Contributed by AV, 17-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses eucrct2eupth1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
eucrct2eupth1.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
eucrct2eupth1.d ${⊢}{\phi }\to {F}\mathrm{EulerPaths}\left({G}\right){P}$
eucrct2eupth1.c ${⊢}{\phi }\to {F}\mathrm{Circuits}\left({G}\right){P}$
eucrct2eupth1.s ${⊢}\mathrm{Vtx}\left({S}\right)={V}$
eucrct2eupth.n ${⊢}{\phi }\to {N}=\left|{F}\right|$
eucrct2eupth.j ${⊢}{\phi }\to {J}\in \left(0..^{N}\right)$
eucrct2eupth.e ${⊢}{\phi }\to \mathrm{iEdg}\left({S}\right)={{I}↾}_{{F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]}$
eucrct2eupth.k ${⊢}{K}={J}+1$
eucrct2eupth.h ${⊢}{H}=\left({F}\mathrm{cyclShift}{K}\right)\mathrm{prefix}\left({N}-1\right)$
eucrct2eupth.q ${⊢}{Q}=\left({x}\in \left(0..^{N}\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)$
Assertion eucrct2eupth ${⊢}{\phi }\to {H}\mathrm{EulerPaths}\left({S}\right){Q}$

### Proof

Step Hyp Ref Expression
1 eucrct2eupth1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 eucrct2eupth1.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 eucrct2eupth1.d ${⊢}{\phi }\to {F}\mathrm{EulerPaths}\left({G}\right){P}$
4 eucrct2eupth1.c ${⊢}{\phi }\to {F}\mathrm{Circuits}\left({G}\right){P}$
5 eucrct2eupth1.s ${⊢}\mathrm{Vtx}\left({S}\right)={V}$
6 eucrct2eupth.n ${⊢}{\phi }\to {N}=\left|{F}\right|$
7 eucrct2eupth.j ${⊢}{\phi }\to {J}\in \left(0..^{N}\right)$
8 eucrct2eupth.e ${⊢}{\phi }\to \mathrm{iEdg}\left({S}\right)={{I}↾}_{{F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]}$
9 eucrct2eupth.k ${⊢}{K}={J}+1$
10 eucrct2eupth.h ${⊢}{H}=\left({F}\mathrm{cyclShift}{K}\right)\mathrm{prefix}\left({N}-1\right)$
11 eucrct2eupth.q ${⊢}{Q}=\left({x}\in \left(0..^{N}\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)$
12 3 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {F}\mathrm{EulerPaths}\left({G}\right){P}$
13 9 eqcomi ${⊢}{J}+1={K}$
14 13 oveq2i ${⊢}{F}\mathrm{cyclShift}\left({J}+1\right)={F}\mathrm{cyclShift}{K}$
15 oveq1 ${⊢}{J}={N}-1\to {J}+1={N}-1+1$
16 elfzo0 ${⊢}{J}\in \left(0..^{N}\right)↔\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)$
17 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
18 17 3ad2ant2 ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to {N}\in ℂ$
19 16 18 sylbi ${⊢}{J}\in \left(0..^{N}\right)\to {N}\in ℂ$
20 npcan1 ${⊢}{N}\in ℂ\to {N}-1+1={N}$
21 7 19 20 3syl ${⊢}{\phi }\to {N}-1+1={N}$
22 15 21 sylan9eq ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {J}+1={N}$
23 22 oveq2d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {F}\mathrm{cyclShift}\left({J}+1\right)={F}\mathrm{cyclShift}{N}$
24 6 oveq2d ${⊢}{\phi }\to {F}\mathrm{cyclShift}{N}={F}\mathrm{cyclShift}\left|{F}\right|$
25 crctiswlk ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to {F}\mathrm{Walks}\left({G}\right){P}$
26 2 wlkf ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to {F}\in \mathrm{Word}\mathrm{dom}{I}$
27 25 26 syl ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to {F}\in \mathrm{Word}\mathrm{dom}{I}$
28 4 27 syl ${⊢}{\phi }\to {F}\in \mathrm{Word}\mathrm{dom}{I}$
29 cshwn ${⊢}{F}\in \mathrm{Word}\mathrm{dom}{I}\to {F}\mathrm{cyclShift}\left|{F}\right|={F}$
30 28 29 syl ${⊢}{\phi }\to {F}\mathrm{cyclShift}\left|{F}\right|={F}$
31 24 30 eqtrd ${⊢}{\phi }\to {F}\mathrm{cyclShift}{N}={F}$
32 31 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {F}\mathrm{cyclShift}{N}={F}$
33 23 32 eqtrd ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {F}\mathrm{cyclShift}\left({J}+1\right)={F}$
34 14 33 syl5eqr ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {F}\mathrm{cyclShift}{K}={F}$
35 eqid ${⊢}\left|{F}\right|=\left|{F}\right|$
36 1 2 4 35 crctcshlem1 ${⊢}{\phi }\to \left|{F}\right|\in {ℕ}_{0}$
37 fz0sn0fz1 ${⊢}\left|{F}\right|\in {ℕ}_{0}\to \left(0\dots \left|{F}\right|\right)=\left\{0\right\}\cup \left(1\dots \left|{F}\right|\right)$
38 36 37 syl ${⊢}{\phi }\to \left(0\dots \left|{F}\right|\right)=\left\{0\right\}\cup \left(1\dots \left|{F}\right|\right)$
39 38 eleq2d ${⊢}{\phi }\to \left({x}\in \left(0\dots \left|{F}\right|\right)↔{x}\in \left(\left\{0\right\}\cup \left(1\dots \left|{F}\right|\right)\right)\right)$
40 elun ${⊢}{x}\in \left(\left\{0\right\}\cup \left(1\dots \left|{F}\right|\right)\right)↔\left({x}\in \left\{0\right\}\vee {x}\in \left(1\dots \left|{F}\right|\right)\right)$
41 39 40 syl6bb ${⊢}{\phi }\to \left({x}\in \left(0\dots \left|{F}\right|\right)↔\left({x}\in \left\{0\right\}\vee {x}\in \left(1\dots \left|{F}\right|\right)\right)\right)$
42 elsni ${⊢}{x}\in \left\{0\right\}\to {x}=0$
43 0le0 ${⊢}0\le 0$
44 42 43 eqbrtrdi ${⊢}{x}\in \left\{0\right\}\to {x}\le 0$
45 44 adantl ${⊢}\left({\phi }\wedge {x}\in \left\{0\right\}\right)\to {x}\le 0$
46 45 iftrued ${⊢}\left({\phi }\wedge {x}\in \left\{0\right\}\right)\to if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)={P}\left({x}+{N}\right)$
47 6 fveq2d ${⊢}{\phi }\to {P}\left({N}\right)={P}\left(\left|{F}\right|\right)$
48 crctprop ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to \left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
49 simpr ${⊢}\left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to {P}\left(0\right)={P}\left(\left|{F}\right|\right)$
50 49 eqcomd ${⊢}\left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to {P}\left(\left|{F}\right|\right)={P}\left(0\right)$
51 4 48 50 3syl ${⊢}{\phi }\to {P}\left(\left|{F}\right|\right)={P}\left(0\right)$
52 47 51 eqtrd ${⊢}{\phi }\to {P}\left({N}\right)={P}\left(0\right)$
53 52 adantr ${⊢}\left({\phi }\wedge {x}=0\right)\to {P}\left({N}\right)={P}\left(0\right)$
54 oveq1 ${⊢}{x}=0\to {x}+{N}=0+{N}$
55 7 19 syl ${⊢}{\phi }\to {N}\in ℂ$
56 55 addid2d ${⊢}{\phi }\to 0+{N}={N}$
57 54 56 sylan9eqr ${⊢}\left({\phi }\wedge {x}=0\right)\to {x}+{N}={N}$
58 57 fveq2d ${⊢}\left({\phi }\wedge {x}=0\right)\to {P}\left({x}+{N}\right)={P}\left({N}\right)$
59 fveq2 ${⊢}{x}=0\to {P}\left({x}\right)={P}\left(0\right)$
60 59 adantl ${⊢}\left({\phi }\wedge {x}=0\right)\to {P}\left({x}\right)={P}\left(0\right)$
61 53 58 60 3eqtr4d ${⊢}\left({\phi }\wedge {x}=0\right)\to {P}\left({x}+{N}\right)={P}\left({x}\right)$
62 42 61 sylan2 ${⊢}\left({\phi }\wedge {x}\in \left\{0\right\}\right)\to {P}\left({x}+{N}\right)={P}\left({x}\right)$
63 46 62 eqtrd ${⊢}\left({\phi }\wedge {x}\in \left\{0\right\}\right)\to if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)={P}\left({x}\right)$
64 63 ex ${⊢}{\phi }\to \left({x}\in \left\{0\right\}\to if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)={P}\left({x}\right)\right)$
65 elfznn ${⊢}{x}\in \left(1\dots \left|{F}\right|\right)\to {x}\in ℕ$
66 nnnle0 ${⊢}{x}\in ℕ\to ¬{x}\le 0$
67 65 66 syl ${⊢}{x}\in \left(1\dots \left|{F}\right|\right)\to ¬{x}\le 0$
68 67 adantl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{F}\right|\right)\right)\to ¬{x}\le 0$
69 68 iffalsed ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{F}\right|\right)\right)\to if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)={P}\left({x}+{N}-{N}\right)$
70 65 nncnd ${⊢}{x}\in \left(1\dots \left|{F}\right|\right)\to {x}\in ℂ$
71 70 adantl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{F}\right|\right)\right)\to {x}\in ℂ$
72 55 adantr ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{F}\right|\right)\right)\to {N}\in ℂ$
73 71 72 pncand ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{F}\right|\right)\right)\to {x}+{N}-{N}={x}$
74 73 fveq2d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{F}\right|\right)\right)\to {P}\left({x}+{N}-{N}\right)={P}\left({x}\right)$
75 69 74 eqtrd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{F}\right|\right)\right)\to if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)={P}\left({x}\right)$
76 75 ex ${⊢}{\phi }\to \left({x}\in \left(1\dots \left|{F}\right|\right)\to if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)={P}\left({x}\right)\right)$
77 64 76 jaod ${⊢}{\phi }\to \left(\left({x}\in \left\{0\right\}\vee {x}\in \left(1\dots \left|{F}\right|\right)\right)\to if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)={P}\left({x}\right)\right)$
78 41 77 sylbid ${⊢}{\phi }\to \left({x}\in \left(0\dots \left|{F}\right|\right)\to if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)={P}\left({x}\right)\right)$
79 78 imp ${⊢}\left({\phi }\wedge {x}\in \left(0\dots \left|{F}\right|\right)\right)\to if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)={P}\left({x}\right)$
80 79 mpteq2dva ${⊢}{\phi }\to \left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)\right)=\left({x}\in \left(0\dots \left|{F}\right|\right)⟼{P}\left({x}\right)\right)$
81 80 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)\right)=\left({x}\in \left(0\dots \left|{F}\right|\right)⟼{P}\left({x}\right)\right)$
82 9 oveq2i ${⊢}{N}-{K}={N}-\left({J}+1\right)$
83 15 oveq2d ${⊢}{J}={N}-1\to {N}-\left({J}+1\right)={N}-\left({N}-1+1\right)$
84 21 oveq2d ${⊢}{\phi }\to {N}-\left({N}-1+1\right)={N}-{N}$
85 55 subidd ${⊢}{\phi }\to {N}-{N}=0$
86 84 85 eqtrd ${⊢}{\phi }\to {N}-\left({N}-1+1\right)=0$
87 83 86 sylan9eq ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {N}-\left({J}+1\right)=0$
88 82 87 syl5eq ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {N}-{K}=0$
89 88 breq2d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \left({x}\le {N}-{K}↔{x}\le 0\right)$
90 9 oveq2i ${⊢}{x}+{K}={x}+{J}+1$
91 90 fveq2i ${⊢}{P}\left({x}+{K}\right)={P}\left({x}+{J}+1\right)$
92 15 oveq2d ${⊢}{J}={N}-1\to {x}+{J}+1={x}+\left({N}-1\right)+1$
93 21 oveq2d ${⊢}{\phi }\to {x}+\left({N}-1\right)+1={x}+{N}$
94 92 93 sylan9eq ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {x}+{J}+1={x}+{N}$
95 94 fveq2d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {P}\left({x}+{J}+1\right)={P}\left({x}+{N}\right)$
96 91 95 syl5eq ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {P}\left({x}+{K}\right)={P}\left({x}+{N}\right)$
97 90 oveq1i ${⊢}{x}+{K}-{N}={x}+\left({J}+1\right)-{N}$
98 97 fveq2i ${⊢}{P}\left({x}+{K}-{N}\right)={P}\left({x}+\left({J}+1\right)-{N}\right)$
99 92 oveq1d ${⊢}{J}={N}-1\to {x}+\left({J}+1\right)-{N}={x}+\left({N}-1+1\right)-{N}$
100 93 oveq1d ${⊢}{\phi }\to {x}+\left({N}-1+1\right)-{N}={x}+{N}-{N}$
101 99 100 sylan9eq ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {x}+\left({J}+1\right)-{N}={x}+{N}-{N}$
102 101 fveq2d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {P}\left({x}+\left({J}+1\right)-{N}\right)={P}\left({x}+{N}-{N}\right)$
103 98 102 syl5eq ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {P}\left({x}+{K}-{N}\right)={P}\left({x}+{N}-{N}\right)$
104 89 96 103 ifbieq12d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)=if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)$
105 104 mpteq2dv ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)=\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le 0,{P}\left({x}+{N}\right),{P}\left({x}+{N}-{N}\right)\right)\right)$
106 4 25 syl ${⊢}{\phi }\to {F}\mathrm{Walks}\left({G}\right){P}$
107 1 wlkp ${⊢}{F}\mathrm{Walks}\left({G}\right){P}\to {P}:\left(0\dots \left|{F}\right|\right)⟶{V}$
108 ffn ${⊢}{P}:\left(0\dots \left|{F}\right|\right)⟶{V}\to {P}Fn\left(0\dots \left|{F}\right|\right)$
109 106 107 108 3syl ${⊢}{\phi }\to {P}Fn\left(0\dots \left|{F}\right|\right)$
110 109 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {P}Fn\left(0\dots \left|{F}\right|\right)$
111 dffn5 ${⊢}{P}Fn\left(0\dots \left|{F}\right|\right)↔{P}=\left({x}\in \left(0\dots \left|{F}\right|\right)⟼{P}\left({x}\right)\right)$
112 110 111 sylib ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {P}=\left({x}\in \left(0\dots \left|{F}\right|\right)⟼{P}\left({x}\right)\right)$
113 81 105 112 3eqtr4d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)={P}$
114 12 34 113 3brtr4d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)$
115 4 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {F}\mathrm{Circuits}\left({G}\right){P}$
116 115 34 113 3brtr4d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)$
117 elfzolt3 ${⊢}{J}\in \left(0..^{N}\right)\to 0<{N}$
118 7 117 syl ${⊢}{\phi }\to 0<{N}$
119 elfzoelz ${⊢}{J}\in \left(0..^{N}\right)\to {J}\in ℤ$
120 7 119 syl ${⊢}{\phi }\to {J}\in ℤ$
121 120 peano2zd ${⊢}{\phi }\to {J}+1\in ℤ$
122 9 121 eqeltrid ${⊢}{\phi }\to {K}\in ℤ$
123 cshwlen ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge {K}\in ℤ\right)\to \left|{F}\mathrm{cyclShift}{K}\right|=\left|{F}\right|$
124 123 eqcomd ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge {K}\in ℤ\right)\to \left|{F}\right|=\left|{F}\mathrm{cyclShift}{K}\right|$
125 28 122 124 syl2anc ${⊢}{\phi }\to \left|{F}\right|=\left|{F}\mathrm{cyclShift}{K}\right|$
126 6 125 eqtrd ${⊢}{\phi }\to {N}=\left|{F}\mathrm{cyclShift}{K}\right|$
127 118 126 breqtrd ${⊢}{\phi }\to 0<\left|{F}\mathrm{cyclShift}{K}\right|$
128 127 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to 0<\left|{F}\mathrm{cyclShift}{K}\right|$
129 126 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {N}=\left|{F}\mathrm{cyclShift}{K}\right|$
130 129 oveq1d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {N}-1=\left|{F}\mathrm{cyclShift}{K}\right|-1$
131 8 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \mathrm{iEdg}\left({S}\right)={{I}↾}_{{F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]}$
132 28 6 7 3jca ${⊢}{\phi }\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge {N}=\left|{F}\right|\wedge {J}\in \left(0..^{N}\right)\right)$
133 132 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge {N}=\left|{F}\right|\wedge {J}\in \left(0..^{N}\right)\right)$
134 cshimadifsn0 ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge {N}=\left|{F}\right|\wedge {J}\in \left(0..^{N}\right)\right)\to {F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]=\left({F}\mathrm{cyclShift}\left({J}+1\right)\right)\left[\left(0..^{N}-1\right)\right]$
135 133 134 syl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]=\left({F}\mathrm{cyclShift}\left({J}+1\right)\right)\left[\left(0..^{N}-1\right)\right]$
136 14 imaeq1i ${⊢}\left({F}\mathrm{cyclShift}\left({J}+1\right)\right)\left[\left(0..^{N}-1\right)\right]=\left({F}\mathrm{cyclShift}{K}\right)\left[\left(0..^{N}-1\right)\right]$
137 135 136 syl6eq ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]=\left({F}\mathrm{cyclShift}{K}\right)\left[\left(0..^{N}-1\right)\right]$
138 137 reseq2d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {{I}↾}_{{F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]}={{I}↾}_{\left({F}\mathrm{cyclShift}{K}\right)\left[\left(0..^{N}-1\right)\right]}$
139 131 138 eqtrd ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \mathrm{iEdg}\left({S}\right)={{I}↾}_{\left({F}\mathrm{cyclShift}{K}\right)\left[\left(0..^{N}-1\right)\right]}$
140 eqid ${⊢}\left({F}\mathrm{cyclShift}{K}\right)\mathrm{prefix}\left({N}-1\right)=\left({F}\mathrm{cyclShift}{K}\right)\mathrm{prefix}\left({N}-1\right)$
141 eqid ${⊢}{\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}={\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}$
142 1 2 114 116 5 128 130 139 140 141 eucrct2eupth1 ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{prefix}\left({N}-1\right)\right)\mathrm{EulerPaths}\left({S}\right)\left({\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}\right)$
143 10 a1i ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {H}=\left({F}\mathrm{cyclShift}{K}\right)\mathrm{prefix}\left({N}-1\right)$
144 fzossfz ${⊢}\left(0..^{N}\right)\subseteq \left(0\dots {N}\right)$
145 6 oveq2d ${⊢}{\phi }\to \left(0\dots {N}\right)=\left(0\dots \left|{F}\right|\right)$
146 144 145 sseqtrid ${⊢}{\phi }\to \left(0..^{N}\right)\subseteq \left(0\dots \left|{F}\right|\right)$
147 146 resmptd ${⊢}{\phi }\to {\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0..^{N}\right)}=\left({x}\in \left(0..^{N}\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)$
148 elfzoel2 ${⊢}{J}\in \left(0..^{N}\right)\to {N}\in ℤ$
149 fzoval ${⊢}{N}\in ℤ\to \left(0..^{N}\right)=\left(0\dots {N}-1\right)$
150 7 148 149 3syl ${⊢}{\phi }\to \left(0..^{N}\right)=\left(0\dots {N}-1\right)$
151 150 reseq2d ${⊢}{\phi }\to {\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0..^{N}\right)}={\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}$
152 147 151 eqtr3d ${⊢}{\phi }\to \left({x}\in \left(0..^{N}\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)={\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}$
153 11 152 syl5eq ${⊢}{\phi }\to {Q}={\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}$
154 153 adantl ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {Q}={\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}$
155 142 143 154 3brtr4d ${⊢}\left({J}={N}-1\wedge {\phi }\right)\to {H}\mathrm{EulerPaths}\left({S}\right){Q}$
156 4 adantl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {F}\mathrm{Circuits}\left({G}\right){P}$
157 peano2nn0 ${⊢}{J}\in {ℕ}_{0}\to {J}+1\in {ℕ}_{0}$
158 157 3ad2ant1 ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to {J}+1\in {ℕ}_{0}$
159 158 adantr ${⊢}\left(\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\wedge ¬{J}={N}-1\right)\to {J}+1\in {ℕ}_{0}$
160 simpl2 ${⊢}\left(\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\wedge ¬{J}={N}-1\right)\to {N}\in ℕ$
161 1cnd ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to 1\in ℂ$
162 nn0cn ${⊢}{J}\in {ℕ}_{0}\to {J}\in ℂ$
163 162 3ad2ant1 ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to {J}\in ℂ$
164 18 161 163 subadd2d ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to \left({N}-1={J}↔{J}+1={N}\right)$
165 eqcom ${⊢}{J}={N}-1↔{N}-1={J}$
166 eqcom ${⊢}{N}={J}+1↔{J}+1={N}$
167 164 165 166 3bitr4g ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to \left({J}={N}-1↔{N}={J}+1\right)$
168 167 necon3bbid ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to \left(¬{J}={N}-1↔{N}\ne {J}+1\right)$
169 157 nn0red ${⊢}{J}\in {ℕ}_{0}\to {J}+1\in ℝ$
170 169 3ad2ant1 ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to {J}+1\in ℝ$
171 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
172 171 3ad2ant2 ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to {N}\in ℝ$
173 nn0z ${⊢}{J}\in {ℕ}_{0}\to {J}\in ℤ$
174 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
175 zltp1le ${⊢}\left({J}\in ℤ\wedge {N}\in ℤ\right)\to \left({J}<{N}↔{J}+1\le {N}\right)$
176 173 174 175 syl2an ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\right)\to \left({J}<{N}↔{J}+1\le {N}\right)$
177 176 biimp3a ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to {J}+1\le {N}$
178 170 172 177 leltned ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to \left({J}+1<{N}↔{N}\ne {J}+1\right)$
179 178 biimprd ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to \left({N}\ne {J}+1\to {J}+1<{N}\right)$
180 168 179 sylbid ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to \left(¬{J}={N}-1\to {J}+1<{N}\right)$
181 180 imp ${⊢}\left(\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\wedge ¬{J}={N}-1\right)\to {J}+1<{N}$
182 159 160 181 3jca ${⊢}\left(\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\wedge ¬{J}={N}-1\right)\to \left({J}+1\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}+1<{N}\right)$
183 182 ex ${⊢}\left({J}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}<{N}\right)\to \left(¬{J}={N}-1\to \left({J}+1\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}+1<{N}\right)\right)$
184 16 183 sylbi ${⊢}{J}\in \left(0..^{N}\right)\to \left(¬{J}={N}-1\to \left({J}+1\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}+1<{N}\right)\right)$
185 elfzo0 ${⊢}{J}+1\in \left(0..^{N}\right)↔\left({J}+1\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {J}+1<{N}\right)$
186 184 185 syl6ibr ${⊢}{J}\in \left(0..^{N}\right)\to \left(¬{J}={N}-1\to {J}+1\in \left(0..^{N}\right)\right)$
187 7 186 syl ${⊢}{\phi }\to \left(¬{J}={N}-1\to {J}+1\in \left(0..^{N}\right)\right)$
188 187 impcom ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {J}+1\in \left(0..^{N}\right)$
189 9 a1i ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {K}={J}+1$
190 6 eqcomd ${⊢}{\phi }\to \left|{F}\right|={N}$
191 190 oveq2d ${⊢}{\phi }\to \left(0..^\left|{F}\right|\right)=\left(0..^{N}\right)$
192 191 adantl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \left(0..^\left|{F}\right|\right)=\left(0..^{N}\right)$
193 188 189 192 3eltr4d ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {K}\in \left(0..^\left|{F}\right|\right)$
194 eqid ${⊢}{F}\mathrm{cyclShift}{K}={F}\mathrm{cyclShift}{K}$
195 eqid ${⊢}\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)=\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)$
196 3 adantl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {F}\mathrm{EulerPaths}\left({G}\right){P}$
197 1 2 156 35 193 194 195 196 eucrctshift ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)$
198 simprl ${⊢}\left(\left(¬{J}={N}-1\wedge {\phi }\right)\wedge \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)\right)\to \left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)$
199 simprr ${⊢}\left(\left(¬{J}={N}-1\wedge {\phi }\right)\wedge \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)\right)\to \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)$
200 127 ad2antlr ${⊢}\left(\left(¬{J}={N}-1\wedge {\phi }\right)\wedge \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)\right)\to 0<\left|{F}\mathrm{cyclShift}{K}\right|$
201 126 oveq1d ${⊢}{\phi }\to {N}-1=\left|{F}\mathrm{cyclShift}{K}\right|-1$
202 201 ad2antlr ${⊢}\left(\left(¬{J}={N}-1\wedge {\phi }\right)\wedge \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)\right)\to {N}-1=\left|{F}\mathrm{cyclShift}{K}\right|-1$
203 8 adantl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \mathrm{iEdg}\left({S}\right)={{I}↾}_{{F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]}$
204 132 adantl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge {N}=\left|{F}\right|\wedge {J}\in \left(0..^{N}\right)\right)$
205 204 134 syl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]=\left({F}\mathrm{cyclShift}\left({J}+1\right)\right)\left[\left(0..^{N}-1\right)\right]$
206 205 136 syl6eq ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]=\left({F}\mathrm{cyclShift}{K}\right)\left[\left(0..^{N}-1\right)\right]$
207 206 reseq2d ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {{I}↾}_{{F}\left[\left(0..^{N}\right)\setminus \left\{{J}\right\}\right]}={{I}↾}_{\left({F}\mathrm{cyclShift}{K}\right)\left[\left(0..^{N}-1\right)\right]}$
208 203 207 eqtrd ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \mathrm{iEdg}\left({S}\right)={{I}↾}_{\left({F}\mathrm{cyclShift}{K}\right)\left[\left(0..^{N}-1\right)\right]}$
209 208 adantr ${⊢}\left(\left(¬{J}={N}-1\wedge {\phi }\right)\wedge \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)\right)\to \mathrm{iEdg}\left({S}\right)={{I}↾}_{\left({F}\mathrm{cyclShift}{K}\right)\left[\left(0..^{N}-1\right)\right]}$
210 eqid ${⊢}{\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}={\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}$
211 1 2 198 199 5 200 202 209 140 210 eucrct2eupth1 ${⊢}\left(\left(¬{J}={N}-1\wedge {\phi }\right)\wedge \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)\right)\to \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{prefix}\left({N}-1\right)\right)\mathrm{EulerPaths}\left({S}\right)\left({\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}\right)$
212 10 a1i ${⊢}\left(\left(¬{J}={N}-1\wedge {\phi }\right)\wedge \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)\right)\to {H}=\left({F}\mathrm{cyclShift}{K}\right)\mathrm{prefix}\left({N}-1\right)$
213 190 oveq1d ${⊢}{\phi }\to \left|{F}\right|-{K}={N}-{K}$
214 213 breq2d ${⊢}{\phi }\to \left({x}\le \left|{F}\right|-{K}↔{x}\le {N}-{K}\right)$
215 214 adantl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \left({x}\le \left|{F}\right|-{K}↔{x}\le {N}-{K}\right)$
216 190 oveq2d ${⊢}{\phi }\to {x}+{K}-\left|{F}\right|={x}+{K}-{N}$
217 216 fveq2d ${⊢}{\phi }\to {P}\left({x}+{K}-\left|{F}\right|\right)={P}\left({x}+{K}-{N}\right)$
218 217 adantl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {P}\left({x}+{K}-\left|{F}\right|\right)={P}\left({x}+{K}-{N}\right)$
219 215 218 ifbieq2d ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)=if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)$
220 219 mpteq2dv ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)=\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)$
221 150 eqcomd ${⊢}{\phi }\to \left(0\dots {N}-1\right)=\left(0..^{N}\right)$
222 221 adantl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \left(0\dots {N}-1\right)=\left(0..^{N}\right)$
223 220 222 reseq12d ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}={\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0..^{N}\right)}$
224 6 adantl ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {N}=\left|{F}\right|$
225 224 oveq2d ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \left(0\dots {N}\right)=\left(0\dots \left|{F}\right|\right)$
226 144 225 sseqtrid ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to \left(0..^{N}\right)\subseteq \left(0\dots \left|{F}\right|\right)$
227 226 resmptd ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)↾}_{\left(0..^{N}\right)}=\left({x}\in \left(0..^{N}\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)$
228 223 227 eqtrd ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}=\left({x}\in \left(0..^{N}\right)⟼if\left({x}\le {N}-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-{N}\right)\right)\right)$
229 228 11 syl6reqr ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {Q}={\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}$
230 229 adantr ${⊢}\left(\left(¬{J}={N}-1\wedge {\phi }\right)\wedge \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)\right)\to {Q}={\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)↾}_{\left(0\dots {N}-1\right)}$
231 211 212 230 3brtr4d ${⊢}\left(\left(¬{J}={N}-1\wedge {\phi }\right)\wedge \left(\left({F}\mathrm{cyclShift}{K}\right)\mathrm{EulerPaths}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\wedge \left({F}\mathrm{cyclShift}{K}\right)\mathrm{Circuits}\left({G}\right)\left({x}\in \left(0\dots \left|{F}\right|\right)⟼if\left({x}\le \left|{F}\right|-{K},{P}\left({x}+{K}\right),{P}\left({x}+{K}-\left|{F}\right|\right)\right)\right)\right)\right)\to {H}\mathrm{EulerPaths}\left({S}\right){Q}$
232 197 231 mpdan ${⊢}\left(¬{J}={N}-1\wedge {\phi }\right)\to {H}\mathrm{EulerPaths}\left({S}\right){Q}$
233 155 232 pm2.61ian ${⊢}{\phi }\to {H}\mathrm{EulerPaths}\left({S}\right){Q}$