Step | Hyp | Ref
| Expression |
1 | | crctcsh.h |
. . . . 5
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
2 | | crctcsh.d |
. . . . . . 7
⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) |
3 | | crctis1wlk 41002 |
. . . . . . 7
⊢ (𝐹(CircuitS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
4 | | crctcsh.i |
. . . . . . . 8
⊢ 𝐼 = (iEdg‘𝐺) |
5 | 4 | 1wlkf 40819 |
. . . . . . 7
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
6 | 2, 3, 5 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
7 | | cshwcl 13395 |
. . . . . 6
⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼) |
9 | 1, 8 | syl5eqel 2692 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ Word dom 𝐼) |
10 | 9 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻 ∈ Word dom 𝐼) |
11 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) |
12 | | crctcsh.v |
. . . . . . . . . 10
⊢ 𝑉 = (Vtx‘𝐺) |
13 | 12 | 1wlkp 40821 |
. . . . . . . . 9
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉) |
14 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
15 | | crctcsh.s |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) |
16 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℕ0) |
18 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈
ℕ0) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈
ℕ0) |
20 | 17, 19 | nn0addcld 11232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ∈
ℕ0) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈
ℕ0) |
22 | | crctcsh.n |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑁 = (#‘𝐹) |
23 | | elfz3nn0 12303 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈
ℕ0) |
24 | 22, 23 | syl5eqelr 2693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (0...𝑁) → (#‘𝐹) ∈
ℕ0) |
25 | 24 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (#‘𝐹) ∈
ℕ0) |
26 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℤ) |
27 | 26 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℝ) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℝ) |
29 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ) |
30 | 29 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℝ) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℝ) |
32 | | elfzel2 12211 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℤ) |
33 | 32 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℝ) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑁 ∈ ℝ) |
35 | | leaddsub 10383 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆))) |
36 | 28, 31, 34, 35 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆))) |
37 | 36 | biimpar 501 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ 𝑁) |
38 | 37, 22 | syl6breq 4624 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ (#‘𝐹)) |
39 | 21, 25, 38 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ0 ∧
(#‘𝐹) ∈
ℕ0 ∧ (𝑥 + 𝑆) ≤ (#‘𝐹))) |
40 | 15, 39 | sylanl1 680 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ0 ∧
(#‘𝐹) ∈
ℕ0 ∧ (𝑥 + 𝑆) ≤ (#‘𝐹))) |
41 | | elfz2nn0 12300 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 + 𝑆) ∈ (0...(#‘𝐹)) ↔ ((𝑥 + 𝑆) ∈ ℕ0 ∧
(#‘𝐹) ∈
ℕ0 ∧ (𝑥 + 𝑆) ≤ (#‘𝐹))) |
42 | 40, 41 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(#‘𝐹))) |
43 | 42 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(#‘𝐹))) |
44 | 14, 43 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘(𝑥 + 𝑆)) ∈ 𝑉) |
45 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
46 | | elfzoel2 12338 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℤ) |
47 | | zaddcl 11294 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑥 + 𝑆) ∈ ℤ) |
48 | 47 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℤ) |
49 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈
ℤ) |
50 | 48, 49 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬
𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ) |
52 | | zsubcl 11296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ) |
53 | 52 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ) |
54 | 53 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℝ) |
55 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℝ) |
56 | | ltnle 9996 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 − 𝑆) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆))) |
57 | 54, 55, 56 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆))) |
58 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
59 | 58 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) |
60 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑆 ∈ ℤ → 𝑆 ∈
ℝ) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑆 ∈
ℝ) |
62 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑥 ∈
ℝ) |
63 | | ltsubadd 10377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆))) |
64 | 59, 61, 62, 63 | syl2an23an 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆))) |
65 | 59 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈
ℝ) |
66 | 48 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℝ) |
67 | 65, 66 | posdifd 10493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) ↔ 0 < ((𝑥 + 𝑆) − 𝑁))) |
68 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 0
∈ ℝ) |
69 | 50 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℝ) |
70 | | ltle 10005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((0
∈ ℝ ∧ ((𝑥 +
𝑆) − 𝑁) ∈ ℝ) → (0 <
((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
71 | 68, 69, 70 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (0 <
((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
72 | 67, 71 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
73 | 64, 72 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
74 | 57, 73 | sylbird 249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (¬
𝑥 ≤ (𝑁 − 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
75 | 74 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬
𝑥 ≤ (𝑁 − 𝑆)) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)) |
76 | 51, 75 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬
𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
77 | 76 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬
𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))))) |
78 | 26, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (0...𝑁) → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))))) |
79 | 78 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))))) |
80 | 29, 46, 79 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))))) |
81 | 80 | imp31 447 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
82 | | elnn0z 11267 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ0 ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
83 | 81, 82 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈
ℕ0) |
84 | 24 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (#‘𝐹) ∈
ℕ0) |
85 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ (0..^𝑁) ↔ (𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) |
86 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (0...𝑁) ↔ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) |
87 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℝ) |
88 | 87 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) → 𝑆 ∈ ℝ) |
89 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℝ) |
90 | 89 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑥
≤ 𝑁) → 𝑥 ∈
ℝ) |
91 | 88, 90 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → (𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ)) |
92 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
93 | 92, 92 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
94 | 93 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
96 | 91, 95 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
97 | | simpr3 1062 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → 𝑥 ≤ 𝑁) |
98 | | ltle 10005 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁)) |
99 | 87, 92, 98 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑆 < 𝑁 → 𝑆 ≤ 𝑁)) |
100 | 99 | 3impia 1253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) → 𝑆 ≤ 𝑁) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → 𝑆 ≤ 𝑁) |
102 | 96, 97, 101 | jca32 556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁))) |
103 | 85, 86, 102 | syl2anb 495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁))) |
104 | | le2add 10389 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))) |
105 | 104 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)) |
106 | 103, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)) |
107 | 66, 65, 65 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
108 | 107 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
109 | 26, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ (0...𝑁) → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
110 | 109 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
111 | 29, 46, 110 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
112 | 111 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
113 | | lesubadd 10379 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))) |
115 | 106, 114 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁) |
116 | 115 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁) |
117 | 116, 22 | syl6breq 4624 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ (#‘𝐹)) |
118 | 83, 84, 117 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ0 ∧
(#‘𝐹) ∈
ℕ0 ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (#‘𝐹))) |
119 | 15, 118 | sylanl1 680 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ0 ∧
(#‘𝐹) ∈
ℕ0 ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (#‘𝐹))) |
120 | | elfz2nn0 12300 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 + 𝑆) − 𝑁) ∈ (0...(#‘𝐹)) ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ0 ∧
(#‘𝐹) ∈
ℕ0 ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (#‘𝐹))) |
121 | 119, 120 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(#‘𝐹))) |
122 | 121 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(#‘𝐹))) |
123 | 45, 122 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) ∈ 𝑉) |
124 | 44, 123 | ifclda 4070 |
. . . . . . . . . 10
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉) |
125 | 124 | exp32 629 |
. . . . . . . . 9
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉))) |
126 | 13, 125 | syl 17 |
. . . . . . . 8
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉))) |
127 | 11, 126 | mpcom 37 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)) |
128 | 127 | imp 444 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉) |
129 | | crctcsh.q |
. . . . . 6
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
130 | 128, 129 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → 𝑄:(0...𝑁)⟶𝑉) |
131 | 12, 4, 2, 22, 15, 1 | crctcshlem2 41021 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐻) = 𝑁) |
132 | 131 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (0...(#‘𝐻)) = (0...𝑁)) |
133 | 132 | feq2d 5944 |
. . . . 5
⊢ (𝜑 → (𝑄:(0...(#‘𝐻))⟶𝑉 ↔ 𝑄:(0...𝑁)⟶𝑉)) |
134 | 130, 133 | mpbird 246 |
. . . 4
⊢ (𝜑 → 𝑄:(0...(#‘𝐻))⟶𝑉) |
135 | 134 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑄:(0...(#‘𝐻))⟶𝑉) |
136 | | wlkv 40815 |
. . . . . . . . 9
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
137 | 136 | simp1d 1066 |
. . . . . . . 8
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐺 ∈ V) |
138 | 12, 4 | is1wlkg 40816 |
. . . . . . . 8
⊢ (𝐺 ∈ V → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))) |
139 | 137, 138 | syl 17 |
. . . . . . 7
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))) |
140 | 139 | ibi 255 |
. . . . . 6
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))) |
141 | 2, 3, 140 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))) |
142 | 141 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))) |
143 | 22 | eqcomi 2619 |
. . . . . . . . . 10
⊢
(#‘𝐹) = 𝑁 |
144 | 143 | oveq2i 6560 |
. . . . . . . . 9
⊢
(0..^(#‘𝐹)) =
(0..^𝑁) |
145 | 144 | raleqi 3119 |
. . . . . . . 8
⊢
(∀𝑖 ∈
(0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
146 | | fzo1fzo0n0 12386 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ (0..^𝑁) ∧ 𝑆 ≠ 0)) |
147 | 146 | simplbi2 653 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ (0..^𝑁) → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁))) |
148 | 15, 147 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁))) |
149 | 148 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑆 ∈ (1..^𝑁)) |
150 | 149 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝑆 ∈ (1..^𝑁)) |
151 | | simplll 794 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝐹 ∈ Word dom 𝐼) |
152 | | 1wlkslem1 40809 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
153 | 152 | cbvralv 3147 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
(0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
154 | 153 | biimpi 205 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
(0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
155 | 154 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
156 | | crctprop 40998 |
. . . . . . . . . . . . . 14
⊢ (𝐹(CircuitS‘𝐺)𝑃 → (𝐹(TrailS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
157 | 143 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃‘(#‘𝐹)) = (𝑃‘𝑁) |
158 | 157 | eqeq2i 2622 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘𝑁)) |
159 | 158 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑃‘0) = (𝑃‘𝑁)) |
160 | 159 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑃‘𝑁) = (𝑃‘0)) |
161 | 160 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(TrailS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑃‘𝑁) = (𝑃‘0)) |
162 | 2, 156, 161 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0)) |
163 | 162 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (𝑃‘𝑁) = (𝑃‘0)) |
164 | 163 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (𝑃‘𝑁) = (𝑃‘0)) |
165 | 150, 129,
1, 22, 151, 155, 164 | crctcsh1wlkn0lem7 41019 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
166 | 131 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0..^(#‘𝐻)) = (0..^𝑁)) |
167 | 166 | raleqdv 3121 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
168 | 167 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
169 | 168 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
170 | 165, 169 | mpbird 246 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
171 | 170 | ex 449 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
172 | 145, 171 | syl5bi 231 |
. . . . . . 7
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
173 | 172 | ex 449 |
. . . . . 6
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((𝜑 ∧ 𝑆 ≠ 0) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))) |
174 | 173 | com23 84 |
. . . . 5
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))) |
175 | 174 | 3impia 1253 |
. . . 4
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
176 | 142, 175 | mpcom 37 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
177 | 10, 135, 176 | 3jca 1235 |
. 2
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(#‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
178 | 12, 4, 2, 22, 15, 1, 129 | crctcshlem3 41022 |
. . . 4
⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
179 | 178 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
180 | 12, 4 | is1wlk 40813 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(1Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(#‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))) |
181 | 179, 180 | syl 17 |
. 2
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻(1Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(#‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))) |
182 | 177, 181 | mpbird 246 |
1
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(1Walks‘𝐺)𝑄) |