# 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 = Vtx ⁡ G$
eucrct2eupth1.i $⊢ I = iEdg ⁡ G$
eucrct2eupth1.d $⊢ φ → F EulerPaths ⁡ G P$
eucrct2eupth1.c $⊢ φ → F Circuits ⁡ G P$
eucrct2eupth1.s $⊢ Vtx ⁡ S = V$
eucrct2eupth.n $⊢ φ → N = F$
eucrct2eupth.j $⊢ φ → J ∈ 0 ..^ N$
eucrct2eupth.e $⊢ φ → iEdg ⁡ S = I ↾ F 0 ..^ N ∖ J$
eucrct2eupth.k $⊢ K = J + 1$
eucrct2eupth.h $⊢ H = F cyclShift K prefix N − 1$
eucrct2eupth.q $⊢ Q = x ∈ 0 ..^ N ⟼ if x ≤ N − K P ⁡ x + K P ⁡ x + K - N$
Assertion eucrct2eupth $⊢ φ → H EulerPaths ⁡ S Q$

### Proof

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