Step | Hyp | Ref
| Expression |
1 | | eucrctshift.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | eucrctshift.i |
. . . . 5
⊢ 𝐼 = (iEdg‘𝐺) |
3 | | eucrctshift.c |
. . . . 5
⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) |
4 | | eucrctshift.n |
. . . . 5
⊢ 𝑁 = (#‘𝐹) |
5 | | eucrctshift.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) |
6 | | eucrctshift.h |
. . . . 5
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
7 | | eucrctshift.q |
. . . . 5
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
8 | 1, 2, 3, 4, 5, 6, 7 | crctcshtrl 41026 |
. . . 4
⊢ (𝜑 → 𝐻(TrailS‘𝐺)𝑄) |
9 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝐻(TrailS‘𝐺)𝑄) → 𝐻(TrailS‘𝐺)𝑄) |
10 | | eucrctshift.e |
. . . . . . . 8
⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) |
11 | 2 | eupthf1o 41372 |
. . . . . . . 8
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼) |
13 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐻(TrailS‘𝐺)𝑄) → 𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼) |
14 | | trlis1wlk 40905 |
. . . . . . . . 9
⊢ (𝐻(TrailS‘𝐺)𝑄 → 𝐻(1Walks‘𝐺)𝑄) |
15 | 2 | 1wlkf 40819 |
. . . . . . . . 9
⊢ (𝐻(1Walks‘𝐺)𝑄 → 𝐻 ∈ Word dom 𝐼) |
16 | | wrdf 13165 |
. . . . . . . . 9
⊢ (𝐻 ∈ Word dom 𝐼 → 𝐻:(0..^(#‘𝐻))⟶dom 𝐼) |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . . 8
⊢ (𝐻(TrailS‘𝐺)𝑄 → 𝐻:(0..^(#‘𝐻))⟶dom 𝐼) |
18 | | df-f1o 5811 |
. . . . . . . . . 10
⊢ (𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝐹:(0..^(#‘𝐹))–onto→dom 𝐼)) |
19 | | dffo3 6282 |
. . . . . . . . . . 11
⊢ (𝐹:(0..^(#‘𝐹))–onto→dom 𝐼 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼∃𝑦 ∈ (0..^(#‘𝐹))𝑖 = (𝐹‘𝑦))) |
20 | | crctis1wlk 41002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹(CircuitS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
21 | 2 | 1wlkf 40819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
22 | | lencl 13179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐹 ∈ Word dom 𝐼 → (#‘𝐹) ∈
ℕ0) |
23 | 4 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(0..^𝑁) =
(0..^(#‘𝐹)) |
24 | 23 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑆 ∈ (0..^𝑁) ↔ 𝑆 ∈ (0..^(#‘𝐹))) |
25 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑆 ∈ (0..^(#‘𝐹)) → 𝑆 ∈
ℕ0) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹)))
→ 𝑆 ∈
ℕ0) |
27 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → 𝑦 ∈ ℕ0) |
28 | | nn0sub 11220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑆 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑆 ≤ 𝑦 ↔ (𝑦 − 𝑆) ∈
ℕ0)) |
29 | 26, 27, 28 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑆 ≤ 𝑦 ↔ (𝑦 − 𝑆) ∈
ℕ0)) |
30 | 29 | biimpac 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑦 − 𝑆) ∈
ℕ0) |
31 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ (0..^(#‘𝐹)) ↔ (𝑦 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑦 < (#‘𝐹))) |
32 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) →
(#‘𝐹) ∈
ℕ) |
33 | 31, 32 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (#‘𝐹) ∈
ℕ) |
34 | 33 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ∈ ℕ) |
35 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℝ) |
36 | 35 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) ∧ 𝑆 ∈
(0..^(#‘𝐹))) →
𝑦 ∈
ℝ) |
37 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢
((#‘𝐹) ∈
ℕ → (#‘𝐹)
∈ ℝ) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → (#‘𝐹)
∈ ℝ) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) ∧ 𝑆 ∈
(0..^(#‘𝐹))) →
(#‘𝐹) ∈
ℝ) |
40 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑆 ∈ (0..^(#‘𝐹)) → 𝑆 ∈ ℤ) |
41 | 40 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑆 ∈ (0..^(#‘𝐹)) → 𝑆 ∈ ℝ) |
42 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
(((#‘𝐹) ∈
ℝ ∧ 𝑆 ∈
ℝ) → ((#‘𝐹) + 𝑆) ∈ ℝ) |
43 | 38, 41, 42 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) ∧ 𝑆 ∈
(0..^(#‘𝐹))) →
((#‘𝐹) + 𝑆) ∈
ℝ) |
44 | 36, 39, 43 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) ∧ 𝑆 ∈
(0..^(#‘𝐹))) →
(𝑦 ∈ ℝ ∧
(#‘𝐹) ∈ ℝ
∧ ((#‘𝐹) + 𝑆) ∈
ℝ)) |
45 | | elfzole1 12347 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑆 ∈ (0..^(#‘𝐹)) → 0 ≤ 𝑆) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) ∧ 𝑆 ∈
(0..^(#‘𝐹))) → 0
≤ 𝑆) |
47 | | addge01 10417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
(((#‘𝐹) ∈
ℝ ∧ 𝑆 ∈
ℝ) → (0 ≤ 𝑆
↔ (#‘𝐹) ≤
((#‘𝐹) + 𝑆))) |
48 | 38, 41, 47 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) ∧ 𝑆 ∈
(0..^(#‘𝐹))) →
(0 ≤ 𝑆 ↔
(#‘𝐹) ≤
((#‘𝐹) + 𝑆))) |
49 | 46, 48 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) ∧ 𝑆 ∈
(0..^(#‘𝐹))) →
(#‘𝐹) ≤
((#‘𝐹) + 𝑆)) |
50 | 44, 49 | lelttrdi 10078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) ∧ 𝑆 ∈
(0..^(#‘𝐹))) →
(𝑦 < (#‘𝐹) → 𝑦 < ((#‘𝐹) + 𝑆))) |
51 | 50 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → (𝑆 ∈
(0..^(#‘𝐹)) →
(𝑦 < (#‘𝐹) → 𝑦 < ((#‘𝐹) + 𝑆)))) |
52 | 51 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → (𝑦 <
(#‘𝐹) → (𝑆 ∈ (0..^(#‘𝐹)) → 𝑦 < ((#‘𝐹) + 𝑆)))) |
53 | 52 | 3impia 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) → (𝑆 ∈ (0..^(#‘𝐹)) → 𝑦 < ((#‘𝐹) + 𝑆))) |
54 | 53 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) →
(((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹)))
→ 𝑦 <
((#‘𝐹) + 𝑆))) |
55 | 54 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹))))
→ 𝑦 <
((#‘𝐹) + 𝑆)) |
56 | 35 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) → 𝑦 ∈
ℝ) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹))))
→ 𝑦 ∈
ℝ) |
58 | 41 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹))))
→ 𝑆 ∈
ℝ) |
59 | | elfzoel2 12338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑆 ∈ (0..^(#‘𝐹)) → (#‘𝐹) ∈
ℤ) |
60 | 59 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑆 ∈ (0..^(#‘𝐹)) → (#‘𝐹) ∈
ℝ) |
61 | 60 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹))))
→ (#‘𝐹) ∈
ℝ) |
62 | 57, 58, 61 | ltsubaddd 10502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹))))
→ ((𝑦 − 𝑆) < (#‘𝐹) ↔ 𝑦 < ((#‘𝐹) + 𝑆))) |
63 | 55, 62 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹))))
→ (𝑦 − 𝑆) < (#‘𝐹)) |
64 | 63 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) →
(((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹)))
→ (𝑦 − 𝑆) < (#‘𝐹))) |
65 | 31, 64 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (((#‘𝐹) ∈ ℕ0
∧ 𝑆 ∈
(0..^(#‘𝐹))) →
(𝑦 − 𝑆) < (#‘𝐹))) |
66 | 65 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑦 − 𝑆) < (#‘𝐹)) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑦 − 𝑆) < (#‘𝐹)) |
68 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 − 𝑆) ∈ (0..^(#‘𝐹)) ↔ ((𝑦 − 𝑆) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ (𝑦 − 𝑆) < (#‘𝐹))) |
69 | 30, 34, 67, 68 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑦 − 𝑆) ∈ (0..^(#‘𝐹))) |
70 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 = (𝑦 − 𝑆) → (𝑧 + 𝑆) = ((𝑦 − 𝑆) + 𝑆)) |
71 | 70 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 = (𝑦 − 𝑆) → ((𝑧 + 𝑆) mod (#‘𝐹)) = (((𝑦 − 𝑆) + 𝑆) mod (#‘𝐹))) |
72 | 40 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑆 ∈ (0..^(#‘𝐹)) → 𝑆 ∈ ℂ) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹)))
→ 𝑆 ∈
ℂ) |
74 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → 𝑦 ∈ ℤ) |
75 | 74 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → 𝑦 ∈ ℂ) |
76 | 73, 75 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ)) |
77 | 76 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ)) |
78 | | npcan 10169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑦 − 𝑆) + 𝑆) = 𝑦) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((𝑦 − 𝑆) + 𝑆) = 𝑦) |
80 | 79 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (((𝑦 − 𝑆) + 𝑆) mod (#‘𝐹)) = (𝑦 mod (#‘𝐹))) |
81 | | zmodidfzoimp 12562 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (𝑦 mod (#‘𝐹)) = 𝑦) |
82 | 81 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑦 mod (#‘𝐹)) = 𝑦) |
83 | 80, 82 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (((𝑦 − 𝑆) + 𝑆) mod (#‘𝐹)) = 𝑦) |
84 | 71, 83 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ 𝑧 = (𝑦 − 𝑆)) → ((𝑧 + 𝑆) mod (#‘𝐹)) = 𝑦) |
85 | 84 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ 𝑧 = (𝑦 − 𝑆)) → 𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))) |
86 | 69, 85 | rspcedeq2vd 3291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ∃𝑧 ∈ (0..^(#‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))) |
87 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑆 ∈ (0..^(#‘𝐹)) ↔ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) |
88 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) |
89 | 88 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → 𝑦 ∈ ℂ) |
90 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℂ) |
91 | 90 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑆 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑆 <
(#‘𝐹)) → 𝑆 ∈
ℂ) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → 𝑆 ∈ ℂ) |
93 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
((#‘𝐹) ∈
ℕ → (#‘𝐹)
∈ ℂ) |
94 | 93 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑆 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑆 <
(#‘𝐹)) →
(#‘𝐹) ∈
ℂ) |
95 | 94 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → (#‘𝐹) ∈
ℂ) |
96 | 89, 92, 95 | subadd23d 10293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → ((𝑦 − 𝑆) + (#‘𝐹)) = (𝑦 + ((#‘𝐹) − 𝑆))) |
97 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → 𝑦 ∈ ℕ0) |
98 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℤ) |
99 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢
((#‘𝐹) ∈
ℕ → (#‘𝐹)
∈ ℤ) |
100 | | znnsub 11300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((𝑆 ∈ ℤ ∧
(#‘𝐹) ∈ ℤ)
→ (𝑆 <
(#‘𝐹) ↔
((#‘𝐹) − 𝑆) ∈
ℕ)) |
101 | 98, 99, 100 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑆 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ) → (𝑆 <
(#‘𝐹) ↔
((#‘𝐹) − 𝑆) ∈
ℕ)) |
102 | 101 | biimp3a 1424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑆 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑆 <
(#‘𝐹)) →
((#‘𝐹) − 𝑆) ∈
ℕ) |
103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → ((#‘𝐹) − 𝑆) ∈ ℕ) |
104 | 103 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → ((#‘𝐹) − 𝑆) ∈
ℕ0) |
105 | 97, 104 | nn0addcld 11232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → (𝑦 + ((#‘𝐹) − 𝑆)) ∈
ℕ0) |
106 | 96, 105 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → ((𝑦 − 𝑆) + (#‘𝐹)) ∈
ℕ0) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((𝑦 − 𝑆) + (#‘𝐹)) ∈
ℕ0) |
108 | | simplr2 1097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → (#‘𝐹) ∈ ℕ) |
109 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) → 𝑦 ∈ ℂ) |
110 | | subcl 10159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑦 − 𝑆) ∈ ℂ) |
111 | 109, 91, 110 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → (𝑦 − 𝑆) ∈ ℂ) |
112 | 95, 111 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → ((#‘𝐹) ∈ ℂ ∧ (𝑦 − 𝑆) ∈ ℂ)) |
113 | 112 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((#‘𝐹) ∈ ℂ ∧ (𝑦 − 𝑆) ∈ ℂ)) |
114 | | addcom 10101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((#‘𝐹) ∈
ℂ ∧ (𝑦 −
𝑆) ∈ ℂ) →
((#‘𝐹) + (𝑦 − 𝑆)) = ((𝑦 − 𝑆) + (#‘𝐹))) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((#‘𝐹) + (𝑦 − 𝑆)) = ((𝑦 − 𝑆) + (#‘𝐹))) |
116 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) → 𝑦 ∈ ℝ) |
117 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℝ) |
118 | 117 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑆 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑆 <
(#‘𝐹)) → 𝑆 ∈
ℝ) |
119 | | ltnle 9996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 ↔ ¬ 𝑆 ≤ 𝑦)) |
120 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑦 ∈
ℝ) |
121 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑆 ∈
ℝ) |
122 | 120, 121 | sublt0d 10532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((𝑦 − 𝑆) < 0 ↔ 𝑦 < 𝑆)) |
123 | 122 | biimprd 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 → (𝑦 − 𝑆) < 0)) |
124 | 119, 123 | sylbird 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (¬
𝑆 ≤ 𝑦 → (𝑦 − 𝑆) < 0)) |
125 | 116, 118,
124 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → (¬ 𝑆 ≤ 𝑦 → (𝑦 − 𝑆) < 0)) |
126 | 125 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → (𝑦 − 𝑆) < 0) |
127 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 − 𝑆) ∈ ℝ) |
128 | 116, 118,
127 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → (𝑦 − 𝑆) ∈ ℝ) |
129 | 37 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑆 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑆 <
(#‘𝐹)) →
(#‘𝐹) ∈
ℝ) |
130 | 129 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → (#‘𝐹) ∈
ℝ) |
131 | 128, 130 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) → ((𝑦 − 𝑆) ∈ ℝ ∧ (#‘𝐹) ∈
ℝ)) |
132 | 131 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((𝑦 − 𝑆) ∈ ℝ ∧ (#‘𝐹) ∈
ℝ)) |
133 | | ltaddneg 10130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((𝑦 − 𝑆) ∈ ℝ ∧ (#‘𝐹) ∈ ℝ) → ((𝑦 − 𝑆) < 0 ↔ ((#‘𝐹) + (𝑦 − 𝑆)) < (#‘𝐹))) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((𝑦 − 𝑆) < 0 ↔ ((#‘𝐹) + (𝑦 − 𝑆)) < (#‘𝐹))) |
135 | 126, 134 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((#‘𝐹) + (𝑦 − 𝑆)) < (#‘𝐹)) |
136 | 115, 135 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹)) |
137 | 107, 108,
136 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) ∧ (𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → (((𝑦 − 𝑆) + (#‘𝐹)) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹))) |
138 | 137 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑦 ∈ ℕ0
∧ 𝑦 < (#‘𝐹)) → ((𝑆 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑆 < (#‘𝐹)) → (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (#‘𝐹)) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹))))) |
139 | 138 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) → ((𝑆 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑆 <
(#‘𝐹)) → (¬
𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (#‘𝐹)) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹))))) |
140 | 87, 139 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) → (𝑆 ∈ (0..^(#‘𝐹)) → (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (#‘𝐹)) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹))))) |
141 | 140 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) →
(((#‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(#‘𝐹)))
→ (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (#‘𝐹)) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹))))) |
142 | 31, 141 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (((#‘𝐹) ∈ ℕ0
∧ 𝑆 ∈
(0..^(#‘𝐹))) →
(¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (#‘𝐹)) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹))))) |
143 | 142 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (#‘𝐹)) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹)))) |
144 | 143 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (((𝑦 − 𝑆) + (#‘𝐹)) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹))) |
145 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑦 − 𝑆) + (#‘𝐹)) ∈ (0..^(#‘𝐹)) ↔ (((𝑦 − 𝑆) + (#‘𝐹)) ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ ((𝑦 − 𝑆) + (#‘𝐹)) < (#‘𝐹))) |
146 | 144, 145 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((𝑦 − 𝑆) + (#‘𝐹)) ∈ (0..^(#‘𝐹))) |
147 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 = ((𝑦 − 𝑆) + (#‘𝐹)) → (𝑧 + 𝑆) = (((𝑦 − 𝑆) + (#‘𝐹)) + 𝑆)) |
148 | 147 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 = ((𝑦 − 𝑆) + (#‘𝐹)) → ((𝑧 + 𝑆) mod (#‘𝐹)) = ((((𝑦 − 𝑆) + (#‘𝐹)) + 𝑆) mod (#‘𝐹))) |
149 | 73 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑆 ∈ ℂ) |
150 | 75 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑦 ∈ ℂ) |
151 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℂ) |
152 | 151 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (#‘𝐹) ∈ ℂ) |
153 | 149, 150,
152 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (#‘𝐹) ∈
ℂ)) |
154 | 153 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (#‘𝐹) ∈
ℂ)) |
155 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(#‘𝐹) ∈ ℂ)
→ 𝑦 ∈
ℂ) |
156 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(#‘𝐹) ∈ ℂ)
→ (#‘𝐹) ∈
ℂ) |
157 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(#‘𝐹) ∈ ℂ)
→ 𝑆 ∈
ℂ) |
158 | 155, 157,
156 | nppcand 10296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(#‘𝐹) ∈ ℂ)
→ (((𝑦 − 𝑆) + (#‘𝐹)) + 𝑆) = (𝑦 + (#‘𝐹))) |
159 | 155, 156,
158 | comraddd 10129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(#‘𝐹) ∈ ℂ)
→ (((𝑦 − 𝑆) + (#‘𝐹)) + 𝑆) = ((#‘𝐹) + 𝑦)) |
160 | 154, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (((𝑦 − 𝑆) + (#‘𝐹)) + 𝑆) = ((#‘𝐹) + 𝑦)) |
161 | 160 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((((𝑦 − 𝑆) + (#‘𝐹)) + 𝑆) mod (#‘𝐹)) = (((#‘𝐹) + 𝑦) mod (#‘𝐹))) |
162 | 31 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (𝑦 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑦 < (#‘𝐹))) |
163 | 162 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑦 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑦 < (#‘𝐹))) |
164 | | addmodid 12580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑦 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑦 <
(#‘𝐹)) →
(((#‘𝐹) + 𝑦) mod (#‘𝐹)) = 𝑦) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (((#‘𝐹) + 𝑦) mod (#‘𝐹)) = 𝑦) |
166 | 161, 165 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((((𝑦 − 𝑆) + (#‘𝐹)) + 𝑆) mod (#‘𝐹)) = 𝑦) |
167 | 148, 166 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ 𝑧 = ((𝑦 − 𝑆) + (#‘𝐹))) → ((𝑧 + 𝑆) mod (#‘𝐹)) = 𝑦) |
168 | 167 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ 𝑧 = ((𝑦 − 𝑆) + (#‘𝐹))) → 𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))) |
169 | 146, 168 | rspcedeq2vd 3291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((#‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ∃𝑧 ∈ (0..^(#‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))) |
170 | 86, 169 | pm2.61ian 827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ∃𝑧 ∈ (0..^(#‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))) |
171 | 23 | rexeqi 3120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑧 ∈
(0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹)) ↔ ∃𝑧 ∈ (0..^(#‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))) |
172 | 170, 171 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(#‘𝐹))) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))) |
173 | 172 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) ∈
ℕ0 → (𝑆 ∈ (0..^(#‘𝐹)) → (𝑦 ∈ (0..^(#‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))))) |
174 | 24, 173 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) ∈
ℕ0 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(#‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))))) |
175 | 22, 174 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 ∈ Word dom 𝐼 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(#‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))))) |
176 | 20, 21, 175 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐹(CircuitS‘𝐺)𝑃 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(#‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))))) |
177 | 3, 5, 176 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑦 ∈ (0..^(#‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹)))) |
178 | 177 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝑦 ∈ (0..^(#‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹)))) |
179 | 178 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))) |
180 | 179 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹))) |
181 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹)) → (𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (#‘𝐹)))) |
182 | 181 | reximi 2994 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑧 ∈
(0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (#‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (#‘𝐹)))) |
183 | 180, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (#‘𝐹)))) |
184 | 3, 20, 21 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
185 | 184 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → 𝐹 ∈ Word dom 𝐼) |
186 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ) |
187 | 5, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑆 ∈ ℤ) |
188 | 187 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → 𝑆 ∈ ℤ) |
189 | 23 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ (0..^𝑁) ↔ 𝑧 ∈ (0..^(#‘𝐹))) |
190 | 189 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ (0..^𝑁) → 𝑧 ∈ (0..^(#‘𝐹))) |
191 | | cshwidxmod 13400 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑆 ∈ ℤ ∧ 𝑧 ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (#‘𝐹)))) |
192 | 185, 188,
190, 191 | syl2an3an 1378 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (#‘𝐹)))) |
193 | 192 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ (𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (#‘𝐹))))) |
194 | 193 | rexbidva 3031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (#‘𝐹))))) |
195 | 183, 194 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧)) |
196 | 1, 2, 3, 4, 5, 6 | crctcshlem2 41021 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (#‘𝐻) = 𝑁) |
197 | 196 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0..^(#‘𝐻)) = (0..^𝑁)) |
198 | 197 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (0..^(#‘𝐻)) = (0..^𝑁)) |
199 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → 𝑖 = (𝐹‘𝑦)) |
200 | 6 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐻‘𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧) |
201 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (𝐻‘𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧)) |
202 | 199, 201 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (𝑖 = (𝐻‘𝑧) ↔ (𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧))) |
203 | 198, 202 | rexeqbidv 3130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (∃𝑧 ∈ (0..^(#‘𝐻))𝑖 = (𝐻‘𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧))) |
204 | 195, 203 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → ∃𝑧 ∈ (0..^(#‘𝐻))𝑖 = (𝐻‘𝑧)) |
205 | 204 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑖 = (𝐹‘𝑦) → ∃𝑧 ∈ (0..^(#‘𝐻))𝑖 = (𝐻‘𝑧))) |
206 | 205 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (∃𝑦 ∈ (0..^(#‘𝐹))𝑖 = (𝐹‘𝑦) → ∃𝑧 ∈ (0..^(#‘𝐻))𝑖 = (𝐻‘𝑧))) |
207 | 206 | ralimdva 2945 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∀𝑖 ∈ dom 𝐼∃𝑦 ∈ (0..^(#‘𝐹))𝑖 = (𝐹‘𝑦) → ∀𝑖 ∈ dom 𝐼∃𝑧 ∈ (0..^(#‘𝐻))𝑖 = (𝐻‘𝑧))) |
208 | 207 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑖 ∈
dom 𝐼∃𝑦 ∈ (0..^(#‘𝐹))𝑖 = (𝐹‘𝑦) ∧ 𝜑) → ∀𝑖 ∈ dom 𝐼∃𝑧 ∈ (0..^(#‘𝐻))𝑖 = (𝐻‘𝑧)) |
209 | 208 | anim1i 590 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑖 ∈
dom 𝐼∃𝑦 ∈ (0..^(#‘𝐹))𝑖 = (𝐹‘𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(#‘𝐻))⟶dom 𝐼) → (∀𝑖 ∈ dom 𝐼∃𝑧 ∈ (0..^(#‘𝐻))𝑖 = (𝐻‘𝑧) ∧ 𝐻:(0..^(#‘𝐻))⟶dom 𝐼)) |
210 | 209 | ancomd 466 |
. . . . . . . . . . . . 13
⊢
(((∀𝑖 ∈
dom 𝐼∃𝑦 ∈ (0..^(#‘𝐹))𝑖 = (𝐹‘𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(#‘𝐻))⟶dom 𝐼) → (𝐻:(0..^(#‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼∃𝑧 ∈ (0..^(#‘𝐻))𝑖 = (𝐻‘𝑧))) |
211 | | dffo3 6282 |
. . . . . . . . . . . . 13
⊢ (𝐻:(0..^(#‘𝐻))–onto→dom 𝐼 ↔ (𝐻:(0..^(#‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼∃𝑧 ∈ (0..^(#‘𝐻))𝑖 = (𝐻‘𝑧))) |
212 | 210, 211 | sylibr 223 |
. . . . . . . . . . . 12
⊢
(((∀𝑖 ∈
dom 𝐼∃𝑦 ∈ (0..^(#‘𝐹))𝑖 = (𝐹‘𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(#‘𝐻))⟶dom 𝐼) → 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼) |
213 | 212 | exp31 628 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
dom 𝐼∃𝑦 ∈ (0..^(#‘𝐹))𝑖 = (𝐹‘𝑦) → (𝜑 → (𝐻:(0..^(#‘𝐻))⟶dom 𝐼 → 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼))) |
214 | 19, 213 | simplbiim 657 |
. . . . . . . . . 10
⊢ (𝐹:(0..^(#‘𝐹))–onto→dom 𝐼 → (𝜑 → (𝐻:(0..^(#‘𝐻))⟶dom 𝐼 → 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼))) |
215 | 18, 214 | simplbiim 657 |
. . . . . . . . 9
⊢ (𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼 → (𝜑 → (𝐻:(0..^(#‘𝐻))⟶dom 𝐼 → 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼))) |
216 | 215 | com13 86 |
. . . . . . . 8
⊢ (𝐻:(0..^(#‘𝐻))⟶dom 𝐼 → (𝜑 → (𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼 → 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼))) |
217 | 17, 216 | syl 17 |
. . . . . . 7
⊢ (𝐻(TrailS‘𝐺)𝑄 → (𝜑 → (𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼 → 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼))) |
218 | 217 | impcom 445 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐻(TrailS‘𝐺)𝑄) → (𝐹:(0..^(#‘𝐹))–1-1-onto→dom
𝐼 → 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼)) |
219 | 13, 218 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝐻(TrailS‘𝐺)𝑄) → 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼) |
220 | 9, 219 | jca 553 |
. . . 4
⊢ ((𝜑 ∧ 𝐻(TrailS‘𝐺)𝑄) → (𝐻(TrailS‘𝐺)𝑄 ∧ 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼)) |
221 | 8, 220 | mpdan 699 |
. . 3
⊢ (𝜑 → (𝐻(TrailS‘𝐺)𝑄 ∧ 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼)) |
222 | 1, 2, 3, 4, 5, 6, 7 | crctcshlem3 41022 |
. . . 4
⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
223 | 2 | iseupth 41368 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(EulerPaths‘𝐺)𝑄 ↔ (𝐻(TrailS‘𝐺)𝑄 ∧ 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼))) |
224 | 222, 223 | syl 17 |
. . 3
⊢ (𝜑 → (𝐻(EulerPaths‘𝐺)𝑄 ↔ (𝐻(TrailS‘𝐺)𝑄 ∧ 𝐻:(0..^(#‘𝐻))–onto→dom 𝐼))) |
225 | 221, 224 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐻(EulerPaths‘𝐺)𝑄) |
226 | 1, 2, 3, 4, 5, 6, 7 | crctcsh 41027 |
. 2
⊢ (𝜑 → 𝐻(CircuitS‘𝐺)𝑄) |
227 | 225, 226 | jca 553 |
1
⊢ (𝜑 → (𝐻(EulerPaths‘𝐺)𝑄 ∧ 𝐻(CircuitS‘𝐺)𝑄)) |